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
.
To read more about technical algorithms in Ganak, please refer to our paper
build MIS from here and add mis.py
, muser2
and togmus
to build
directory.
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 ../bin/ganak.py .
You can run GANAK by using 'ganak.py' Python script. A simple invocation looks as follows:
python3 ganak.py <cnffile>
The usage instructions and default values to arguments can be found by running:
python3 ganak.py -h
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.
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])