# Conflict Driven Clause Learning combined with brute force

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

• I have trouble understanding what you are asking. Your title and post don't seem to match, and shouldn't there be more tags? – Raphael Feb 20 '16 at 1:19