ApproxMC-p(y)

License:GPL Version 3
Version: 4
Download:http://gitlab.com/QIF/approxmc-py
Date: 2016-06-09
Authors: Alexander Weigl <weigl@kit.edu>,
Vladimir Klebanov <klebanov@kit.edu>,
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 − δ

Synopsis

usage: approxmc-p.py [-h] [-c CONFIDENCE] [-t TOLERANCE]
                     [--seed INT] [-v] [--version]
                     [--sat-command SAT_COMMAND] [--request-dir REQUEST_DIR]
                     DIMACS-FILE

Getting Started

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

$ git clone https://gitlab.com/QIF/approxmc-py

or download the tarball:

$ wget http://formal.iti.kit.edu/approxmc-py/approxmc-py-4.tar.gz
$ 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 xorblast.py and sharpCDCL executable, is on $PATH:

    export PATH=$PATH:/home/weigl/work/xorblast/
export PATH=$PATH:/home/weigl/work/sharpCDCL/build

  5. Run using approxmc-p.py (formely known as run.py):

    ~/w/approxmc-py % ./approxmc-p.py -vvvv \
     --sat-command 'adapters/sharpCDCL.sh {maxcount} {file}' \
     ~/work/qif-sat/case_study_crc/logs_2/1452259749/crc32_8_0x04C11DB7.pp.cnf

Have a lot of fun…

Arguments

-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/sharpCDCL.sh {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)

Adapters

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.

Citing

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

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

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

Changelog

Generated on: 2016-08-03.