I know the procedure simply by transforming each clause l1 ∨ ⋯ ∨ ln to a conjunction of n − 2 clauses .
I try to show the values satisfying the original and the final formula with Z3 to show that they are equisatisfiable as an SMT file.
For clarify can you give any example about this procedure . Thank you.
Equivalence checking is done by asking the solver if there's an assignment that can distinguish two formulas. If there's no such assignment, then you can conclude the formulas are equivalent, or in the SAT context, equi-satisfiable.
Here's a simple example:
from z3 import *
a, b, c = Bools('a b c')
fml1 = Or(And(a, b), And(a, c))
fml2 = And(a, Or(b, c))
s = Solver()
s.add(Distinct(fml1, fml2))
print(s.check())
Now if fml1 is an arbitrary SAT formula, and fml2 is a 3-SAT converted version (I'm not saying the above are SAT and 3-SAT conversions, but substitute the result of your algorithm here), then we'd expect that the SAT solver cannot distinguish them, i.e., the formula Distinct(fml1, fml2) would be unsatisfiable. Indeed, we get:
unsat
establishing that they are the same.
If you are using SMTLib only, then the template to use is:
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert (distinct (or (and a b) (and a c))
(and a (or b c))))
(check-sat)