Ganak is a state-of-the art model counter that won all available awards at the 2024 and 2025 Model Counting Competitions. It can count over any field, including but not limited to integers, rationals, complex numbers, integers modulo prime, and polynomials over a finite field.
It can run in probabilistic mode (default), non-probabilistic mode (--prob 0),
and approximate counting mode (--appmct <timeout>), where it switches to
ApproxMC after a predetermined timeout.
To read more about Ganak-specific ideas, refer to our newer paper, and our older paper. You can also check out our presentation PDF here. Note that Ganak employs many ideas by many people. See AUTHORS for a list.
You can use Ganak online, straight from your browser
Use of the release binaries is strongly encouraged, as Ganak requires a specific set of libraries to be installed. The second best thing to use is Nix. Simply install nix and then:
nix shell github:meelgroup/ganakThen you will have ganak binary available and ready to use.
If this is somehow not what you want, you can also build it. See the GitHub Action for the specific set of steps.
Ganak takes a CNF in a special, DIMACS-like format as specified by the model counting competition guidelines. Basically, the format is as follows:
c t pwmc
p cnf 3 2
c p weight 1 0.3 0
c p weight -1 0.8 0
1 2 3 0
-1 2 0
c p show 1 2 0
The first line says it's a projected weighted model counting instance. The second line says it has 3 variables and 2 clauses. The third and fourth lines specify the weights of the variables 1. The weight of the literal 1 is 0.3 and the weight of the literal -1 is 0.8. The weight of all unspecified variables is 1 for both positive and negative literals.
The last line says that the projection set of the counter is only variables 1 and 2. If no projection set is given, then the counter does an unprojected count, i.e. all variables are assumed to be in the projection set.
Beware to ALWAYS give the weight of both the literal and its negation or different counters may give different results.
It is highly encouraged to give both the positive and the negative literal's
weight, e.g. 1 and -1:
c p weight 1 0.3 0
c p weight -1 0.8 0
This is important because different counters have different defaults, so in order to have consistent results, you should must specify the weights of both the positive and the negative literals.
There are many different ways you can specify the weights, the following are all valid:
c p weight 1 1/4 0
c p weight -1 3e-5 0
c p weight 2 -9 0
c p weight -2 -3.4e5 0
Notice that in --mode 1 Ganak will give exact rational counts, so you can
always be sure that the count is exact. This is very unlike all other
counters, which use floating point numbers to represent the weights, and
therefore you can only guess whether the value they show is correct or not.
While many claim to have "infinite precision", in reality, only their error
can be shown to be potentially infinite.
Ganak integrate ApproxMC and can switch to approximate counting after a timeout.
This is done by using the --appmct flag. For example, if you want to run
Ganak for 1000 seconds and then switch to approximate counting, you can do:
./ganak --appmct 1000 --mode 0 <file>
Note that this can only be used with --mode 0, i.e. in unweighted
counting.
By default, Ganak uses a probabilistic caching of component counts, which means that in extremely rare cases, often less than 1 case per billion (depending on the problem), it can return incorrect count. The probability of the wrong count is displayed at the end of solving with:
c s pac guarantees epsilon: 0 delta: 6.45757296e-10
which means that the probability of the wrong count is at most
6.45757296e-10, i.e. less than 1 in a billion.
If you must have a non-probabilistic count, you can use the --prob 0 flag.
Ganak supports many different weights:
- For counting over integers, the default mode
--mode 0works. Here, you can even run approximate counting after some timeout, with e.g--appmct 1000which will automatically switch over to approximate counting after 1000s of preprocessing and Ganak. - For counting over rationals (i.e. infinite precision weighted counting), you
can use
--mode 1which will give you a precise count, without any floating point errors. - For counting over the complex rationals field, you need to specify the weight of the
literal as a complex number and pass the
--mode 2flag. For example, if you want to give the weight 1/2 + 4i for literal 9, you can specify the weight asc p weight 9 1/2 4 0. - For counting over polynomials over a finite field, you can use
--mode 3which will give you a polynomial count. The weight of the literal is given asc p weight 9 1/2*x0+4x1+2 0which means the weight of literal 9 is1/2*x_0 + 4*x_1+2. In this mode you MUST specify the number of polynomial variables via--npolyvars N - For parity counting, you can use the
--mode 4flag. This will count the number of solutions modulo 2 - For counting over integers modulo a prime, you can use
--mode 5 --prime X, where X is the prime. - For counting over the complex numbers, but using floats instead of infinite
precision rationals, you can use
--mode 6, and specify the weights as per--mode 2.
You can also write your own field by implementing the Field and FieldGen
interfaces. Absolutely any field will work, and it's as easy as implementing
+,-,* and / operators, and the 0 and 1 constants. It's a fun
exercise to do.
We use the SharpVelvet model counter fuzzer, developed by Anna Latour to check correctness of Ganak.
@inproceedings{SM2025,
title={Engineering an Efficient Probabilistic Exact Model Counter},
author={Soos, Mate and Meel, Kuldeep S.},
booktitle={Proceedings of the International Conference on Computer Aided Verification (CAV)}
year={2025}
}
@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)},
year={2019}
}