Conflict Driven Clause Learning combined with brute force

Question

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

Answer 1

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.