Abstract
We give a deterministic #SAT algorithm for de Morgan formulas of size up to n 2.63, which runs in time TeX . This improves upon the deterministic #SAT algorithm of [3], which has similar running time but works only for formulas of size less than n 2.5.
Our new algorithm is based on the shrinkage of de Morgan formulas under random restrictions, shown by Paterson and Zwick [12]. We prove a concentrated and constructive version of their shrinkage result. Namely, we give a deterministic polynomial-time algorithm that selects variables in a given de Morgan formula so that, with high probability over the random assignments to the chosen variables, the original formula shrinks in size, when simplified using a deterministic polynomial-time formula-simplification algorithm.
Our new algorithm is based on the shrinkage of de Morgan formulas under random restrictions, shown by Paterson and Zwick [12]. We prove a concentrated and constructive version of their shrinkage result. Namely, we give a deterministic polynomial-time algorithm that selects variables in a given de Morgan formula so that, with high probability over the random assignments to the chosen variables, the original formula shrinks in size, when simplified using a deterministic polynomial-time formula-simplification algorithm.
| Original language | English |
|---|---|
| Title of host publication | Mathematical Foundations of Computer Science 2014 |
| Subtitle of host publication | 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part II |
| Publisher | Springer Berlin Heidelberg |
| Pages | 165-176 |
| Number of pages | 12 |
| Volume | 8635 |
| ISBN (Electronic) | 978-3-662-44465-8 |
| ISBN (Print) | 978-3-662-44464-1 |
| DOIs | |
| Publication status | Published - 2014 |