Timeline for An easy case of SAT that is not easy for tree resolution
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 30, 2013 at 7:56 | vote | accept | Jan Johannsen | ||
| Jun 27, 2013 at 20:30 | comment | added | vzn | @mikolas as I understand the question, if satisfiable/unsatisfiable instances of the family can be recognized in P time, but it is hard for tree or DAG resolution, that is what is sought. now am not sure this is pointed out in any papers, but afaik (anyone know more?), PHP sat/unsat instances can be recognized in P time. | |
| Jun 27, 2013 at 18:54 | history | edited | András Salamon | CC BY-SA 3.0 |
add citation
|
| Jun 26, 2013 at 14:38 | history | edited | András Salamon | CC BY-SA 3.0 |
add Cook
|
| Jun 26, 2013 at 14:03 | comment | added | Mikolas | I meant that if I have some result about all-different constraints, then it's not clear how this result translates to CNF. As I understand the questions, Jan wanted CNFs hard for tree-res but easy for something else (eg. dag-res). It's not clear to me also why PHP would be an example for this because PHP is exponential for dag-res as well. (BTW the referenced thesis looks neat!) | |
| Jun 26, 2013 at 13:52 | comment | added | András Salamon | @Mikolas: could you clarify what it is you are concerned about? | |
| Jun 26, 2013 at 12:53 | comment | added | Mikolas | Not sure if that's what Jan is looking for as he asks specifically for CNF. | |
| Jun 26, 2013 at 9:43 | history | answered | András Salamon | CC BY-SA 3.0 |