Thank you for sharing! A great reference for SAT solving is: Donald Knuth, <i>The Art of Computer Programming</i>, Volume 4, Fascicle 6: Satisfiability.<p>SAT is also an opportunity to point to an important family of data structures called <i>Binary Decision Diagrams</i>, abbreviated as BDDs, and their variants. Using BDDs, you can solve many interesting tasks that would be infeasible with most other known methods.<p>Of particular relevance are ordered and reduced BDDs, sometimes abbreviated as ROBDDS, or also simply BDDs if it is clear from the context that they are ordered and reduced. A second very important variant are zero-suppressed BDDs, abbreviated as ZDDs.<p>More information is available from:<p><a href="https://en.wikipedia.org/wiki/Binary_decision_diagram" rel="nofollow">https://en.wikipedia.org/wiki/Binary_decision_diagram</a><p>and especially in:<p>Donald Knuth, <i>The Art of Computer Programming</i>, Volume 4, Fascicle 1: Bitwise tricks & techniques; Binary Decision Diagrams, of which a fascicle is available online:<p><a href="http://www-cs-faculty.stanford.edu/~knuth/fasc1b.ps.gz" rel="nofollow">http://www-cs-faculty.stanford.edu/~knuth/fasc1b.ps.gz</a><p>One application of BDDs is found in the constraint solvers for Boolean tasks that ship with some Prolog systems. For example, consider the SAT formula from the article:<p><pre><code> a∧(a∨x∨y)∧(¬a∨¬b)∧(c∨b)∧(d∨¬b)
</code></pre>
With SICStus Prolog and its CLP(B) library, we can express this task by posting the following query:<p><pre><code> ?- sat(A*(A + X + Y)*(~A + ~B)*(C+B)*(D + ~B)).
</code></pre>
In response, the system answers with:<p><pre><code> A = C, C = 1,
B = 0,
sat(X=:=X),
sat(Y=:=Y),
sat(D=:=D).
</code></pre>
This is an example of a SAT solver that is <i>complete</i>, which is an important classification that is also explained in the article. In this concrete case, the Prolog system's answer means that A and C must <i>definitely</i> be 1, and B must <i>definitely</i> be 0, to make the formula satisfiable at all.<p>In this concrete case, the other variables (X, Y and D) may each be assigned any of the two truth values: They have no influence on the formula's satisfiability!<p>Using the predicate labeling/1, you can <i>generate</i> all satisfying assignments on backtracking. In this concrete case, they are:<p><pre><code> ?- sat(A*(A + X + Y)*(~A + ~B)*(C+B)*(D + ~B)),
labeling([X,Y,D]).
A = C, C = 1, X = Y, Y = B, B = D, D = 0 ;
A = C, C = D, D = 1, X = Y, Y = B, B = 0 ;
A = Y, Y = C, C = 1, X = B, B = D, D = 0 ;
A = Y, Y = C, C = D, D = 1, X = B, B = 0 ;
A = X, X = C, C = 1, Y = B, B = D, D = 0 ;
A = X, X = C, C = D, D = 1, Y = B, B = 0 ;
A = X, X = Y, Y = C, C = 1, B = D, D = 0 ;
A = X, X = Y, Y = C, C = D, D = 1, B = 0.</code></pre>