2
$\begingroup$

I am learning about the Conflict Driven Clause Learning method to solve SAT problems. In this method it is possible to learn clauses and add these in the set of the initial clauses. I understand a learned clause as the negation of a conjunction of clauses such that these make a formula false (conflict).

I have thinking in another way to add learned clauses, in parallel way, to the set of learned clauses. That is, select a random set of assignments for the all variables of a formula $\phi$. If these assignments make the formula false then add this to the set of learned clauses, using negation operator. Sorry by my ignorance but, Do you know if is it reasoning valid?

For example in the next formula in Dimacs format

1 4 0
1 -3 -8 0
1 8 12 0 
2 11 0
-7 -3 9 0
-7 8 -9 0
7 8 -10 0
7 10 -12 0

If 1=0 and 2=1 and 3=1 and 4=0 and 5=0 and 6=0 and 7=0 and 8=0 and 9=0 and 10=0 and 11=0 and 12=1 then $\phi$ is false. Then, the new set of formulas is

1 4 0
1 -3 -8 0
1 8 12 0 
2 11 0
-7 -3 9 0
-7 8 -9 0
7 8 -10 0
7 10 -12 0
1 -2 -3 4 5 6 7 8 9 10 11 -12
$\endgroup$
  • 1
    $\begingroup$ I have trouble understanding what you are asking. Your title and post don't seem to match, and shouldn't there be more tags? $\endgroup$ – Raphael Feb 20 '16 at 1:19
5
$\begingroup$

Your reasoning is valid, but it won't help a SAT solver go much faster. Your method produces long clauses that only forbid a single assignment. What you want to speed up a recursively searching SAT solver is to learn short clauses that forbid many assignments. That requires a more sophisticated learning strategy than adding a simple disjunction of the negation of the current variable assignment.

$\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.