On computing minimal independent support and its applications to sampling and counting

Alexander Ivrii, Sharad Malik, Kuldeep S. Meel, Moshe Y. Vardi

Research output: Contribution to journalArticle

21 Scopus citations

Abstract

Constrained sampling and counting are two fundamental problems arising in domains ranging from artificial intelligence and security, to hardware and software testing. Recent approaches to approximate solutions for these problems rely on employing SAT solvers and universal hash functions that are typically encoded as XOR constraints of length n/2 for an input formula with n variables. As the runtime performance of SAT solvers heavily depends on the length of XOR constraints, recent research effort has been focused on reduction of length of XOR constraints. Consequently, a notion of Independent Support was proposed, and it was shown that constructing XORs over independent support (if known) can lead to a significant reduction in the length of XOR constraints without losing the theoretical guarantees of sampling and counting algorithms. In this paper, we present the first algorithmic procedure (and a corresponding tool, called MIS) to determine minimal independent support for a given CNF formula by employing a reduction to group minimal unsatisfiable subsets (GMUS). By utilizing minimal independent supports computed by MIS, we provide new tighter bounds on the length of XOR constraints for constrained counting and sampling. Furthermore, the universal hash functions constructed from independent supports computed by MIS provide two to three orders of magnitude performance improvement in state-of-the-art constrained sampling and counting tools, while still retaining theoretical guarantees.

Original languageEnglish (US)
Pages (from-to)41-58
Number of pages18
JournalConstraints
Volume21
Issue number1
DOIs
StatePublished - Jan 1 2016

All Science Journal Classification (ASJC) codes

  • Software
  • Discrete Mathematics and Combinatorics
  • Computational Theory and Mathematics
  • Artificial Intelligence

Keywords

  • Independent support
  • Model counting
  • SAT sampling

Fingerprint Dive into the research topics of 'On computing minimal independent support and its applications to sampling and counting'. Together they form a unique fingerprint.

  • Cite this