Timeline for Is SAT a context-free language?
Current License: CC BY-SA 3.0
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 23, 2017 at 7:17 | comment | added | Aryeh | Actually, I'm quite confident that it works. The derivation tree necessarily has bounded out-degree, meaning that to generate a substring of sufficient length, you need some minimal height -- and that immediately allows for a pidgeonhole argument. | |
| Jan 22, 2017 at 21:14 | comment | added | mak | Yes, something like this could work, but it might end up being somewhat more complicated than the argument given by Marzio De Biasi here so maybe not worth the effort. Thanks for the quick answer and the discussion. | |
| Jan 21, 2017 at 22:49 | comment | added | Aryeh | OK, I see the problem -- I was implicitly assuming that $|xyz|$ can be bounded in length (as in the classic pumping lemma), while also being able to specify something about its location in the string. I think the argument can be fixed by re-doing the pumping lemma from scratch. We'll make that first variable a really long sequence of 1's -- long enough that some sub-tree generating a contiguous substring of those 1's has to be sufficiently deep for the pidgeonhole principle to apply. | |
| Jan 21, 2017 at 21:42 | comment | added | mak | p would be 3 here (to make the illustration short), but the example is meant to be generic. I am using binary numbers rather than decimal ones, and I am (as it was easier to write) requiring that all other variables are mapped to false rather than just the ones with a "1" in them. | |
| Jan 21, 2017 at 21:28 | comment | added | Aryeh | what is the value of p in your example? | |
| Jan 21, 2017 at 20:56 | comment | added | mak | Item 2 (referring to the Wikipedia page) is always true if you only mark p positions in total, so this can't help much. Item 1 only requires that 1 marked position is pumped, but does not restrict how much of the unmarked string can be in xy. It seems to me that you could (un)pump, e.g., "(111)(~0)(~1)...(~110)" by picking u="(11", x="1", y="", z=")(~0)...(~110" and v=")", so as to obtain "(11)", which is satisfiable. | |
| Jan 21, 2017 at 19:17 | comment | added | Aryeh | I think my application of Ogden's Lemma works, even if I may be off by a constant here or there. I mark only the contiguous stretch of 1s in the first variable of the formula. Ogden's lemma (items 1 and 2) force the pumped region to be limited to this contiguous stretch. Hence, any negative pumping will create unsatisfiable formulae. | |
| Jan 20, 2017 at 15:35 | comment | added | mak | I do not follow your argument here. Ogden's Lemma allows any of the strings to have any amount of unmarked positions, so negative pumping does not affect only the marked positions. | |
| Jan 19, 2017 at 10:19 | comment | added | Aryeh | The negative pumping only affects the string $1^p$ -- because of the way I've placed the marks, as per Ogden's lemma. So while I cannot ensure that a positive pumping will create an unsatisfiable assignment, I can certainly ensure that a negative one will -- since it will create litterals indexed by $1^q$, where $q<p$. | |
| Jan 19, 2017 at 10:12 | comment | added | mak | I do not understand yet how your argument would ensure that the negative pumping does not also remove the parts of the formula that you need to ensure unsatisfiability of any positive unit clause other than $x_N$. Can you elaborate? | |
| Jan 18, 2017 at 9:45 | comment | added | Aryeh | @mak I edited the answer to reflect your observation. | |
| Jan 18, 2017 at 9:44 | history | edited | Aryeh | CC BY-SA 3.0 |
added 44 characters in body
|
| Jan 18, 2017 at 9:23 | comment | added | Emil Jeřábek | Even with arbitrary non-CNF formulas in finitely many variables, satisfiability (and any language that cannot distinguish two logically equivalent formulas for that matter) is easily seen to be context-free. However, I fail to see the relevance of this. Satisfiability of formulas in finitely many varibles is a trivial problem that has nothing to do with the complexity of SAT. | |
| Jan 17, 2017 at 23:20 | comment | added | mak | The claim with regularity only works for CNFSAT (I added a clarification to my question). | |
| Jan 17, 2017 at 22:09 | history | edited | Aryeh | CC BY-SA 3.0 |
clarified which variable $1^p$ represents
|
| Jan 17, 2017 at 17:57 | comment | added | Aryeh | ... But I think the language is still regular, because one takes the finite collection of "essentially distinct" (i.e., without trivial repetitions) formulae and then allows the various repetitions. | |
| Jan 17, 2017 at 17:56 | comment | added | Aryeh | Note: In my claim that for a finite number of variables the language is finite, I am implicitly disallowing repeating a variable within a clause or a clause unboundedly many times | |
| Jan 17, 2017 at 17:13 | history | edited | user6973 | CC BY-SA 3.0 |
fixed broken link
|
| Jan 17, 2017 at 17:03 | history | answered | Aryeh | CC BY-SA 3.0 |