CODEWITHSUNDEEP
algorithmlogictheoryboolean-logic
Elaqqad
Elaqqad

Reputation: 85

Generating satisfiable and non satisfiable formulas

I am working in a project in which I have to generate propositional formulas in form CNF to perform some tests; And I come across the following questions:

  1. How to generate a random satisfiable formula ?
  2. How to generate a random valid formula ?

For the second question I have an idea, for example we can generate a random formula p and then take the formula p or not p and then convert the resulting formula in CNF but the problem is that can we generate all valid formulas this way?

The allowed booleans operators here are : or,and,not

Thank you for your help

Upvotes: 2

Views: 361

Answers (1)

blazs
blazs

Reputation: 4845

First, let L be the set of k literals l1,l2,l3,...,lk for prespecified k. Now given the set of literals we can generate CNF formulas from them.

I would suggest first choosing the number of clauses---i.e. the number of conjucted OR-expressions---, say m, and then n_1,n_2,...,n_m, where n_i is the number of OR-connected literals. You may choose these numbers at random, or you can have them as parameters to better control the size and structure of the formula.

For example, for m=2 and n1=2 and n2=2 you'd have CNFs of the form (l1 OR l2) AND (l3 OR l4) where li's are chosen from L and are either negated or not.

Now that you know what the formula will look like, iterate through positions of the literals and for each position:

  • choose a literal l from L uniformly at random;
  • flip a fair coin to decide whether to negate the literal.

You end up with a "random" formula in CNF. You don't know whether it is satisfiable, however.

Update (April 5th 2016). If you wanted to efficiently generate a random satisfiable CNF with given parameters k, m, and ni's, you would have to be able to efficiently compute which formulas are satisfiable (thus implicitly solving the 3-SAT problem). For this reason I believe there is no polynomial-time algorithm (unless P=NP) for generating random 3-CNF (so that each satisfiable 3-CNF with the given structure is equally likely). Because generating random 3-CNF is hard, so is generating CNF in general.

There are probably algorithms for generating a subset of satisfiable 3-CNF's, which might be good enough for practical purposes; the same goes for generating unsatisfiable instances.

Upvotes: 1

Related Questions