Four Flavors of Entailment for Projected Model Counting

Description

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.

Period	09 Jul 2020
Event title	Workshop on Model Counting (MCW 2020@SAT)
Event type	Conference
Location	AustriaShow on map