Name
Abstract | ||
|---|---|---|
An important extension of satisfiability testing is model-counting, a task that corresponds to problems such as probabilistic reasoning and computing the permanent of a Boolean matrix. We recently introduced Cachet, an exact model-counting algorithm that combines formula caching, clause learning, and component analysis. This paper reports on experiments with various techniques for improving the performance of Cachet, including component-selection strategies, variable-selection branching heuristics, randomization, backtracking schemes, and cross-component implications. The result of this work is a highly-tuned version of Cachet, the first (and currently, only) system able to exactly determine the marginal probabilities of variables in random 3-SAT formulas with 150+ variables. We use this to discover an interesting property of random formulas that does not seem to have been previously observed. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11499107_17 | SAT |
Keywords | Field | DocType |
backtracking scheme,random formula,clause learning,cross-component implication,component-selection strategy,fast exact model counting,formula caching,boolean matrix,component analysis,3-sat formula,exact model-counting algorithm,variable selection,satisfiability,probabilistic reasoning | Discrete mathematics,Constraint satisfaction,Random variable,Combinatorics,Logical matrix,Computer science,Satisfiability,Algorithm,Heuristics,Probabilistic logic,Backtracking,Marginal distribution | Conference |
Volume | ISSN | ISBN |
3569 | 0302-9743 | 3-540-26276-8 |
Citations | PageRank | References |
44 | 1.88 | 14 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tian Sang | 1 | 231 | 9.69 |
| Paul Beame | 2 | 2234 | 176.07 |
| Henry A. Kautz | 3 | 9271 | 1010.27 |