0
$\begingroup$

I have a model counting program bob. On some graph coloring formulas, bob got the right answer only after removing clause learning. That is to say, with clause learning, bob sometimes counts duplicate solutions, while satisfiability remains stable. This would be big news if true.

$\endgroup$
2
  • 2
    $\begingroup$ What's your question? We want you to state a specific question in the body of the question. This isn't the place for announcements or advertisements about new advances or new ideas. What does it mean for clause learning to be parsimonious? Can you define those terms and give some background to make your question interesting and useful for others? $\endgroup$ – D.W. Apr 23 at 2:24
  • $\begingroup$ I notice folks have given you similar feedback before: cs.stackexchange.com/questions/103061/…, cs.stackexchange.com/questions/77381/…. $\endgroup$ – D.W. Apr 23 at 2:26
4
$\begingroup$

I don't know precisely how Bob works, but let's talk about clause learning.

Suppose you have a set of variable assignments, $A$, say $x_1 = 0$, $x_2 = 1$, $x_3 = 0$. This is a single clause in disjunctive normal form:

$$A = \neg x_1 \wedge x_2 \wedge \neg x_3$$

The negation of this set of assignments is a single clause in conjunctive normal form:

$$\neg A = x_1 \vee \neg x_2 \vee x_3$$

So if you have a set of variable assignments that you know you never want to see in any solution, you can add its negation to a SAT problem in CNF and it remains a SAT problem in CNF.

With conflict-directed clause learning, you add clauses which correspond to "dead ends" in the search. Suppose you try some assignments and find that this is not a valid SAT solution. This means that you have identified a CNF clause which is unsatisfiable (i.e. a "conflict"). So if you can find an appropriate subset of assignments that inevitably leads to the dead end, and add its negation as a new clause, this has the effect of directing the search so that it will not get stuck in that dead end any more, while also not changing the solution set.

For model counting, you find a solution to the SAT problem, add its negation as a new clause, and then go try to find a solution to the augmented problem.

It would be big news indeed if adding the negation of a known solution to a SAT problem meant that the solution that you explicitly negated is still a solution. I suspect Bob has a bug.

$\endgroup$

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.