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

1. We released a new tool SymGanak, which exploits the inherent symmetry exhibited in combinatorial problems for component-caching in ganak to achieve significant performance gains. Please checkout to symganak branch for more details.
2. We added a support for Weighted Model Counting: Please checkout to wmc branch for more details.
3. We replaced MIS with arjun to calculate minimal independent set for IS heuristic as arjun is more performant than MIS.

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])