License:GPL Version 3
Version: 4
Date: 2016-06-09
Authors: Alexander Weigl <>,
Vladimir Klebanov <>,
Jörg D. Weisbarth

ApproxMC-p is a (δ, ϵ)-counter for models of propositional formulas with support for projection. In short, ApproxMC-p calculates an model count M for an propositional formula φ with projection on Δ, s.t. the confidence δ and the tolerance ϵ is maintained.

P((1 − ϵ)#(φ|Δ) ≤ M ≤ (1 + ϵ)#(φ|Δ)) ≥ 1 − δ


usage: [-h] [-c CONFIDENCE] [-t TOLERANCE]
                     [--seed INT] [-v] [--version]
                     [--sat-command SAT_COMMAND] [--request-dir REQUEST_DIR]

Getting Started

You can obtain ApproxMC-p(y) by cloning the repository:

$ git clone

or download the tarball:

$ wget
$ tar xf approxmc-py-4.tar.gz

Following further steps are needed:

  1. Ensure that scipy is installed -- for me:

    sudo dnf python3-scipy
  2. Ensure you have a bounded #SAT with projection installed, like clasp, sharpCDCL or an adapted version cryptominisat.

  3. Some adapters need xorblast, as a SAT-preprocessor for xor-clauses.

  4. Ensure, e.g. that and sharpCDCL executable, is on $PATH:

    export PATH=$PATH:/home/weigl/work/xorblast/
    export PATH=$PATH:/home/weigl/work/sharpCDCL/build
  5. Run using (formely known as

    ~/w/approxmc-py % ./ -vvvv \
         --sat-command 'adapters/ {maxcount} {file}' \

Have a lot of fun…


-h, --help shows an help message

-c CONFIDENCE, --confidence CONFIDENCE specifies the confidence (1 - δ). A higher confidence leads to multiple runs.

-t TOLERANCE, --tolerance TOLERANCE tolerance (ϵ) of the approximation. The smaller tolerance, the models need to be counted in one slice (less slices are make).

--sat-command SAT_COMMAND The command for invoking a bounded #SAT tool. You can place {maxcount} and {filename} as the placeholder for values. Example:

--sat-command './adapters/ {maxcount} {filename}'

--request-dir REQUEST_DIR directory to save the generated DIMACS files, that are given to the bounded #SAT solvers

--seed INT set the seed for the internal PRNG, that is used to shuffle the xor constraints.

-v, --verbose increase output verbosity

--version print version information

--lower_bound LOWER_BOUND lower bound on the number of model

--sat-timeout SAT_TIMEOUT timeout in seconds for cryptominisat2 calls
(currently not supported)


ApproxMC-p is able to use different bounded #SAT solvers. Several adapters for different #SAT solvers are provided with ApproxMC-p (Folder adapters/).

An adapter needs to fulfill the following protocol:

  1. The adapter takes to parameters - maxcount -- the maximal number of models to find - filename -- the path to the DIMACS file, containing XOR clauses
  2. The adapter returns a 0 exit level on success and prints the number of counted models at last.


If you cite ApproxMC-py, then please reference the following publication:

Vladimir Klebanov, Alexander Weigl and Jörg Weibarth.
Sound Probabilistic #SAT with Projection.

If you have any question, feel free to contact us.