Talk:Boolean satisfiability problem

Untitled

Because of their length, the previous discussions on this page have been archived. If further archiving is needed, see Wikipedia:How to archive a talk page.

Previous discussions:

• Archive 1 (from creation to 18/10/2005)

Needs Discussion of Location of Hard SAT Problems

There is interesting work on the distribution of hard SAT problems, which seems like it should be discussed here. I don't have time to add it now, but here is a link to the seminal paper: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.7362 Polytrope (talk) 17:11, 9 March 2011 (UTC)

Why No Discussion on XOR-SAT?

It would be great to add some discussion on XOR-SAT —Preceding unsigned comment added by 128.30.64.21 (talk) 23:45, 10 August 2010 (UTC) There is a "hidden" reason every discussion is deleted: there is no constructive formula from OR-SAT in polynomial space able to represent a XOR-SAT. That contradicts the theorem of Cook which expects how the configuration would be. I would recommend you my own links, but I am sure this will be deleted too. — Preceding unsigned comment added by Juan Manuel Dato (talk • contribs) 14:19, 12 October 2012 (UTC)

Combine this Page with "Satisfiability and validity"

This page addresses the same topic, but in more detail. Suggest merging "Satisfiability and validity" into this by making it the introduction.

Proper Abbreviation Syntax

Is the proper syntax for abbreviating 3-Satisfiability "3SAT" or "3-SAT" (hyphen or no hyphen)? The page seems inconsistent with regards to this.

Sdoroudi (talk) 05:52, 1 June 2008 (UTC)

I've seen paper titles using 3-SAT,[1][2] 3SAT,[3] and even 3Sat.[4] In short, there is little agreement among researchers on this. Dcoetzee 08:55, 1 June 2008 (UTC)

That said, is there anyway to standardize the article (we can put in somewhere an "also abbreviated as" or something like that, the first time the abbreviations are mentioned). I don't much care which we go for, it would just be nice if the article is standardized. 131.215.170.228 (talk) 16:52, 1 June 2008 (UTC)

Sorry forgot to sign Sdoroudi (talk) 16:52, 1 June 2008 (UTC)

Satisfiability

Why does the Satisfiability page redirect to this article? Someone not interested in computational complexity theory might be interested merely in a simple definition of satisfiability for propositional and predicate logic. Nortexoid 05:21, 23 May 2006 (UTC)

Please feel free to turn that redirect into an article with these definitions. - Liberatore(T) 10:50, 23 May 2006 (UTC)

Organization

This page seems to be rather redundant and poorly organized to me (I'm quite familiar with the SAT problem). Or maybe I'm just drunk right now... 67.142.130.30 07:18, 12 July 2006 (UTC)

As an expert on Satisfiability, I agree that the page would benefit from some reorganisation and revisions targeted to improving clarity and accuracy of the information provided. I may have time to do this myself in a while, but perhaps the problems have been resolved by then ... Hh 00:20, 27 November 2006 (UTC)

k-SAT: At most k literals or exactly k literals?

There is disagreement between this article and the CNF article on the number of literals in each clause of a k-CNF formula. From Conjunctive Normal Form:

The k-SAT problem is the problem of finding a satisfying assignment to a boolean formula expressed in CNF such that each disjunction contains at most k variables.

From 3-SAT:

3-satisfiability is a special case of k-satisfiability (k-SAT) or simply satisfiability (SAT), when each clause contains exactly k = 3 literals.

Which is it? Should we choose one definition over the other, or should we provide both definitions to the reader? Moreover, must literals in each clause be unique? If yes, then this belongs in the article. Quaternion (talk) 03:08, 7 December 2007 (UTC)

It's very easy to convert between forms. CRGreathouse (t | c) 02:22, 10 March 2011 (UTC)

Factorization

The problem of factorizing a number can be reduced to boolean satisfiablity. Essentially, we build a network of logic gates that perform a multiplication of two sets of inputs A[0..n] and B[0..n] (taken to be binary numbers A and B) and give a set of outputs C[0..n]. Each C is then expressed as a boolean function of the inputs A and B - admittedly, a pretty big one, but finite. We then specify a number by asserting or denying C. Thus, to find the factors of 10 we would assert C[3] & ~C[2] & C[1] & ~C[0]. We also assert that neither A nor B is 1. If we then can satisfy this in polynomial time, the solution for A[0..n] wil be a factor of C. —Preceding unsigned comment added by 207.169.186.10 (talk) 05:50, 12 December 2007 (UTC)

Contradiction

This article is in direct contradiction with 2-SAT, which states:

2-satisfiability (abbreviated as 2-SAT) is a special case of satisfiability if expressions are written in conjunctive normal form with 2 variables per clause (2-CNF).

whereas this article insists on DNF! Can someone please fix? linas (talk) 17:39, 31 March 2008 (UTC)

As I said at Talk:2-satisfiability, it is not a contradiction. Sat in disjunctive normal form is trivial: each term gives a satisfying assignment. Sat in conjunctive normal form is, in general, hard, but 2-sat is an easier (though not as trivial as DNF) special case. —David Eppstein (talk) 17:52, 31 March 2008 (UTC)

The paragraph discussing SAT for DNF expressions just seems to be under the wrong section heading. I've moved it, which I think resolves the issue. Quaternion (talk) 17:57, 31 March 2008 (UTC)

Literals versus Variables

The description of the example for 3-Satisfiability includes the following sentence:

E has two clauses (denoted by parentheses), four literals (x1, x2, x3, x4), and k=3 (three literals per clause).

but in the example, there is also the literal not(x2) and not(x3). As far as I know, a literal is a variable or the negation of a variable in propositional logic, and a term or the negation of a term in predicate logic. Therefore, it should read "... four variables (x1, x2, x3, x4) ..." or "... five literals (x1, x2, not(x2), not(x3), x4) ...". The distinction between literals and variables (or atoms in predicate logic) is an important one, and this example description is confusing for newcomers to logic.

If you all agree, I will change the description, or somebody else, who is positive, might do. —Preceding unsigned comment added by 141.84.9.33 (talk) 17:09, 26 February 2009 (UTC)

Literals vs. Variables

I agree with you, this may be confusing to newcomers, I think it is better to say "literals formed with variables" or better "literals formed with atom names" atoms should be enough but "atom names" may be more informative to newcomers. Also I think this notation is better:

$({l}_{1\,1}\vee {l}_{1\,2}\vee {l}_{1\,3})\wedge ({l}_{2\,1}\vee {l}_{2\,2}\vee {l}_{2\,3})\wedge \ldots \wedge ({l}_{m\,1}\vee {l}_{m\,2}\vee {l}_{m\,3})$

where each ${l}_{i\,j}$ is a literal, i.e. a proposition variable or its negation

But the one given in the article shows better in the screen. I tried \mathcal{l} to display a calligraphic l, to avoid confusion with number one or capital i, but did not worked. Anyway this is a superfluous change in notation as the other is readable to anyone, but distinction between variables and literals should be clear and informative to newcomers as remarked by the previous user. —Preceding unsigned comment added by Elias (talk • contribs) 22:15, 6 June 2009 (UTC)

Vacuous lead

Judging by the lead there seems to be no problem. Shouldn't the lead give at least a hint as to what the problem is? Wikipedia expects an article's lead to summarize the article. The concept of Boolean satisfiability on its own is a triviality. --Vaughan Pratt (talk) 06:33, 19 March 2011 (UTC)

I added a paragraph. Did it help? 75.57.242.120 (talk) 01:47, 20 March 2011 (UTC)

Reading through the article, the whole thing (while containing good material) badly needs reorganization and rewriting. I'll see if I can mess with it in coming days/weeks/whatever, but expert help would be much appreciated. 75.57.242.120 (talk) 02:11, 20 March 2011 (UTC)

random SAT

We should add something about it. This looks useful. 75.57.242.120 (talk) 01:32, 20 March 2011 (UTC)

Preserving paragraph deleted from Boolean satisfiability problem#Exactly-1 3-satisfiability

I just deleted the following paragraph, putting it here in case I terribly misunderstood something:

(Context, kept:)

Another reduction involves only four new variables and three clauses: R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z).

(deleted:)

To prove that $R$ must exist, one first express $R$ as product of maxterms, then show that

$x\lor y\lor z=(\neg x\lor a\lor b)\land (\neg y\lor c\lor d)\land (\neg z\lor e\lor f)\land (a\lor c\lor e)$

The left side is evaluated true if and only if the right hand side is one-in-three 3SAT satisfied. The other variables are newly added variables that don't exist in any other expression.

(Context, kept:)

The one-in-three 3SAT problem is often used in the literature as a known NP-complete problem in a reduction to show that other problems are NP-complete.

My reasons for deleting:

• When proving that 3-SAT can be reduced to 1-in-3-SAT, the existence of R is assumed; there is no need to prove it.
• The equation is wrong: e.g. for x=y=z=FALSE and a=TRUE, the lhs and the rhs evaluates to FALSE and TRUE, respectively.
• I cannot see how the existence of R would follow from the equation.

Jochen Burghardt (talk) 18:30, 20 September 2013 (UTC)

How does the relation sol(1-in-3-sat) => sol(xor3sat) => sol(3-sat) imply cubic time for 3-sat?

The article states:

 As a consequence, for each CNF formula, either the 3-SAT problem or the 1-in-3-SAT problem can be decided in cubic time.

The unnecessarily complex convolution of 1-in-3-sat, xor3sat and 3-sat can be reduced to a simple truth table over the literals l_ij of a clause C_i being true or false, which shows that any solution for 1-in-3-sat is necessarily a solution for xor3sat. Also, any solution for xor3sat is necessarily a solution for 3-sat:

li1	li2	li3	1-in-3-sat	xor3sat	3-sat
0	0	0	0	0	0
0	0	1	1	1	1
0	1	0	1	1	1
0	1	1	0	0	1
1	0	0	1	1	1
1	0	1	0	0	1
1	1	0	0	0	1
1	1	1	0	1	1

However, there is no way backwards: 3-sat => xor3sat => 1-in-3-sat. And there is no connection between the complexities of how to obtain a solution.

If you obtain a solution for 1-in-3-sat in super-polynomial time, you also have a solution for xor3sat, that you could have obtained there in cubic time. So you were sort of clumsy. If you find a solution for xor3sat in cubic time, you got lucky for 3-sat. However, if the solution has 3 literals evaluating to true, it is not a valid solution for 1-in-3-sat. And so on ...

Wolfmanx (talk) 15:36, 25 November 2013 (UTC)

The description is really about substituting operators in a CNF formula. Let ⊥ stand for an n-ary operator for literals, so that the entire expression becomes true, if exactly one literal is true (do not ever show this to a mathematician!). Now you can derive the different versions by simple operator substitution:

CNF template:	( p ? q ? r) ∧ (s ? t ? u)
1-in-3-sat:	( p ⊥ q ⊥ r) ∧ (s ⊥ t ⊥ u)
xor3sat:	( p ⊕ q ⊕ r) ∧ (s ⊕ t ⊕ u)
3-sat:	( p ∨ q ∨ r) ∧ (s ∨ t ∨ u)

The reason, why it cannot be described this way, is that there is no binary operator for 1-in-2, that can be applied to a previous result and another variable to acquire the same result as a 1-in-3 operation. Or more formally, let f_2 be the binary 1-in-2 operator and f_3 the ternary 1-in-3 operator, then:

 f_2( f_2(a, b), c) != f_3(a, b, c)

This leads to the separation of graph theory and propositional logic. Graph theory deals with the annoying 1-in-2, 1-in-3, ..., 2-in-5, ... or any selection at all stuff. Propositional logic deals with the nice stuff that can be reduced to binary logic functions. Since it is possible to map back and forth between graph theory and propositional logic, everybody is happy (except me).

I find the graphic misleading. It is about the number of entries in a truth-table, that evaluate to true (1). It seems to imply some quality of the problem types, that is somehow related to set theory and cardinalities, which just makes no sense at all. All problems from 1-in-3-sat, xor3sat and 3-sat can be mapped onto each other. Just not necessarily in polynomial time. And 1-in-3-sat is not easier to solve than 3-sat. xor3sat is easier to solve, but it takes exponential time to map 3-sat to xor3sat.

When you consider, that for 2-satisfiabilty, 1-in-2-sat and xor2sat are equivalent, and further that all all 2-sat problems can be trivially mapped to an independent set problem, that is equivalent to a (different) 1-in-2-sat problem. Then it is easy to see, why 2-sat is necessarily solvable in polynomial time and why 3-sat is not: for 2-satisfiability, everything maps down to an xor2sat in polynomial time and can therefore be solved in polynomial time.

However, these simple relations cannot be described in a simple manner, since f_2( f_2(a, b), c) != f_3(a, b, c) does not fit in the otherwise perfect system of a propositional calculus, and it is forbidden to write (a ⊥ b ⊥ c) if it is not the same as ((a ⊥ b) ⊥ c) and not the same as (a ⊥ (b ⊥ c)).

Just to clarify, I really like this page and I come back here often for nourishment! Feel free to delete any unnecessary rant.

Wolfmanx (talk) 16:54, 25 November 2013 (UTC)

Concerning your 1st post, I think, you may have confused "decided" and "solved". My justification for the above cited sentence from the article is as follows: Given a CNF formula f, run the xor-3-SAT algorithm, which takes at most cubic time.

• If its result is "unsolvable", then the 1-in-3-SAT can't have a solution either, i.e. f has been decided to be 1-in-3-SAT unsolvable.
• If it returns a solution, then this is also a solution for the (ordinary) 3-SAT problem, i.e. f has been decided to be 3-SAT solvable.

I admit that the notions of 1-in-3-SAT, xor-3-SAT, and 3-SAT are confusing, and the presentation in the article is not optimal. I guess I tried to explain the same as you did using your p,q,r table (for one clause) when I introduced the picture (for two clauses) in section Boolean_satisfiability_problem#XOR-satisfiability, viz. "sol(1-in-3-sat) => sol(xor3sat) => sol(3-sat)". - Jochen Burghardt (talk) 17:42, 25 November 2013 (UTC)

Well, that's the reason why I posted in the first place: I was confused about the meaning of "decided" :)

I had to translate the statement to truth tables, ending up with the conclusion (in your words, emphasised additions by me):

• If its result is "unsolvable", then the 1-in-3-SAT can't have a solution either, i.e. f has been decided to be 1-in-3-SAT unsolvable, but nothing is decided about the 3-SAT problem.
• If it returns a solution, then this is also a solution for the (ordinary) 3-SAT problem, i.e. f has been decided to be 3-SAT solvable, but nothing is decided about the 1-in-3-SAT problem, if the solution requires any clause to have exactly 3 literals to be true.

This basically boils down to the sermon I wrote above about being lucky, etc. but your wording is definitely better.

Since I primarily try to understand the implications for SAT algorithms, I finally ended up with this abstract description to explain the section to myself:

The implication for a 3-SAT solution strategy is:

• 1-in-3-SAT (O(2^n)) is obsolete, because XOR3SAT does the same job in cubic time (O(n^3)).
• But if there is no solution for XOR3SAT, 3-SAT (O(2^n)) must be solved anyway.
• However, iff the negated XOR3SAT can be efficiently translated into a constraint for an algorithm, it is still useful to make the search space smaller (a variant of divide and conquer).

The last sentence is what was nagging me for a while now and forced me to come back again and again to figure it out:

• Translating an XOR3SAT problem into a general 3-SAT CNF problem can be done efficiently.
• The negation of a CNF is a DNF, which can be performed trivially in linear time.
• I don't know about DPLL/CDCL, but my own algorithm maps a DNF effectively in quadratic time. So I'm finally at peace and I will explore that further.

Wolfmanx (talk) 12:08, 26 November 2013 (UTC)

Converning your 2nd post, I admit that the article is not sufficiently explicit about the different operators in a CNF formula. It should better define the notion of a "generalized conjunctive normal form formula", viz. as a conjunction of arbitrarily many "generalized clauses", the latter being of the form R(l₁,l₂,l₃) for some fixed ternary boolean operator R and (oridinary) literals l_i. This form is used in the picture in section Boolean_satisfiability_problem#Exactly-1 3-satisfiability, but is never explicitly defined. This way, the problem of composing a ternary 1-of-3 operator from binary operators is avoided. Your truth table from your 1st post could be used to explain the different R operators for 1-in-3-SAT, xor-3-SAT, and (ordinary) 3-SAT. In fact, each of the three rightmost columns shows how the corresponding value R(p,q,r) should be defined, depending on the value of p, q, and r. Do you think that could make it more clear?

The picture you find misleading is that of section Boolean_satisfiability_problem#XOR-satisfiability, I guess? I intended just to give a visualization of your relation "sol(1-in-3-sat) => sol(xor3sat) => sol(3-sat)", seen as inclusion of solution sets: "yellow ⊆ blue ⊆ green" is all it should say - nothing about polynomial-time problem mappings and such stuff. - Jochen Burghardt (talk) 18:14, 25 November 2013 (UTC)

I certainly like your idea of the "generalized conjunctive normal form formula", since decomposition into truth tables is my own personal way to resolve my own confusion. However, I cannot speak for the general population.

I am aware of the functional operator notation, and use X1(l0, l1, l2) myself. I realize that I probably should have used it in the first place, instead of making up my own illustrative notation. I really must give up that habit :)

Yes, that is the picture I mean. It took me a while to figure out that it was about the "Distribution of Solutions for SAT problems", or as you say: "yellow ⊆ blue ⊆ green", and not about "Hardness of SAT problems". Granted that I could have read the description earlier, I still think a caption would help to avoid the confusion in the first place. I have colored the truth table to match the colors of the figure, so the meaning would become clear from the correlation.

Wolfmanx (talk) 12:08, 26 November 2013 (UTC)