The Boolean Satisfiability Problem and SAT Solvers

http://0a.io/boolean-satisfiability-problem-or-sat-in-5-minutes/

by amirouche • 9 years ago

58 14 9 years ago

gfredtech• 9 years ago

NP-hard problems are quite interesting.

JPLeRouzic• 9 years ago

But a NP-hard problem is not necessarily hard to solve in a specific case. So most solvers try basically to enumerate possible solutions and prune them before solving them.

I would expect a smarter approach in solvers' design.

opportune• 9 years ago

"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".

acchow• 9 years ago

Agreed, the wording is a little strange but I think readers of this will understand the meaning anyway.

schoen• 9 years ago

It's probably no less incorrect than saying "the suspect is now somewhere north of Mexico, but we haven't been able to rule out the possibility that he's in Canada" (with an unstated assumption that normally people said to be north of Mexico would be found in the United States).

Edit: on reflection, I actually think I agree with opportune's concern after all, which I had slightly misunderstood at first.

threepipeproblm• 9 years ago

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

zmonx2• 9 years ago

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.

andrewflnr• 9 years ago

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?

zmonx2• 9 years ago

Datalog is a syntactic subset of Prolog, and Datalog queries can be evaluated in polynomial time. This does not fully answer your question, but I hope it is useful for you as a starting point.

sjg007• 9 years ago

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.

PhilWright• 9 years ago

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.

MLij• 9 years ago

From Wikipedia: "A problem p in NP is NP-complete if every other problem in NP can be transformed (or reduced) into p in polynomial time". https://en.wikipedia.org/wiki/NP-completeness

DerekL• 9 years ago

No, the article is correct. Wikipedia says, “A problem p in NP is NP-complete if every other problem in NP can be transformed (or reduced) into p in polynomial time.” They cite the paper “The complexity of theorem-proving procedures”, Stephen A. Cook (1971), which says:

    It is shown that any recognition
    problem solved by a polynomial time-
    bounded nondeterministic Turing
    machine can be "reduced" to the pro-
    blem of determining whether a given
    propositional formula is a tautology.

https://en.wikipedia.org/wiki/NP-completeness http://dl.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=805047

CarolineW• 9 years ago

You say:

All problems in NP cannot be reduced to NP-Complete.

I'm interested into what has led you to believe this to be the case. The word "Complete" here means this: Given any problem C in NPC, and any problem R in NP, any instance of R can be converted to an instance of C with only polynomial extra work. That includes converting the instance over, and then bringing the solution back.

All problems in NP-Complete can be converted between each other.

That is a simple consequence of the first bit, since problems in NPC are also in NP.

That matches what the article says.

So, what led you to believe the article to be wrong?

The Boolean Satisfiability Problem and SAT Solvers

Related Stories