How to check if sets of clauses are satisfiable.

390 Views Asked by At

I do not know how to check if the sets of clauses are satisfiable in an efficient way. Consider I have these sets for which I need to to check satisfiability. How do I do it efficiently without taking all the combinations into consideration iteratively?

Is this satisfiable: $\{(q, b),(r,¬e),(¬b, r),(¬d, ¬q),(¬q, ¬b),(¬r, ¬d),(d, e),(¬r, b)\}$? With few iterations I see it is but I am not sure.

What about this: $\{(r, b, ¬j), (¬r, e, f ), (j, ¬e), (j, ¬f), (a, ¬b, r), (¬a, f)\}$

1

There are 1 best solutions below

2
On BEST ANSWER

Davis Putnam is a pretty straightforward algorithm and goes fairly quickly just by hand (on paper). The basic idea is to keep 'splitting' on the different variables involved and 'reduce' the clause set accordingly. There are also some easy short-cuts and heuristics you can use to speed up the process.

For example, the second clause set contains $a$ as one of the variables, so let's 'split' on that $a$. This mean that we consider the two possibilities: $a$ is either true or false. Now, when $a$ is true, that means that every clause that contains $a$ will be satisfied, so we can remove it from the clause set. Moreover, any $\neg a$ can be removed from any clause that contains it, since clearly that clause cannot be satisfied by setting $a$ to true: we say that as such we are 'reducing' the clause with regard to $a$. So, this gives us as the remaining clause set:

$\{(r, b, ¬j), (¬r, e, f ), (j, ¬e), (j, ¬f), ( f)\}$

OK, and here is one of those short-cuts: clearly we now need to set $f$ to true since it is in a clause all by itself (a 'unit' clause). So, we can once again take out any clause containing $f$, and reduce the rest:

$\{(r,b,¬j), (j, ¬e), (j)\}$

Same for $j$:

$\{(r,b) \}$

And now we can either set $r$ or $b$ to true, and we're done: yes, it is satisfiable ... and apparently one way to do so is by setting all variables to true. (getting a model by keeping track of the splits is another nice feature of this method ... but always verify your answer to make sure you didn't make a mistake)

Of course, had this not worked, then we should also have considered the case where $a$ is false: now we can remove any clause containing $\neg a$, and remove any $a$ from all other clauses. Etc.

In general, you want to use a tree structure to keep track of the splittings that you go through. And yes, with large enough problems that still runs into exponential explosion, but that's the very nature of the satisfiability problem.