Timeline for Satisfiability of general Boolean formulas with at most two occurrences per variable
Current License: CC BY-SA 2.5
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 22, 2009 at 1:21 | comment | added | Ryan Williams | Interesting... note we can throw in the "duals" of (2) and (3) as well: if the paths to the LCA of x and NOT(x) are all ORs, then we can replace the subtree with 1; if one path to the LCA is only ORs, we might as well set the literal to make that OR true. Now I do not know if it's always satisfiable otherwise... | |
| Dec 22, 2009 at 1:01 | history | edited | David Eppstein | CC BY-SA 2.5 |
added 376 characters in body; added 33 characters in body
|
| Dec 22, 2009 at 0:59 | comment | added | Reid Barton | By similar logic to (1), in the case where each variable appears only once, the formula is always satisfiable. | |
| Dec 22, 2009 at 0:56 | comment | added | Ryan Williams | I was aware of points (1) and (2), but neglected to point them out. They should probably be present in any prospective algorithm. As for your question, what about the formula "(x1 OR x2) AND NOT(x1) AND NOT(x2)"? | |
| Dec 22, 2009 at 0:49 | history | undeleted | David Eppstein | ||
| Dec 22, 2009 at 0:49 | history | edited | David Eppstein | CC BY-SA 2.5 |
added 328 characters in body
|
| Dec 22, 2009 at 0:15 | history | deleted | David Eppstein | ||
| Dec 22, 2009 at 0:14 | history | answered | David Eppstein | CC BY-SA 2.5 |