Closing the Gap Between Short and Long XORs for Model Counting

Authors

  • Shengjia Zhao Tsinghua University
  • Sorathan Chaturapruek Stanford University
  • Ashish Sabharwal Allen Institute for AI
  • Stefano Ermon Stanford University

DOI:

https://doi.org/10.1609/aaai.v30i1.10430

Keywords:

Model Counting, Randomized Hashing, SAT

Abstract

Many recent algorithms for approximate model counting are based on a reduction to combinatorial searches over random subsets of the space defined by parity or XOR constraints. Long parity constraints (involving many variables) provide strong theoretical guarantees but are computationally difficult. Short parity constraints are easier to solve but have weaker statistical properties. It is currently not known how long these parity constraints need to be. We close the gap by providing matching necessary and sufficient conditions on the required asymptotic length of the parity constraints. Further, we provide a new family of lower bounds and the first non-trivial upper bounds on the model count that are valid for arbitrarily short XORs. We empirically demonstrate the effectiveness of these bounds on model counting benchmarks and in a Satisfiability Modulo Theory (SMT) application motivated by the analysis of contingency tables in statistics.

Downloads

Published

2016-03-05

How to Cite

Zhao, S., Chaturapruek, S., Sabharwal, A., & Ermon, S. (2016). Closing the Gap Between Short and Long XORs for Model Counting. Proceedings of the AAAI Conference on Artificial Intelligence, 30(1). https://doi.org/10.1609/aaai.v30i1.10430

Issue

Section

Technical Papers: Reasoning under Uncertainty