Talk:Satisfiability

Combine this Page with "Boolean satisfiability problem"

This page addresses the same topic, but in much less detail. Suggest merging this page into "Boolean satisfiability problem" by making it the introduction.

I would object strongly to that. This should be the main article, and boolean satisfiability should be a supporting page of this one, not vise versa. Satisfiability is a more general concept than just its boolean/propositional aspect.Greg Bard 21:31, 5 March 2010 (UTC)

Unfinished

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)

My fault. I had started to write this sentence, and then decided to add the Reduction of validity to satisfiability section instead, which rendered what I was going to say redudnant. I've deleted it now. — Charles Stewart (talk) 09:45, 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)

Requested move

The following discussion is an archived discussion of a requested move. Please do not modify it. Subsequent comments should be made in a new section on the talk page. No further edits should be made to this section.

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)

• Support: Satisfiability seems to be the main subject. Validity has its own article with a slightly different meaning, but there is already a link here.--RDBury (talk) 23:57, 8 March 2010 (UTC)

The above discussion is preserved as an archive of a requested move. Please do not modify it. Subsequent comments should be made in a new section on this talk page. No further edits should be made to this section.

satisfiability *is not* a semi-decidable problem for FOL

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)

satisfiablity, theories, etc.

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)

Satisfiability

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)

I've got to run, so can't do anything reasoned for about 12-24 hours. My quick take is that although satisfiability is a topic that is related to first-order logic, it is, in fact, used in many other places as well. So, for example: its important in term-rewriting, but in term re-writing, there are no predicates, no logical connectives, no quantifiers, no concept of true/false; yet satsifiability is closely defined, and algorithms to determine it are developed. So the trick for this article is to have a broad definition that fulfills the general need, and then break it down to that needed by the various different branches. linas (talk) 22:53, 16 June 2011 (UTC)

There is certainly the "=" predicate, and if you chase the definitions in "Term Rewriting and All That" they do refer to truth in the sense of model theory and first-order logic. For example, definitions 3.5.1 and 3.5.3 define the relation $\approx _{E}$ in terms of the model-theoretic satisfaction relation $\vDash$, and the definition of "satisfiable" on page 58 is in terms of substitution (which is a model-theoretic concept) and the $\approx _{E}$ relation. I don't have a copy of the book; I requested it from the library, so I should be able to look at it in more detail in a few days. So far I am limited to preview in google books. — Carl (CBM · talk) 00:45, 17 June 2011 (UTC)

Sorry; not to mis-lead. Of course, one can't do math with using equals signs at some point; and yes, chap 3 does review models in a more-or-less standard sense. As to whether "=" is a predicate or not is debatable. In an informal, vague sense, of course it is. However, in the formal sense, the language (or 'signature') of a term algebra does not contain predicate symbols, or atomic symbols or sentences or connectives. Informally, of course, these are casually used through-out the text to discuss results and to make claims; they just are not placed/used/defined as symbols of the objects under study. Nonetheless, one can still ask questions such as "if I have these two terms, arising from some signature S, under what cases are they equal?" which is a satisfiability problem, even though S is not (the signature of) a predicate logic, or any other kind of logic. linas (talk) 14:30, 17 June 2011 (UTC)

I think you are thinking of the special case of first-order logic in which the are no predicate symbols other than "=", and where people only look at atomic formulas, which are always of the form $t_{1}=t_{2}$. This is how universal algebra is usually done, anyway: it is a special case of first-order logic, which is why model theory and universal algebra are so closely connected.

The definition of "satisfiability of an equation" in the setting of universal algebra seems to be exactly the same as the definition of satisfiability of the equation in first-order logic: is there a structure in which the two terms are equal? In the context of univseral algebra these structures are commonly called "groups", "rings", etc. but they are simply structures from the point of view of logic. — Carl (CBM · talk) 14:48, 17 June 2011 (UTC)

When you say "universal algebra is usually done as a special case of first-order logic", I will strongly argue that. I've got a book, title "Universal Algebra", Paul Cohen, and I'm pretty sure the words "first order logic" or "predicate logic" never appear anywhere in the book. At some level, yes, the one topic may be considered to be a subset of the other topic, but, in general, a narrower topic will have results and theorems that do not apply to the broader topic. When you say "seems to be the same as", I think its a mistake to try to be all fuzzy-wuzzy about definitions; I think the right approach is to give precise definitions suitable for the subfield, while having an informal intro/overview that does the hand-waving, pointing out that they're all the same, more or less.

Anyway, I propose creating a new subsection of this article, viz 'satisfiability in universal algebra' and moving the mention of unification etc. to that section. Thus it would closely resemble the first few pages of chapter 4 of the book 'term rewriting'. I believe that this should fix all your objections.linas (talk) 15:04, 17 June 2011 (UTC)

When Term rewriting says "class of algebras" that is exactly the same thing as when a person in first-order logic says "class of models", because an "algebra" in universal algebra is the same as a "model" or "structure" in first-order logic for the same signature. Thus, for example, Def. 3.2.1 in Term rewriting is exactly the definition of structure (mathematical logic) for a signature that has no predicate symbols other than =. If you are claiming there is a difference between satisfiability in universal algebra and satisfaction in first-order logic, can you say exactly what it is? I will have a copy of Term algebra here in a couple days that I can look at in more detail, I am a little limited by google books at the moment. — Carl (CBM · talk) 16:19, 17 June 2011 (UTC)