![]() | This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||||||||||||||||||
|
This page addresses the same topic, but in much less detail. Suggest merging this page into "Boolean satisfiability problem" by making it the introduction.
This unfinished sentence was on the page. Anyone care to finish this?
Validity of propositional formulae is immediately seen to be
It's currently commented out in the wikitext of the page Sam Douglas ( talk) 04:38, 5 July 2009 (UTC)
... solved by Juan Manuel Dato.
I had it for years, I hope someone review my code in Python 3.0
http://www.archive.org/details/TheSat3ProblemSolved
You can understand the algorithm graphically in
http://www.archive.org/details/ExampleInSpanishOfSatInP
If you prove the code, the #P problem is not exactly solved, SAT yes. I do not know if there is a bug in the code, I suppose not (obviously). The formula is a list of functors of 3 literals, where negative means the opposite (-1 = ~X1) and 0 means literal always False. So the clausules can be constructed with 1, 2 or 3 literals.
Prove it and say if it is right, there are too many technologies hidden yet. —Preceding
unsigned comment added by
79.109.169.86 (
talk) 18:19, 27 January 2011 (UTC)
Here you are a riguorous constructive demonstration
http://www.archive.org/details/ConnectionBetweenSat3AndPBetweenMatch-n —Preceding
unsigned comment added by
79.109.169.15 (
talk)
13:52, 20 March 2011 (UTC)
The result of the move request was: page moved. Vegaswikian ( talk) 00:23, 20 March 2010 (UTC)
Satisfiability and validity →
Satisfiability — I think this should be the main article titled "Satisfiability."
Greg Bard
21:31, 5 March 2010 (UTC)
A formula isn't valid iff its negation is satisfiable. If satisfiability were semi-decidable, then unvalidity would be also. Therefore, as validity and unvalidity would be semi-decidable, they would be decidable indeed, which is not possible by Church-Turing *theorem*.
Am I correct? Maybe I'm missing a subtle point. —Preceding unsigned comment added by Corovo ( talk • contribs) 15:58, 11 August 2010 (UTC)
Your argument seems convincing to me, but I think this page states the opposite (in the last paragraph): http://www.coli.uni-saarland.de/projects/milca/courses/comsem/html/node189.html#sec_foinference.problems.3 I am not sure what to believe, and unfortunately I don't have time at the moment to properly examine the problem. FactorialG ( talk) 13:32, 30 May 2012 (UTC)
I would say that they mean unsatisfiability, because they say "not satifiable" in the next sentence. Corovo is right. One can read it here on page 30: https://www.inf.tu-dresden.de/content/institutes/thi/algi/lehre/SS12/AL12/skript/script120413.pdf Martin 91.57.52.115 ( talk) 10:45, 21 July 2012 (UTC)
This description is misleading. There are methods for testing the satisfiability and unvalidity of some statements, just not all statements. This may fit the description of not semidecidable, but it gives the impression there's no semialgorithm for testing satisfiability outside the scope of validity, which is clearly false or we would have no SMT solvers or independence proofs. Also, link rot for the cite.
Argh, I think I just made a mess of this article by mentioning satisfiability modulo theories. The problem is that the article about interpretations states that interpretations are interpretations of theories, but this isn't really the right idea, because for boolean sat, we have interpretations but not theories in this sense, viz not theory (mathematical logic). This inconsistency needs to be resolved across the set of inter-related articles. linas ( talk) 21:59, 13 June 2011 (UTC)
I strongly recommend my document; I cannot show to the world, but I have years studing the problem and NOW I got the solution: Maths are ambiguous, and we can create two TM; each philosophy can get us a different correct response to the question "NP=P?". And the question about if SAT is semidecidable can be read with an easy transformation (every boolean-fbf in SAT). I have to argue something more: the problem XOR-AND and OR-AND SAT are very different..., but those questions will give me hours and hours of explanations.
http://archive.org/details/TheUltimateDefinitionOfNp
I could be sure that there are more true and hidden demonstrations and false and famous in other hand than experts of the area. Please create a forum: my link show two easy demonstrations..., easier impossible. The demonstration NP is not P (in constructive philosophy) is got with diagonalization, and #P=P (in the infinitum philosophy) is very graphical with examples.
I got awful responses from editor in chief, saying nonsenses like "NP problem resolution is nothing with technology". Journals are DEAD and the Claymath Institute is a false institution too: so we cannot know if problems are solved or not.
The language on satisfiability is, again, vague. In general even satisfiability of a theory in propositional logic is not decidable, and similarly the satisfiability of a variable-free equational theory in the language with only $0$, $1$, $+$, and $=$ is not decidable. This is because the decision process can only look at a finite part of the theory before making a decision, and there could be an inconsistency in the part that was not looked at before the decision procedure halts. Thus the decision process will either say that some satisfiable theories are unsatisfiable, or it will say that some unsatisfiable theories are satisfiable. The only thing that can be decidable, in principle, is satisfiability of a sentence or the satisfiability of a finite set of sentences. The latter is equivalent to the former in many contexts.
On to unification. Unification is simply a deductive system for first-order logic. It is not any stronger or weaker than any other deductive system (natural deduction, Hilbert-style, etc.). All of these allow us to enumerate the provable consequences of a theory. None of them can be used to solve the satisfiability question in for theories, only for sentences in some limited circumstances. — Carl ( CBM · talk) 14:51, 16 June 2011 (UTC)
Are we arguing about something, or are we in violent agreement? I'm not claiming half of the things you seem to say I'm claiming, so I don't understand why this conversation is so argumentative. Honestly, I've never studied first-order logic, I do not possess any books that treat first-order logic as a subject of study; certainly Cohen's Universal algebra doesn't treat it as a topic, nor does the term-rewriting book, nor does Hodges' Model theory book. Yet all of these books touch on satisfiability and do so in a concrete fashion. If you believe that all of these different definitions of satisfiability are the same thing, that's fine. And you're almost surely right, and I think here we agree; at some informal level, I do understand that they're all the same. But the reality is that none of these authors felt compelled to define first-order logic before they could talk about satisfiability; the subject matter didn't call for it. Perhaps this article doesn't need to either; it may be a source of confusion to the student. Informally, we agree its all the same thing. Formally, I have no reference which states, in a formal fashion, that these varying definitions really are all the same thing. linas ( talk) 02:06, 18 June 2011 (UTC)
I don't think there is a difference between satifiability in universal algebra and satisfiability in first-order logic, and in fact the fundamentals of universal algebra are a subset of those of first-order logic. The only difference is that universal algebra uses slightly different terminology and then goes off in a different direction.
Although they historically did not always point it out in their publications, the connection is very well known to universal algebraists. You can ask User:Vaughan Pratt. (IIRC he thinks of himself primarily as a universal algebraist.) Or you can look in Chapter IX of the revised (1981) edition of Paul Cohen's Universal Algebra. Its title is Model theory and universal algebra, and it starts with Chang and Keisler's slogan "universal algebra + logic = model theory". Even the old edition had Chapter V, Relational structures and models, and Chapter VI, Axiomatic model classes. These three chapters are really about first-order model theory. Similarly, Grätzer's Universal Algebra used to end with Chapter 6 (Elements of model theory), Chapter 7 (Elementary properties of algebraic structures) and Chapter 8 (Free $\Sigma$-structures), all of which are about first-order model theory. (In the second (2008) edition there are new appendices which go in a different direction.)
What we need in this article is not a separate definition of satisfiability for universal algebra, but a brief explanation of how first-order satisfiability specialises to that important case. Hans Adler 00:42, 19 June 2011 (UTC)
Sigh. I'm pretty sure I never added text that implied it was decidable! Hey! I'm not an idiot! BTW, please note what finite model theory has to say about Goedel and completeness! I also didn't realize that reading books on lambda calc, term rewriting, model theory, and papers on SMT, answer-set programming was "focusing on one case"; I thought that this provided fairly broad coverage of the topic. I work for a chip-design company; yes, the hardware verification tools people have a vast number of constraint satisfaction problems (timing, routing, etc.) These are all "satisfiability" problems, and there's already a small universe of WP pages for these topics: e.g. model checking, local consistency, etc. Some of those pages (I skimmed them recently) link back to this article, or the article on structure (mathematical logic), or to model theory article. Many do not: e.g. local consistency which has three different sections discussing satisfiability, none linking here. Note also discussion of satisfiability in complexity of constraint satisfaction where the theory of relational databases mentioned. (somewhat off-topic, but note that SQL has very rigorous satisfiability demands; keystores became very popular recently precisely because they dump this, and do not require consistency. There's a recent interesting article that points out that keystores and SQL are adjoint, in the sense of monad (category theory). I wouldn't be half surprised if there's some paper somewhere that points out that consistency (in general) and satisfiability (in general) are adjoint in the same sense. But again, the point is that essentially none of these discussions read on or use "first-order logic" as a touchstone definition for satisfiability. linas ( talk) 03:33, 22 June 2011 (UTC)
The first section includes the claim:
"For logics without negation, such as the positive propositional calculus, the questions of validity and satisfiability may be unrelated. In the case of the positive propositional calculus, the satisfiability problem is trivial, as every formula is satisfiable, while the validity problem is co-NP complete."
This corresponds to a similar claim in the article on co-NP-complete (added by the same user). I've argued there that I believe this to be wrong; unless I'm mistaken, for a positive Boolean formula to be a tautology, it is necessary and sufficient for it to be true when all variables are false, and this is easily checked in polynomial time. (Of course, it could still be co-NP-complete, but then we would have P=NP, among other things – highly unlikely.) -- Mlhetland ( talk) 19:52, 27 January 2016 (UTC)
To address the "too technical" complaint in the lead, I attempted a rewrite which preserves the original content but uses more accessible language. Constructive feedback, improvements, or discussion welcome!
One subtlety is that, informally, one would typically refer to something like as unsatisfiable, when in reality it is satisfiable in FOL without additional axioms and only unsatisfiable over the usual theory of the integers (or at least a sufficient subset of the integer axioms). I used integer constraint examples to introduce satisfiability informally, but then provided the technical definition. If we want to avoid these issues, we could stick to propositional logic examples in the lead, even if that is a bit less intuitive. On the other hand, I am not sure if the lead should favor the purely logical meaning of the word "satisfiability" over the meaning modulo a theory, since this is an article about the concept of satisfiability in general.
![]() | This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||||||||||||||||||
|
This page addresses the same topic, but in much less detail. Suggest merging this page into "Boolean satisfiability problem" by making it the introduction.
This unfinished sentence was on the page. Anyone care to finish this?
Validity of propositional formulae is immediately seen to be
It's currently commented out in the wikitext of the page Sam Douglas ( talk) 04:38, 5 July 2009 (UTC)
... solved by Juan Manuel Dato.
I had it for years, I hope someone review my code in Python 3.0
http://www.archive.org/details/TheSat3ProblemSolved
You can understand the algorithm graphically in
http://www.archive.org/details/ExampleInSpanishOfSatInP
If you prove the code, the #P problem is not exactly solved, SAT yes. I do not know if there is a bug in the code, I suppose not (obviously). The formula is a list of functors of 3 literals, where negative means the opposite (-1 = ~X1) and 0 means literal always False. So the clausules can be constructed with 1, 2 or 3 literals.
Prove it and say if it is right, there are too many technologies hidden yet. —Preceding
unsigned comment added by
79.109.169.86 (
talk) 18:19, 27 January 2011 (UTC)
Here you are a riguorous constructive demonstration
http://www.archive.org/details/ConnectionBetweenSat3AndPBetweenMatch-n —Preceding
unsigned comment added by
79.109.169.15 (
talk)
13:52, 20 March 2011 (UTC)
The result of the move request was: page moved. Vegaswikian ( talk) 00:23, 20 March 2010 (UTC)
Satisfiability and validity →
Satisfiability — I think this should be the main article titled "Satisfiability."
Greg Bard
21:31, 5 March 2010 (UTC)
A formula isn't valid iff its negation is satisfiable. If satisfiability were semi-decidable, then unvalidity would be also. Therefore, as validity and unvalidity would be semi-decidable, they would be decidable indeed, which is not possible by Church-Turing *theorem*.
Am I correct? Maybe I'm missing a subtle point. —Preceding unsigned comment added by Corovo ( talk • contribs) 15:58, 11 August 2010 (UTC)
Your argument seems convincing to me, but I think this page states the opposite (in the last paragraph): http://www.coli.uni-saarland.de/projects/milca/courses/comsem/html/node189.html#sec_foinference.problems.3 I am not sure what to believe, and unfortunately I don't have time at the moment to properly examine the problem. FactorialG ( talk) 13:32, 30 May 2012 (UTC)
I would say that they mean unsatisfiability, because they say "not satifiable" in the next sentence. Corovo is right. One can read it here on page 30: https://www.inf.tu-dresden.de/content/institutes/thi/algi/lehre/SS12/AL12/skript/script120413.pdf Martin 91.57.52.115 ( talk) 10:45, 21 July 2012 (UTC)
This description is misleading. There are methods for testing the satisfiability and unvalidity of some statements, just not all statements. This may fit the description of not semidecidable, but it gives the impression there's no semialgorithm for testing satisfiability outside the scope of validity, which is clearly false or we would have no SMT solvers or independence proofs. Also, link rot for the cite.
Argh, I think I just made a mess of this article by mentioning satisfiability modulo theories. The problem is that the article about interpretations states that interpretations are interpretations of theories, but this isn't really the right idea, because for boolean sat, we have interpretations but not theories in this sense, viz not theory (mathematical logic). This inconsistency needs to be resolved across the set of inter-related articles. linas ( talk) 21:59, 13 June 2011 (UTC)
I strongly recommend my document; I cannot show to the world, but I have years studing the problem and NOW I got the solution: Maths are ambiguous, and we can create two TM; each philosophy can get us a different correct response to the question "NP=P?". And the question about if SAT is semidecidable can be read with an easy transformation (every boolean-fbf in SAT). I have to argue something more: the problem XOR-AND and OR-AND SAT are very different..., but those questions will give me hours and hours of explanations.
http://archive.org/details/TheUltimateDefinitionOfNp
I could be sure that there are more true and hidden demonstrations and false and famous in other hand than experts of the area. Please create a forum: my link show two easy demonstrations..., easier impossible. The demonstration NP is not P (in constructive philosophy) is got with diagonalization, and #P=P (in the infinitum philosophy) is very graphical with examples.
I got awful responses from editor in chief, saying nonsenses like "NP problem resolution is nothing with technology". Journals are DEAD and the Claymath Institute is a false institution too: so we cannot know if problems are solved or not.
The language on satisfiability is, again, vague. In general even satisfiability of a theory in propositional logic is not decidable, and similarly the satisfiability of a variable-free equational theory in the language with only $0$, $1$, $+$, and $=$ is not decidable. This is because the decision process can only look at a finite part of the theory before making a decision, and there could be an inconsistency in the part that was not looked at before the decision procedure halts. Thus the decision process will either say that some satisfiable theories are unsatisfiable, or it will say that some unsatisfiable theories are satisfiable. The only thing that can be decidable, in principle, is satisfiability of a sentence or the satisfiability of a finite set of sentences. The latter is equivalent to the former in many contexts.
On to unification. Unification is simply a deductive system for first-order logic. It is not any stronger or weaker than any other deductive system (natural deduction, Hilbert-style, etc.). All of these allow us to enumerate the provable consequences of a theory. None of them can be used to solve the satisfiability question in for theories, only for sentences in some limited circumstances. — Carl ( CBM · talk) 14:51, 16 June 2011 (UTC)
Are we arguing about something, or are we in violent agreement? I'm not claiming half of the things you seem to say I'm claiming, so I don't understand why this conversation is so argumentative. Honestly, I've never studied first-order logic, I do not possess any books that treat first-order logic as a subject of study; certainly Cohen's Universal algebra doesn't treat it as a topic, nor does the term-rewriting book, nor does Hodges' Model theory book. Yet all of these books touch on satisfiability and do so in a concrete fashion. If you believe that all of these different definitions of satisfiability are the same thing, that's fine. And you're almost surely right, and I think here we agree; at some informal level, I do understand that they're all the same. But the reality is that none of these authors felt compelled to define first-order logic before they could talk about satisfiability; the subject matter didn't call for it. Perhaps this article doesn't need to either; it may be a source of confusion to the student. Informally, we agree its all the same thing. Formally, I have no reference which states, in a formal fashion, that these varying definitions really are all the same thing. linas ( talk) 02:06, 18 June 2011 (UTC)
I don't think there is a difference between satifiability in universal algebra and satisfiability in first-order logic, and in fact the fundamentals of universal algebra are a subset of those of first-order logic. The only difference is that universal algebra uses slightly different terminology and then goes off in a different direction.
Although they historically did not always point it out in their publications, the connection is very well known to universal algebraists. You can ask User:Vaughan Pratt. (IIRC he thinks of himself primarily as a universal algebraist.) Or you can look in Chapter IX of the revised (1981) edition of Paul Cohen's Universal Algebra. Its title is Model theory and universal algebra, and it starts with Chang and Keisler's slogan "universal algebra + logic = model theory". Even the old edition had Chapter V, Relational structures and models, and Chapter VI, Axiomatic model classes. These three chapters are really about first-order model theory. Similarly, Grätzer's Universal Algebra used to end with Chapter 6 (Elements of model theory), Chapter 7 (Elementary properties of algebraic structures) and Chapter 8 (Free $\Sigma$-structures), all of which are about first-order model theory. (In the second (2008) edition there are new appendices which go in a different direction.)
What we need in this article is not a separate definition of satisfiability for universal algebra, but a brief explanation of how first-order satisfiability specialises to that important case. Hans Adler 00:42, 19 June 2011 (UTC)
Sigh. I'm pretty sure I never added text that implied it was decidable! Hey! I'm not an idiot! BTW, please note what finite model theory has to say about Goedel and completeness! I also didn't realize that reading books on lambda calc, term rewriting, model theory, and papers on SMT, answer-set programming was "focusing on one case"; I thought that this provided fairly broad coverage of the topic. I work for a chip-design company; yes, the hardware verification tools people have a vast number of constraint satisfaction problems (timing, routing, etc.) These are all "satisfiability" problems, and there's already a small universe of WP pages for these topics: e.g. model checking, local consistency, etc. Some of those pages (I skimmed them recently) link back to this article, or the article on structure (mathematical logic), or to model theory article. Many do not: e.g. local consistency which has three different sections discussing satisfiability, none linking here. Note also discussion of satisfiability in complexity of constraint satisfaction where the theory of relational databases mentioned. (somewhat off-topic, but note that SQL has very rigorous satisfiability demands; keystores became very popular recently precisely because they dump this, and do not require consistency. There's a recent interesting article that points out that keystores and SQL are adjoint, in the sense of monad (category theory). I wouldn't be half surprised if there's some paper somewhere that points out that consistency (in general) and satisfiability (in general) are adjoint in the same sense. But again, the point is that essentially none of these discussions read on or use "first-order logic" as a touchstone definition for satisfiability. linas ( talk) 03:33, 22 June 2011 (UTC)
The first section includes the claim:
"For logics without negation, such as the positive propositional calculus, the questions of validity and satisfiability may be unrelated. In the case of the positive propositional calculus, the satisfiability problem is trivial, as every formula is satisfiable, while the validity problem is co-NP complete."
This corresponds to a similar claim in the article on co-NP-complete (added by the same user). I've argued there that I believe this to be wrong; unless I'm mistaken, for a positive Boolean formula to be a tautology, it is necessary and sufficient for it to be true when all variables are false, and this is easily checked in polynomial time. (Of course, it could still be co-NP-complete, but then we would have P=NP, among other things – highly unlikely.) -- Mlhetland ( talk) 19:52, 27 January 2016 (UTC)
To address the "too technical" complaint in the lead, I attempted a rewrite which preserves the original content but uses more accessible language. Constructive feedback, improvements, or discussion welcome!
One subtlety is that, informally, one would typically refer to something like as unsatisfiable, when in reality it is satisfiable in FOL without additional axioms and only unsatisfiable over the usual theory of the integers (or at least a sufficient subset of the integer axioms). I used integer constraint examples to introduce satisfiability informally, but then provided the technical definition. If we want to avoid these issues, we could stick to propositional logic examples in the lead, even if that is a bit less intuitive. On the other hand, I am not sure if the lead should favor the purely logical meaning of the word "satisfiability" over the meaning modulo a theory, since this is an article about the concept of satisfiability in general.