Thank you for sharing! A great reference for SAT solving is: Donald Knuth, The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. SAT is also a

Thank you for sharing! A great reference for SAT solving is: Donald Knuth, The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. SAT is also an opportunity to point to an important family of data structures called Binary Decision Diagrams, abbreviated as BDDs, and their variants. Using BDDs, you can solve many interesting tasks that would be infeasible with most other known methods. 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. More information is available from: https://en.wikipedia.org/wiki/Binary_decision_diagram https://en.wikipedia.org/wiki/Binary_decision_diagram and especially in: Donald Knuth, The Art of Computer Programming, Volume 4, Fascicle 1: Bitwise tricks & techniques; Binary Decision Diagrams, of which a fascicle is available online: http://www-cs-faculty.stanford.edu/~knuth/fasc1b.ps.gz http://www-cs-faculty.stanford.edu/~knuth/fasc1b.ps.gz 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: a∧(a∨x∨y)∧(¬a∨¬b)∧(c∨b)∧(d∨¬b) With SICStus Prolog and its CLP(B) library, we can express this task by posting the following query: ?- sat(A*(A + X + Y)*(~A + ~B)*(C+B)*(D + ~B)). In response, the system answers with: A = C, C = 1, B = 0, sat(X=:=X), sat(Y=:=Y), sat(D=:=D). This is an example of a SAT solver that is complete, 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 definitely be 1, and B must definitely be 0, to make the formula satisfiable at all. 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! Using the predicate labeling/1, you can generate all satisfying assignments on backtracking. In this concrete case, they are: ?- 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.