Boosting Definability Bipartition Computation Using SAT Witnesses

Bipartitioning the set of variables Var (Sigma) of a propositional formula Sigma w.r.t. definability consists in pointing out a bipartition < I, O > of Var (Sigma) such that S defines the variables of O (outputs) in terms of the variables in I (inputs), i.e., for every o is an element of O, there exists a formula Phi(o) over I such that o double left right arrow Phi(o) is a logical consequence of Sigma. The existence of Phi(o) given o, I, and Sigma is a coNP-complete problem, and as such, it can be addressed in practice using a SAT solver. From a computational perspective, definability bipartitioning has been shown as a valuable pre-processing technique for model counting, a key task for a number of AI problems involving probabilities. To maximize the benefits offered by such a preprocessing, one is interested in deriving subset-minimal bipartitions in terms of input variables, i.e., definability bipartitions < I, O > such that for every i is an element of I, < I \ {i}, O boolean OR {i}> is not a definability bipartition. We show how the computation of subset-minimal bipartitions can be boosted by leveraging not only the decisions furnished by SAT solvers (as done in previous approaches), but also the SAT witnesses (models and cores) justifying those decisions.