Reputation: 124

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

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.

Upvotes: 0

Answers (1)

Valentin Montmirail

Reputation: 2640

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.

enter image description here

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.

enter image description here