Bit-vector model counting using statistical estimation

Seonmo Kim, Stephen McCamant

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

Approximate model counting for bit-vector SMT formulas (generalizing #SAT) has many applications such as probabilistic inference and quantitative information-flow security, but it is computationally difficult. Adding random parity constraints (XOR streamlining) and then checking satisfiability is an effective approximation technique, but it requires a prior hypothesis about the model count to produce useful results. We propose an approach inspired by statistical estimation to continually refine a probabilistic estimate of the model count for a formula, so that each XOR-streamlined query yields as much information as possible. We implement this approach, with an approximate probability model, as a wrapper around an off-the-shelf SMT solver or SAT solver. Experimental results show that the implementation is faster than the most similar previous approaches which used simpler refinement strategies. The technique also lets us model count formulas over floating-point constraints, which we demonstrate with an application to a vulnerability in differential privacy mechanisms.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
EditorsDirk Beyer, Marieke Huisman
PublisherSpringer Verlag
Pages133-151
Number of pages19
ISBN (Print)9783319899596
DOIs
StatePublished - 2018
Event24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 - Thessaloniki, Greece
Duration: Apr 14 2018Apr 20 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10805 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
CountryGreece
CityThessaloniki
Period4/14/184/20/18

Keywords

  • #SAT
  • Bit-vectors
  • Floating point
  • Model counting
  • Randomized algorithms

Fingerprint Dive into the research topics of 'Bit-vector model counting using statistical estimation'. Together they form a unique fingerprint.

  • Cite this

    Kim, S., & McCamant, S. (2018). Bit-vector model counting using statistical estimation. In D. Beyer, & M. Huisman (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (pp. 133-151). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10805 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-89960-2_8