Sound Probabilistic #SAT with Projection

Abstract

We present an improved method for a sound probabilistic estimation of the model count of a boolean formula under projection. The problem solved can be used to encode a variety of quantitative program analyses, such as concerning security of resource consumption. We implement the technique and discuss its application to quantifying information flow in programs.

In Proceedings QAPL'16, arXiv:1610.07696

References in corpus (3)

• Balancing Scalability and Uniformity in SAT Witness Generator
• Uniform Solution Sampling Using a Constraint Solver As an Oracle
• Sampling Techniques for Boolean Satisfiability

Cited by in corpus (1)

• Bit-Vector Model Counting using Statistical Estimation