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?
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
