6
$\begingroup$

Modern SAT solvers use the notion of "watched literals": when a value is chosen for a literal $l$, the solver only checks whether that falsifies clauses with $l$ in them if $l$ is one of the watched literals in the clause. This prevents checking every clause for every newly assigned literal.

The correctness of the scheme comes from the fact that clauses are disjunctions and will only be false if all literals in it are false. So we know it is not false until at least the watched literal is false, and we only need to check when that happens.

I am wondering why the dual idea of a "watched clause" is not used as well. This is how it would work: the overall formula is a CNF, that is, a conjunction of clauses. The watched literal scheme already checks very fast whether the CNF has become false. However, it would also be useful to detect when it becomes true: no further search would be needed then. A conjunction is only true if all clauses in it are true. So we choose one "watched clause" $C$ and, if a literal in $C$ is assigned a value, we check to see if $C$ has turned true. If so, we mark that clause as now irrelevant, and pick another clause not yet satisfied. If we cannot find a not-yet-satisfied clause, all clauses are satisfied and the problem is satisfiable.

I realize this would require keeping track of more information; assigning to literals would now not only require checking if they are watched literals, but also if they are in the watched clause. More importantly, looking for a new watched clause requires checking if other clauses are not yet satisfied, which means checking all their literals. Depending on the structure of the problem instance, this could be much slower. However, for some instances (for example, problems with small clauses) this would be much faster because satisfaction would be detected much sooner.

So my question is whether this is not used simply for empirical reasons (say, it would be slower for most benchmarks), or if there is a deeper flaw about it that I am missing.

A secondary question is: if this is a merely empirical issue, then is there some simple argument predicting this from the description of the technique alone, or is it something that would need to be observed in practice? Or, in other words, if this is a bad idea, is it so in principle, or just empirically?

Addendum:

It has been suggested by an answer that the notion of watched literals implies the use of DPLL which implies tracking which clauses have been satisfied, and that therefore the question does not make sense. It is true that watched literals are used in the context of DPLL, but it is not true that this means tracking satisfied clauses.

The paper on Chaff, which defined watched literals, describes DPLL in pseudo-code as

while (true) {
    if (!decide()) // if no unassigned vars
        return(satisifiable);
    while (!bcp()) { 
        if (!resolveConflict())
            return(not satisfiable);
    }
}

This shows that satisfiability is decided as positive only when all variables are assigned, not when all clauses are satisfied (which could happen much earlier). Chaff and zChaff have been the basis for many of modern SAT solvers, including the very prominent MiniSAT.

The same idea is described in detail in Filip Maric's paper "Formalization and Implementation of Modern SAT Solvers", which describes this approach as the basis for many of the most prominent SAT solvers today.

$\endgroup$
11
$\begingroup$

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear because there can be no backtracking once the formula is solved.

Meanwhile, to maintain your watched clause pointer you must do a search to find a new unsatisfied clause each time your watched clause is satisfied. That search is linear in the number of clauses in the formula. These searches will be triggered during the exponential part of the search and so you will probably do many of them on your way to finding a satisfying assignment.

The net result is that you will waste more time than you will save trying to immediately notice when all clauses are satisfied.

Note that if you're adapting a traditional SAT solver to count solutions, then your idea has more merit. Noticing that all clauses are satisfied while there are still unassigned variables means you have found $2^n$ solutions to the formula, where $n$ is the number of unassigned variables. This provides an exponential speedup over finding these solutions one by one, so the lazy clause tracking could potentially pay for itself. However, an alternative would be to notice a satisfying assignment in the usual way and then undo assignments in reverse order until a clause is left unsatisfied. You would have the same $2^n$ speedup without the clause tracking overhead.

$\endgroup$
-1
$\begingroup$

the question/ setup/ premise does not seem to describe the "watched literals" concept accurately/ correctly. here is a summary from a SAT survey paper 2008, Satisfiability Solvers Gomes, Kautz, Sabharwal, Selman p94

The watched literals scheme of Moskewicz et al. [170], introduced in their solver zChaff, is now a standard method used by most SAT solvers for efficient constraint propagation. This technique falls in the category of lazy data structures introduced earlier by Zhang [236] in the solver Sato. The key idea behind the watched literals scheme, as the name suggests, is to maintain and “watch” two special literals for each active (i.e., not yet satisfied) clause that are not FALSE under the current partial assignment; these literals could either be set to TRUE or be as yet unassigned. Recall that empty clauses halt the DPLL process and unit clauses are immediately satisfied. Hence, one can always find such watched literals in all active clauses.

the description earlier of DPLL in the chapter has the same mechanism/ terminology; "active" clauses are those not yet satisfied. (afaik) virtually every SAT technique keeps track of "active" clauses vs those that are currently unsatisfied under the current partial assignment. the "watched literal" concept is already tightly coupled with keeping track of active clauses as the question seems to wonder about.

$\endgroup$
  • $\begingroup$ Talking about active clauses does not mean you are tracking them individually. That simply means "if a clause has not yet been falsified, one can find watched literals for it." Moskewicz et al, which defined watched literals, shows their DPLL pseudo-code (included in the edited question). It shows that 'satisfiable' happens only when all variables are assigned, not when all clauses are satisfied. $\endgroup$ – user118967 May 16 '15 at 4:18
  • $\begingroup$ this overall is a subtle aspect worthy of further Computer Science Chat but it cant be sorted out in a few soundbites. the techniques sometimes overlap and its not always so clearcut. basically realize modern SAT solvers are extremely optimized after decades of research and all "low hanging fruit" type modifications have mostly been implemented already. if a relatively-simple-to-describe optimization is not in some solver it means its probably too expensive. some of this is too ambiguous to describe in language and one needs code samples or pseudocode to accurately describe/ analyze it more thoroughly. $\endgroup$ – vzn May 16 '15 at 15:27
  • $\begingroup$ There are two different issues at hand. The first is my simple optimization of "watched clauses", which you correctly say would be too simple to not have been adopted by now if it were any good. I did not believe it was good even when I asked it, my question was simply trying to understand why it would not be good because I am trying to understand SAT solvers better. The other issue, which you raised, is whether my assumption that solvers do not track satisfied clauses holds. It does hold. I did not send you just soundbites, I sent you two main references with pseudo-code that shows that. $\endgroup$ – user118967 May 16 '15 at 17:44
  • 1
    $\begingroup$ You mistake "active clause" for "true clause" (or "satisfied clause"). They say an "active clause" means "clause that are not FALSE under the current partial assignment", which is not the same as "true clause". It does not seem that you have checked the two technical references I sent you. Let me know when you do, and I will be glad to chat. $\endgroup$ – user118967 May 16 '15 at 22:10
  • 2
    $\begingroup$ There must have been some unfortunate misunderstanding here. I don't know why you think I am "dinging ppl over superior knowledge". I have merely been responding to you as factually as I can, and providing specific arguments. It does surprise me that you suggest I am being condescending when your very first comment starts with "??? lol" and then ridicules my question. It is also condescending to keep stating your point of view without checking (or at least reacting or responding to) the concrete references I gave you. I certainly checked and responded to yours. $\endgroup$ – user118967 May 17 '15 at 7:31

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.