Testing Equivalence

Short description

Write a program which gets two CNF formulas in DIMACS format at the input and checks if the formulas are equivalent, or if at least one of the formulas implies the other one.

Input

The input to your program is given in form of two files in DIMACS format (also described in the first task). The files represent two formulas \(\varphi\) and \(\psi\).

Output

The program prints on the output the information on whether \(\varphi\Leftrightarrow \psi\), \(\varphi\Rightarrow\psi\), \(\varphi\Leftarrow\psi\), or none of these holds.

Extended description

The basic task is to check if one of the formulas implies the other one. Assume we want to check whether \(\varphi\Rightarrow\psi\) is a valid formula which means that it should hold for every assignment.

We have that \(\varphi\Rightarrow\psi\) holds for every assignment if \(\neg(\varphi\Rightarrow\psi)\) does not hold for any assignment, in other words, it is unsatisfiable. The latter formula can be rewritten as \[\neg(\varphi\Rightarrow\psi)\equiv \varphi\land\neg\psi\] Since \(\psi\) is a CNF, we can use de Morgan rules to turn \(\neg\psi\) into a DNF \(\psi'\). We now have a formula in NNF \(\varphi\land\psi'\) We can now check if \(\varphi\land\psi'\) is unsatisfiable in two ways.

1. Use Tseitin encoding to turn \(\varphi\land\psi'\) into a CNF and call a SAT solver on this CNF formula. This amounts one SAT cal on a possibly big CNF formula. Moreover we need to introduce new variables (basically, one for each clause of \(\psi\)).
2. We have that \(\psi'\) is a disjunction of terms \(\psi'=\bigvee_{C\in \psi}(\neg C)\) where \(C\) is a clause in \(\psi\) and \(\neg C\) is interpreted as \(\neg C=\bigwedge_{l\in C}\neg l\). By using distributivity we can thus write that \[\varphi\land\psi'\equiv\bigvee_{C\in \psi}\left(\varphi\land \neg C\right)\] We can thus use SAT solver on formulas \(\varphi\land\neg C\) for every \(C\in\psi\) to check whether it is unsatisfiable. In this way we get a bigger number of SAT calls, but the SAT solver is called on smaller formulas and we do not need to introduce any new variables. Note also that in this case the SAT solver is called on \(\varphi\) with different assumptions \(\neg C\), we can thus use incremental capabilities of the SAT solver which means that it can (for example) reuse learned clauses.

Implement both of these approaches and compare them on several SATLIB Benchmark Problems.