The Boolean Satisfiability Problem and SAT Solvers

I've alway been interested in this problem. I feel like information theory, Bayesian analysis including Markov chain monte carlo could give you some insight into the distribution of truth values for a satisfiable configuration especially around the phase transition. You can covert 3-SAT into a Bayesian network but exact inference is still NP complete. There should be some higher order information in a graph of the k-SAT problem... But many of the algorithms here are still NPC (e.g. finding a clique).. So then you discover tree width (tree decomposition) as an approximation (also in Bayesian networks) and find out that it is quite useful but still doesn't quite help. It makes faster SAT solvers but we haven't found anything invariant yet.

Anyway I still enjoy thinking about the problem, my random ideas have taken on more structure based on diving into the different subjects and trying to use them on this problem. I find it fascinating that you can take something simple like these linear circuits and it turns out that they are not simple at all and that they scale through the different disciplines.

I'm a little doubtful about the quality of the article. In the first section it says...

"A problem is NP-complete if it belongs to the set (or “class” if you prefer) of the hardest problems in NP - hardest in the sense that every problem ever exists in NP can be reduced to them. (Thus being able to solve a NP-complete problem is equivalent to being able to solve every problem in NP)."

100% wrong. All problems in NP cannot be reduced to NP-Complete. All problems in NP-Complete can be converted between each other. I didn't bother reading the rest of the article, if this basic information is so wrong the rest probably is as well.

"At the moment the most efficient algorithm (for integers larger than 100 digits) we can implement into pre-existing computers{3} has a sub-exponential running time. But we can’t say for certainty that the it is not in P."

Author needs to fix this typo. Additionally, I think this is sloppy reasoning and will confuse readers. Sub-exponential algorithms include polynomial algorithms, so saying that "X is subexponential but we can't prove it is not in P" is not as precise as "Algorithm X is subexponential but at best superpolynomial, which is not to say that problem Y cannot be in P in general".

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

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

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.

For small n: http://www.kevinalbrecht.com/code/joy-mirror/jp-trutab.html

A P-complete programming language seems like an interesting concept in cases where you want to allow programmability but guarantee that running programs from idiots or hostile actors doesn't take too long. Is there any work in using Horn clauses as a sort of P-complete programming language, maybe a bit like Prolog? Or are there nicer P-complete problems that get the same effect?

NP-hard problems are quite interesting.