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
ApproxMCv4 is a state-of-the-art approximate model counter utilizing an improved version of CryptoMiniSat to give approximate model counts to problems of size and complexity that were not possible before.
8
-
9
-
This work is by Mate Soos, Stephan Gocht, and Kuldeep S. Meel, as [published in AAAI-19](https://www.cs.toronto.edu/~meel/Papers/aaai19-sm.pdf) and [in CAV2020](https://www.cs.toronto.edu/~meel/Papers/cav20-sgm.pdf). A large part of the work is in CryptoMiniSat [here](https://github.com/msoos/cryptominisat).
10
-
11
-
ApproxMC handles CNF formulas and performs approximate counting.
12
-
13
-
1. If you are interested in exact model counting, visit our exact counter [Ganak](http://github.com/meelgroup/ganak)
14
-
2. If you are instead interested in DNF formulas, visit our approximate DNF counter [Pepin](https://github.com/meelgroup/pepin).
6
+
# ApproxMC6: Approximate Model Counter
7
+
ApproxMCv6 is a state-of-the-art approximate model counter utilizing an
8
+
improved version of CryptoMiniSat to give approximate model counts to problems
9
+
of size and complexity that were not possible before.
10
+
11
+
This work is the culmination of work by a number of people, including but not
12
+
limited to, Mate Soos, Jiong Yang, Stephan Gocht, Yash Pote, and Kuldeep S.
print("Approximate count is: %d*2**%d"% (count[0], count[1]))
33
42
```
34
43
35
-
The above will print that `Approximate count is: 11*2**16`. Since the largest variable in the clauses was 20, the system contained 2\*\*20 (i.e. 1048576) potential models. However, some of these models were prohibited by the two clauses, and so only approximately 11*2\*\*16 (i.e. 720896) models remained.
44
+
The above will print that `Approximate count is: 11*2**16`. Since the largest
45
+
variable in the clauses was 20, the system contained 2\*\*20 (i.e. 1048576)
46
+
potential models. However, some of these models were prohibited by the two
47
+
clauses, and so only approximately 11*2\*\*16 (i.e. 720896) models remained.
36
48
37
-
If you want to count over a projection set, you need to call `count(projection_set)`, for example:
49
+
If you want to count over a projection set, you need to call
50
+
`count(projection_set)`, for example:
38
51
39
52
```python
40
53
import pyapproxmc
@@ -45,7 +58,8 @@ count = c.count(range(1,10))
45
58
print("Approximate count is: %d*2**%d"% (count[0], count[1]))
46
59
```
47
60
48
-
This now prints `Approximate count is: 7*2**6`, which corresponds to the approximate count of models, projected over variables 1..10.
61
+
This now prints `Approximate count is: 7*2**6`, which corresponds to the
62
+
approximate count of models, projected over variables 1..10.
49
63
50
64
## How to Build a Binary
51
65
To build on Linux, you will need the following:
@@ -104,21 +118,35 @@ sudo ldconfig
104
118
```
105
119
106
120
## How to Use the Binary
107
-
First, you must translate your problem to CNF and just pass your file as input to ApproxMC. Voila -- and it will print the number of solutions of the given CNF formula.
121
+
First, you must translate your problem to CNF and just pass your file as input
122
+
to ApproxMC. Then issue `./approxmc myfile.cnf`, it will print the number of
123
+
solutions of formula.
108
124
109
-
### Providing a Sampling Set
110
-
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. ApproxMC allows you to specify the sampling set using the following modified version of DIMACS format:
125
+
### Providing a Sampling Set (or Projection Set)
126
+
For some applications, one is not interested in solutions over all the
127
+
variables and instead interested in counting the number of unique solutions to
128
+
a subset of variables, called sampling set (also called a "projection set").
129
+
ApproxMC allows you to specify the sampling set using the following modified
130
+
version of DIMACS format:
111
131
112
132
```shell
113
133
$ cat myfile.cnf
114
-
c ind 1 3 4 6 7 8 10 0
134
+
c p show 1 3 4 6 7 8 10 0
115
135
p cnf 500 1
116
136
3 4 0
117
137
```
118
-
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 ApproxMC 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.
138
+
Above, using the `c p show` line, we declare that only variables 1, 3, 4, 6, 7,
139
+
8 and 10 form part of the sampling set out of the CNF's 500 variables
140
+
`1,2...500`. This line must end with a 0. The solution that ApproxMC will be
141
+
giving is essentially answering the question: how many different combination of
142
+
settings to this variables are there that satisfy this problem? Naturally, if
143
+
your sampling set only contains 7 variables, then the maximum number of
144
+
solutions can only be at most 2^7 = 128. This is true even if your CNF has
145
+
thousands of variables.
119
146
120
147
### Running ApproxMC
121
-
In our case, the maximum number of solutions could at most be 2^7=128, but our CNF should be restricting this. Let's see:
148
+
In our case, the maximum number of solutions could at most be 2^7=128, but our
149
+
CNF should be restricting this. Let's see:
122
150
123
151
```shell
124
152
$ approxmc --seed 5 myfile.cnf
@@ -185,20 +213,28 @@ int main() {
185
213
```
186
214
187
215
### ApproxMC5: Sparse-XOR based Approximate Model Counter
188
-
Note: this is beta version release, not recommended for general use. We are currently working on a tight integration of sparse XORs into ApproxMC based on our [LICS-20](http://www.cs.toronto.edu/~meel/Papers/lics20-ma.pdf) paper. You can turn on the sparse XORs using the flag "sparse" but beware as reported in LICS-20 paper, this may slow down in some cases; it is likely to give a significant speedup if the number of solutions is very large.
216
+
Note: this is beta version release, not recommended for general use. We are
217
+
currently working on a tight integration of sparse XORs into ApproxMC based on
218
+
our [LICS-20](http://www.cs.toronto.edu/~meel/Papers/lics20-ma.pdf) paper. You
219
+
can turn on the sparse XORs using the flag `--sparse 1` but beware as reported in
220
+
LICS-20 paper, this may slow down solving in some cases. It is likely to give a
221
+
significant speedup if the number of solutions is very large.
189
222
190
223
191
224
### Issues, questions, bugs, etc.
192
225
Please click on "issues" at the top and [create a new issue](https://github.com/meelgroup/mis/issues/new). All issues are responded to promptly.
193
226
194
227
## How to Cite
195
-
If you use ApproxMC, please cite the following papers: [CAV20](https://dblp.uni-trier.de/rec/conf/cav/SoosGM20.html?view=bibtex), [AAAI19](https://www.cs.toronto.edu/~meel/bib/SM19.bib) and [IJCAI16](https://www.cs.toronto.edu/~meel/bib/CMV16.bib).
196
-
197
-
If you use sparse XORs, please also cite the [LICS20](https://www.cs.toronto.edu/~meel/publications/AM20.bib) paper.
198
-
199
-
ApproxMC builds on a series of papers on hashing-based approach: [Related Publications](https://www.cs.toronto.edu/~meel/publications.html)
228
+
If you use ApproxMC, please cite the following papers:
The benchmarks used in our evaluation can be found [here](https://zenodo.org/records/10449477).
202
-
203
-
## Old Versions
204
-
The old version, 2.0 is available under the branch "ver2". Please check out the releases for the 2.x versions under GitHub [releases](https://github.com/meelgroup/approxmc/releases). Please read the README of the old release to know how to compile the code. Old releases should easily compile.
0 commit comments