Four Flavors of Entailment for Projected Model Counting
Sprache des Vortragstitels:
Workshop on Model Counting (MCW 2020@SAT)
Sprache des Tagungstitel:
Based on our work accepted at SAT?20, we present a novel approach for enumerating partial models of a propositional formula, inspired by how the theory and SAT solvers interact in lazy SMT. Using various forms of dual reasoning allows our CDCL-based algorithm to enumerate partial models without exploring and shrinking full models. Chronological backtracking renders the use of blocking clauses obsolete. Our focus is on projected model enumeration without repetition, hence adapting it to support projected model counting is straightforward. In this presentation-only talk, we introduce the key ideas with focus on the formalization.