How does the SAT solver produce the model(assignment[s])?

Question

Here is a very simple cnf instance as (x1 or x2 or x3)&(x1 or x2)&(x2 or x3)and the formula is definitely satisfiable, the solution is x1 = x2 = x3 = 1, that is enough. So,my question is how the solver produce the assignment using DPLL or other procedure? Thanks.

Answer 1

Well, basically, for the case of CDCL

(CDCL SAT solvers implement DPLL, but can learn new clauses and backtrack non-chronologically. Clause learning with conflict analysis does not affect soundness or completeness. Conflict analysis identifies new clauses using the resolution operation. Therefore each learnt clause can be inferred from the original clauses and other learnt clauses by a sequence of resolution steps. If cN is the new learnt clause, then ϕ is satisfiable if and only if ϕ ∪ {cN} is also satisfiable. Moreover, the modified backtracking step also does not affect soundness or completeness, since backtracking information is obtained from each new learnt clause.).(Source : Wikipedia)

it's working as follow :

At first pick a branching variable, x1. A yellow circle means an arbitrary decision.

Now apply unit propagation, which yields that x4 must be 1 (i.e. True). A gray circle means a forced variable assignment during unit propagation. The resulting graph is called implication graph.

Arbitrarily pick another branching variable, x3.

Apply unit propagation and find the new implication graph.

Here the variable x8 and x12 are forced to be 0 and 1, respectively.

Pick another branching variable, x2.

Find implication graph.

Pick another branching variable, x7.

Find implication graph.

Found a conflict!

Find the cut that lead to this conflict. From the cut, find a conflicting condition.

Take the negation of this condition and make it a clause.

Add the conflict clause to the problem.

Non-chronological back jump to appropriate decision level.

Back jump and set variable values accordingly.

(Answer completely from Wikipedia: Conflict-Driven_Clause_Learning#Example)

Here is a list (not complete for sure) of solvers who use the CDCL algorithm, you should check them out :

• MiniSAT.
• Zchaff SAT.
• Z3.
• ManySAT.