Sibylle Möhle, Armin Biere,
"Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting"
, in Diego Calvanese, Luca Iocchi: 5th Global Conference on Artificial Intelligence, Serie EasyChair EPiC series in Computing, 2019
Original Titel:
Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting
Sprache des Titels:
Englisch
Original Buchtitel:
5th Global Conference on Artificial Intelligence
Original Kurzfassung:
In propositional model counting, also named #SAT, the search space needs to be explored exhaustively, in contrast to SAT, where the task is to determine whether a propositional formula is satisfiable. While state-of-the-art SAT solvers are based on non-chronological backtracking, it has also been shown that backtracking chronologically does not significantly degrade solver performance. Hence investigating the combination of chronological backtracking with conflict-driven clause learning (CDCL) for #SAT seems evident. We present a calculus for #SAT combining chronological backtracking with CDCL and provide a formal proof of its correctness.
Forschungs-