Sound Probabilistic #SAT with Projection

TL;DR

This paper introduces an improved sound probabilistic method for estimating the number of solutions of a boolean formula under projection, with applications in program analysis and security.

Contribution

The paper presents a novel technique for sound probabilistic model counting with projection, enhancing quantitative analysis of programs.

Findings

Effective probabilistic estimation of model counts under projection.

Application to security and resource consumption analysis.

Implementation demonstrates practical utility.

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.