Name
Abstract | ||
|---|---|---|
A fruitful connection between algorithm design and proof complexity is the formalization of the DPLL approach to satisfiability testing in terms of tree-like resolution proofs. We consider extensions of the DPLL approach that add some version of memoization, remembering formulas the algorithm has previously shown unsatisfiable. Various versions of such formula caching algorithms have been suggested for satisfiability and stochastic satisfiability (S. M. Majercik et al., 1998; F. Bacchus et al., 2003). We formalize this method, and characterize the strength of various versions in terms of proof systems. These proof systems seem to be both new and simple, and have a rich structure. We compare their strength to several studied proof systems: tree-like resolution, regular resolution, general resolution, and Res(k). We give both simulations and separations. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1109/CCC.2003.1214425 | IEEE Conference on Computational Complexity |
Keywords | Field | DocType |
backtracking,cache storage,computability,computational complexity,formal specification,symbol manipulation,theorem proving,trees (mathematics),DPLL approach,algorithm design,backtracking,formula caching proof system,memoization,proof complexity,proof system formalization,regular resolution,stochastic satisfiability,tree-like resolution proof | Discrete mathematics,Computer science,Automated theorem proving,Satisfiability,Algorithm,Computability,Theoretical computer science,Mathematical proof,DPLL algorithm,Proof complexity,Memoization,Computational complexity theory | Conference |
ISSN | ISBN | Citations |
1093-0159 | 0-7695-1879-6 | 20 |
PageRank | References | Authors |
1.68 | 18 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paul Beame | 1 | 2234 | 176.07 |
| Russell Impagliazzo | 2 | 5444 | 482.13 |
| Toniann Pitassi | 3 | 2282 | 155.18 |
| Nathan Segerlind | 4 | 223 | 11.22 |