My CNF file ends with many pairs of clauses that represent that two variables are equivalent (eg: -3 7, 3 -7, 5 -11, -5 11, etc.). Do most SAT solvers automatically pre-process these and replace every occurrence of one variable by the other (eg: replace every 7 by 3, and every 11 by 5), or should I first do the replacement processing to produce a simplified CNF file?


1 Answer 1


It won't hurt to do that, but you probably don't need to. If you happen to know that two variables are equivalent, a much easier way to let the solver use this information is simply to assert that they are equivalent:

$$\neg x_3 \leftrightarrow x_7$$

Which becomes, in CNF:

$$\left(x_3 \vee x_7\right) \wedge \left(\neg x_3 \vee \neg x_7\right)$$

Any solver based on DPLL knows how to use this information extremely efficiently.

If the variables appear enough, a CDCL solver will probably find these two clauses by itself eventually, but this would save it a bit of work.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.