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
To build ganak, issue:
sudo apt-get install libgmp-dev libmpfr-dev libmpc-dev
git clone https://github.com/meelgroup/ganak
mkdir build && cd build
cmake ..
make
For Mac, pass option cmake -DDOPCC=OFF ...
to cmake
To count, run:
cd build
./ganak myfile.cnf
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
p cnf 500 1
c ind 1 3 4 6 7 8 10 0
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 e.g. 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. Here, we only have 2**5*3
solutions however, since we ban -3,-4
solution from the tuple (3,4)
.
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}
}