You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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).
1
+
# Ganak2 -- A Probabilistic Exact Model Counter
2
+
Ganak takes in a CNF formula and returns `count` such that `count` is the
3
+
number of solutions of `F` with confidence at least `1 - delta`. Delta is fixed to
4
+
approx 2^-40.
3
5
4
-
To read more about Ganak-specific ideas, please refer to [our paper](https://www.comp.nus.edu.sg/~meel/Papers/ijcai19srsm.pdf). Note that Ganak employs many ideas by many people. See AUTHORS for a list.
6
+
To read more about Ganak-specific ideas, please refer to [our
7
+
paper](https://www.comp.nus.edu.sg/~meel/Papers/ijcai19srsm.pdf). Note that
8
+
Ganak employs many ideas by many people. See AUTHORS for a list.
5
9
6
-
## Compiling in Linux
10
+
## Building
7
11
8
-
To build ganak, you first need to build [CryptoMiniSat](github.com/msoos/cryptominisat). Then issue:
12
+
Use of the [release binaries](https://github.com/meelgroup/ganak/releases) is
13
+
strongly encouraged, as Ganak requires a specific set of libraries to be
14
+
installed. The second best thing to use is Nix. Simply [install
15
+
nix](https://nixos.org/download/) and then:
9
16
10
-
```bash
11
-
sudo apt-get install libgmp-dev
12
-
sudo apt-get install libmpfr-dev
13
-
sudo apt-get install libmpc-dev
14
-
mkdir build &&cd build
15
-
cmake ..
16
-
make
17
+
```plaintext
18
+
git clone https://github.com/meelgroup/ganak
19
+
nix-shell
17
20
```
21
+
If this is somehow not what you want, you can also build it. See the GitHub
22
+
Action for the specific set of steps. At the end of this README you can
23
+
find a detailed set of instructions.
18
24
19
25
## Usage
20
-
Ganak takes a CNF in DIMACS form as an input:
26
+
Ganak takes a CNF in a special, DIMACS-like format as specified by the
27
+
model counting competition [guidelines](https://mccompetition.org/assets/files/mccomp_format_24.pdf).
28
+
Basically, the format is as follows:
21
29
22
-
```bash
23
-
./ganak myfile.cnf
30
+
```plaintext
31
+
c t pwmc
32
+
p cnf 3 2
33
+
c p weight 1 0.3 0
34
+
c p weight -1 0.8 0
35
+
1 2 3 0
36
+
-1 2 0
37
+
c p show 1 2 0
24
38
```
39
+
The first line says it's a projected weighted model counting instance. The
40
+
second line says it has 3 variables and 2 clauses. The third and fourth lines
41
+
specify the weights of the variables 1. The weight of the literal 1 is 0.3 and
42
+
the weight of the literal -1 is 0.8. The weight of all unspecified variables is
43
+
1 for both positive and negative literals.
44
+
45
+
The last line says that the projection set of the counter is only variables 1
46
+
and 2. If no projection set is given, then the counter does an unprojected
47
+
count, i.e. all variables are assumed to be in the projection set.
48
+
49
+
Beware to ALWAYS give the weight of both the literal and its negation or
50
+
different counters may give different results.
51
+
52
+
We can now count the number of solutions of the above formula using Ganak:
53
+
```plaintext
54
+
./ganak --verb 0 --mode 1 a.cnf
55
+
c o Total time [Arjun+GANAK]: 0.00
56
+
s SATISFIABLE
57
+
c s exact arb float 1.8999e+00
58
+
c o exact arb 19/10
59
+
```
60
+
61
+
We need to pass `--mode 1` because it's a weighted model counting instance. The count
62
+
is presented both in a floating point format and as a fraction. The fraction is
63
+
always precise.
25
64
26
65
## Benchmarks
27
-
Few toy benchmarks are given in benchmarks directory. Full list of benchmarks used for our experiments is available [here](https://drive.google.com/file/d/15dUJI55drFH_0-4-qWjoF_YR0amb3xnK/view?usp=sharing)
66
+
Model Counting Competition benchmarks are available on the [Model Counting
GANAK licensed under MIT. Flow Cutter licensed under BSD2-style license. Binary built contains both (they are compatible with each other).
83
+
## Building from source
84
+
85
+
```bash
86
+
sudo apt-get install -yq libgmp-dev libmpfr-dev
87
+
88
+
git clone https://github.com/meelgroup/cadical
89
+
cd cadical
90
+
git checkout add_dynamic_lib
91
+
./configure
92
+
make
93
+
cd ..
94
+
95
+
git clone https://github.com/meelgroup/cadiback
96
+
cd cadiback
97
+
git checkout synthesis
98
+
./configure
99
+
make
100
+
cd ..
101
+
102
+
git clone https://github.com/msoos/cryptominisat
103
+
cd cryptominisat
104
+
git checkout synthesis
105
+
mkdir build &&cd build
106
+
cmake ..
107
+
make
108
+
cd ../..
109
+
110
+
git clone https://github.com/meelgroup/sbva
111
+
cd sbva
112
+
mkdir build &&cd build
113
+
cmake ..
114
+
make
115
+
cd ../..
116
+
117
+
git clone https://github.com/meelgroup/breakid
118
+
cd breakid
119
+
mkdir build &&cd build
120
+
cmake ..
121
+
make
122
+
cd ../..
123
+
124
+
git clone https://github.com/meelgroup/approxmc
125
+
cd approxmc
126
+
mkdir build &&cd build
127
+
git checkout synthesis
128
+
cmake ..
129
+
make
130
+
cd ../..
131
+
132
+
git clone https://github.com/meelgroup/ganak
133
+
cd ganak
134
+
mkdir build &&cd build
135
+
cmake ..
136
+
make
137
+
```
138
+
139
+
if you also need to have the system run on older or different machines, you
140
+
need to have it compile for Sandybridge architecture. To do this, you need to
141
+
recompile GMP and MPFR with the right flags. Here is how to do it:
43
142
44
-
See AUTHORS for full list. Ganak-specific contributions by, in alphabetical order: Kuldeep S. Meel, Subhajit Roy, Shubham Sharma, Mate Soos. However, MANY people's ideas contributed to Ganak. It's easy to list everyone from Stockmayer (e.g. probing) to Donald Knuth (e.g. memops).
0 commit comments