Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
5th Global Conference on Artificial Intelligence
Sprache des Tagungstitel:
Englisch
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-