Timeline for Survey of transformations related to the use of SAT solvers
Current License: CC BY-SA 2.5
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 7, 2011 at 0:12 | comment | added | Mikolas | @Anthony well you did say you are interested in the practical aspect :-) Anyhow, the existing mainstream solvers do not really differentiate between different types of SAT. In the past there has been some work on exploiting binary clauses, for instance. But the existing solvers just use DPLL+unit prop+clause learning. However, some of the preprocessors exploit the structure. But again, not really from the point of view of complexity th. classification. | |
| Apr 6, 2011 at 7:31 | comment | added | Anthony Labarre | I could not access it through your link, here's another one. At first glance, the paper seems quite interesting, but more focused on applications than what I am looking for. | |
| Apr 5, 2011 at 18:44 | history | answered | Mikolas | CC BY-SA 2.5 |