| Abstract: |
Modern SAT solvers can be broadly classified into two categories. The first category comprises solvers based on the DPLL (DavisPutnam-Logemann-Loveland) paradigm, which has achieved remarkable success with the combination of heuristics such as conflict-driven clause learning (CDCL) and restart mechanism. The second category consists of solvers employing the stochastic local search (SLS) approach, with Walksat being a prominent example. In this paper, we demonstrate that these two types of solvers can be distinguished by their performance on Tseitin formulas which have been extensively studied in proof complexity. Specifically, we show that Walksat can efficiently find a satisfying assignment for any satisfiable Tseitin formula with high probability in polynomial time. In contrast, we construct a family of Tseitin formulas on which any DPLL-based solver, even when enhanced with restarts, requires exponential time to find a solution. This analysis reveals a clear limitation of DPLL-based solvers compared to Walksat and suggests a potential direction for their improvements. |
下载中心
会议室预定
电子邮箱