Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
We offer a new understanding of some aspects of practical SAT-solvers that are based on DPLL with unit-clause propagation, clause-learning, and restarts. We do so by analyzing a concrete algorithm which we claim is faithful to what practical solvers do. In particular, before making any new decision or restart, the solver repeatedly applies the unit-resolution rule until saturation, and leaves no component to the mercy of non-determinism except for some internal randomness. We prove the perhaps surprising fact that, although the solver is not explicitly designed for it, with high probability it ends up behaving as width-k resolution after no more than O(n^2k+2) conflicts and restarts, where n is the number of variables. In other words, width-k resolution can be thought of as O(n^2k+2) restarts of the unit-resolution rule with learning.
Code (0)
등록된 구현이 없습니다.
Tasks
2kSimilar Papers 제목 키워드 기반
Solving MaxSAT and #SAT on structured CNF formulas
In this paper we propose a structural parameter of CNF formulas and use it to identify instances of weighted MaxSAT and #SAT that can be solved in polynomial time. Given a CNF formula we say that a set of clauses is prec…
Relating Complexity-theoretic Parameters with SAT Solver Performance
Over the years complexity theorists have proposed many structural parameters to explain the surprising efficiency of conflict-driven clause-learning (CDCL) SAT solvers on a wide variety of large industrial Boolean instan…
Subsumption-driven clause learning with DPLL+restarts
We propose to use a DPLL+restart to solve SAT instances by successive simplifications based on the production of clauses that subsume the initial clauses. We show that this approach allows the refutation of pebbling form…
The Algorithmic Phase Transition of Random $k$-SAT for Low Degree Polynomials
Let $\Phi$ be a uniformly random $k$-SAT formula with $n$ variables and $m$ clauses. We study the algorithmic task of finding a satisfying assignment of $\Phi$. It is known that satisfying assignments exist with high pro…
Advancing Lazy-Grounding ASP Solving Techniques -- Restarts, Phase Saving, Heuristics, and More
Answer-Set Programming (ASP) is a powerful and expressive knowledge representation paradigm with a significant number of applications in logic-based AI. The traditional ground-and-solve approach, however, requires ASP pr…