GANAK takes in a CNF formula F
and a confidence delta
as input and returns count
such that count
is the number of solutions of F
with confidence at least 1 - delta
. GANAK supports projected model counting (see below).
To read more about technical algorithms in Ganak, please refer to our paper
- Support Added for Weighted Model Counting: Please checkout to wmc branch.
- Replaced MIS with arjun to calculate minimal independent set for IS heuristic.
To build ganak, issue:
bash
sudo apt-get install libgmp-dev
sudo apt-get install libmpfr-dev
sudo apt-get install libmpc-dev
mkdir build && cd build
cmake ..
make
cp ganak ../bin/
You can use the run_ganak.sh script in scripts directory to run ganak. A simple invocation looks as follows:
./run_ganak.sh <cnffile>
To use different settings of parameters modify the helper run_ganak.sh script. The usage instructions and default values to parameters can be found by running:
../bin/ganak
For some applications, one is not interested in solutions over all the variables and instead interested in counting the number of unique solutions to a subset of variables, called sampling set. GANAK allows you to specify the sampling set using the following modified version of DIMACS format:
$ cat myfile.cnf
c ind 1 3 4 6 7 8 10 0
p cnf 500 1
3 4 0
Above, using the c ind
line, we declare that only variables 1, 3, 4, 6, 7, 8 and 10 form part of the sampling set out of the CNF's 500 variables 1,2...500
. This line must end with a 0. The solution that GANAK will be giving is essentially answering the question: how many different combination of settings to this variables are there that satisfy this problem? Naturally, if your sampling set only contains 7 variables, then the maximum number of solutions can only be at most 2^7 = 128. This is true even if your CNF has thousands of variables.
Note: By default if sampling set is present ganak will do projected model counting, to turn off projected model counting use the -noPMC flag.
Few toy benchmarks are given in benchmarks directory. Full list of benchmarks used for our experiments is available here
Please click on "issues" at the top and create a new issue. All issues are responded to promptly.
@inproceedings{SRSM19,
title={GANAK: A Scalable Probabilistic Exact Model Counter},
author={Sharma, Shubham and Roy, Subhajit and Soos, Mate and Meel, Kuldeep S.},
booktitle={Proceedings of International Joint Conference on Artificial Intelligence (IJCAI)},
month={8},
year={2019}
}
- Shubham Sharma ([email protected])
- Mate Soos ([email protected])
- Subhajit Roy ([email protected])
- Kuldeep Meel ([email protected])