3
$\begingroup$

In recent SAT competitions, there is a Certified UNSAT track. The problem instances are all unsatisfiable and the solvers are asked to produce certificates for unsatisfiability. One way is to produce a resolution refutation for the set of clauses in a problem instance. How can a SAT solver, say MiniSAT, be modified to do this? Can this be done for every solver? I searched the Internet and found little information. A reference is good for me.

$\endgroup$
  • $\begingroup$ Here is an example: mat.unb.br/ayala/MFingerSAT.pdf. CDCL solvers correspond to general resolution, whereas without clause learning you get only treelike resolution. These concepts are explained in lecture notes on the area, which can be found online. $\endgroup$ – Yuval Filmus Apr 28 '16 at 10:56
3
$\begingroup$

A clause-learning SAT solver can be described approximately as follows. There is a stash of learned clauses, which starts empty. We run a recursive procedure, which at each point in time, first checks whether the current assignment (initially empty) contradicts an axiom or something in the stash. If so, there is no need to explore this branch. Otherwise, it picks a variable, and tries both assignment recursively. When a recursive call corresponding to a partial assignment $\alpha$ returns, we learn the clause $\lnot \alpha$. At any given point in time we are allowed to forget clauses. (It's important for the proof that each clause is learned, even if we forget it later on).

We now take the transcript of the algorithm and consider the clauses in the order in which they are learned. We prove that whenever a clause $c$ is learned, it can be derived using the rules of resolution from existing clauses or from axioms; in particular, at the very end we derive contradiction.

We allow the weakening rule in the refutation we construct; we can always get rid of weakening later on without increasing the refutation length (exercise).

There are three cases to consider. If the clause $c$ was learned because the corresponding assignment contradicted an axiom $c'$ or a clause in the stash $c'$, then $c$ is a weakening of $c'$. The interesting case is when $c = \lnot \alpha$ was learned since both assignment to some variable $x$ failed to produce a satisfying assignment. These assignments correspond to the learned clauses $c \lor x$ and $c \lor \lnot x$, from which $c$ follows by resolution.

Note that if we never use clauses in the stash then the resulting refutation is tree-like (every clause is used once), assuming we state each axiom whenever it's needed (rather than once and for all). Also, in any case the size (number of lines) of the refutation is the same as the number of recursive calls.

$\endgroup$
3
$\begingroup$

The simplest method of modifying a typical DPLL-based CDCL solver is to have it output every clause it learned while deciding a formula is unsatisfiable. Such a list of clauses constitutes a RUP proof, which can be used to either construct a traditional resolution-based proof of unsatisfiability or show unsatisfiability directly using a somewhat different verification scheme. See "Verification of Proofs of Unsatisfiability for CNF Formulas" and "Verifying RUP Proofs of Propositional Unsatisfiability" for the details.

$\endgroup$
1
$\begingroup$

If you know something about CDCL conflict clause generation, you will know that they are produced by resolution per se. For example, on page 137 of Handbook of Satisfiability, clause learning is done by the following procedure: $$\omega_L^{d,i}=\begin{cases}\alpha(\kappa)&{\rm if\ }i=0\\ \omega_L^{d,i-1}\odot\alpha(l)&{\rm if\ }i\ne0\land\xi(\omega_L^{d,i-1},l,d)=1\\ \omega_L^{d,i-1}&{\rm if\ }i\ne0\land\forall_l\xi(\omega_L^{d,i-1},l,d)=0 \end{cases}$$ Here, $\alpha(v)$ is the antecedent of $v$. The first line specifies the base case. The recursion will ensue following the second line. The third line signals a fixed point and the process halts. Note in the second line, $\odot$ signifies resolution.

So just print the generation process and you will get a resolution refutation of the unsatisfiable formula.

$\endgroup$
-2
$\begingroup$

Not every solver can be thus modified, and people are searching for new solvers that cannot produce resolution refutations. (Resolution is slow and we want fast solvers.)

But CDCL solvers can p-simulate general resolution. That means they can produce resolution refutations that are only polynomially larger than general resolution. The method is written in Pipatsrisawat and Darwiche's On the power of clause-learning SAT solvers as resolution engines.

But that is not a good answer, because we want to show SAT solvers are slow, instead of how efficient they are. One way is to show general resolution p-simulates CDCL solvers. But people are too happy proving how good SAT solvers are to consider the other direction.

I don't know how to answer my own question. That's why I seem to turn this to a discussion forum. But that's why I'm asking in the first place.

Those who know why "CDCL solvers correspond to general resolution" please stand up and explain why general resolution is as good as CDCL SAT solvers!

$\endgroup$
  • $\begingroup$ Should it be that solvers p-simulate general resolution, or that general resolution p-simulates solvers? I guess it's the latter because we want to lowerbound the runtime of solvers. $\endgroup$ – Zirui Wang Apr 30 '16 at 17:57
  • $\begingroup$ I think this paper is proving wrong things. $\endgroup$ – Zirui Wang Apr 30 '16 at 18:04
  • $\begingroup$ The direction that general resolution is as good as CDCL SAT solvers is not there. Who can provide such a reference? Thanks a lot. $\endgroup$ – Zirui Wang Apr 30 '16 at 18:09
  • $\begingroup$ Welcome to CS.SE. This is a question-and-answer site, not a discussion forum. Please don't use answers to request clarification or ask new questions. If you have a follow-up question, please post it separately. Also, please make your answer self-contained: instead of referring to the comments, include the information in your answer. Comments exist only to help people improve their post and can be deleted at any time. I will delete the question part of your answer; please edit it to include a full citation to the paper you're referring to. $\endgroup$ – D.W. Apr 30 '16 at 18:26
  • $\begingroup$ The paper is just proving something else. What you want to show is that the transcript of a CDCL refutation can be converted to a resolution refutation. There won't be any polynomial blow-up in this direction. $\endgroup$ – Yuval Filmus Apr 30 '16 at 20:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.