Skip to content

Commit

Permalink
Updating readme
Browse files Browse the repository at this point in the history
  • Loading branch information
@msoos
msoos committed Jun 3, 2024
1 parent b382413 commit 4a1604b
Showing 1 changed file with 63 additions and 27 deletions.
90 changes: 63 additions & 27 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,24 @@
[![Docker Hub](https://img.shields.io/badge/docker-latest-blue.svg)](https://hub.docker.com/r/msoos/approxmc/)


# ApproxMC4: Approximate Model Counter
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.

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

ApproxMC handles CNF formulas and performs approximate counting.

1. If you are interested in exact model counting, visit our exact counter [Ganak](http://github.com/meelgroup/ganak)
2. If you are instead interested in DNF formulas, visit our approximate DNF counter [Pepin](https://github.com/meelgroup/pepin).
# ApproxMC6: Approximate Model Counter
ApproxMCv6 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.

This work is the culmination of work by a number of people, including but not
limited to, Mate Soos, Jiong Yang, Stephan Gocht, Yash Pote, and Kuldeep S.
Meel. Publications: published [in
AAAI-19](https://www.cs.toronto.edu/~meel/Papers/aaai19-sm.pdf), [in
CAV2020](https://www.cs.toronto.edu/~meel/Papers/cav20-sgm.pdf), and [in
CAV2023](https://arxiv.org/pdf/2305.09247). A large part of the work is in
[CryptoMiniSat](https://github.com/msoos/cryptominisat).

ApproxMC handles CNF formulas and performs approximate counting.
1. If you are interested in exact model counting, visit our exact counter
[Ganak](http://github.com/meelgroup/ganak)
2. If you are instead interested in DNF formulas, visit our approximate DNF
counter [Pepin](https://github.com/meelgroup/pepin).

## How to use the Python interface

Expand All @@ -32,9 +41,13 @@ count = c.count()
print("Approximate count is: %d*2**%d" % (count[0], count[1]))
```

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.
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.

If you want to count over a projection set, you need to call `count(projection_set)`, for example:
If you want to count over a projection set, you need to call
`count(projection_set)`, for example:

```python
import pyapproxmc
Expand All @@ -45,7 +58,8 @@ count = c.count(range(1,10))
print("Approximate count is: %d*2**%d" % (count[0], count[1]))
```

This now prints `Approximate count is: 7*2**6`, which corresponds to the approximate count of models, projected over variables 1..10.
This now prints `Approximate count is: 7*2**6`, which corresponds to the
approximate count of models, projected over variables 1..10.

## How to Build a Binary
To build on Linux, you will need the following:
Expand Down Expand Up @@ -104,21 +118,35 @@ sudo ldconfig
```

## How to Use the Binary
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.
First, you must translate your problem to CNF and just pass your file as input
to ApproxMC. Then issue `./approxmc myfile.cnf`, it will print the number of
solutions of formula.

### Providing a Sampling Set
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:
### Providing a Sampling Set (or Projection Set)
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 (also called a "projection set").
ApproxMC allows you to specify the sampling set using the following modified
version of DIMACS format:

```shell
$ cat myfile.cnf
c ind 1 3 4 6 7 8 10 0
c p show 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 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.
Above, using the `c p show` 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.

### Running ApproxMC
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:
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:

```shell
$ approxmc --seed 5 myfile.cnf
Expand Down Expand Up @@ -185,20 +213,28 @@ int main() {
```

### ApproxMC5: Sparse-XOR based Approximate Model Counter
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.
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 1` but beware as reported in
LICS-20 paper, this may slow down solving in some cases. It is likely to give a
significant speedup if the number of solutions is very large.


### Issues, questions, bugs, etc.
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.

## How to Cite
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).

If you use sparse XORs, please also cite the [LICS20](https://www.cs.toronto.edu/~meel/publications/AM20.bib) paper.

ApproxMC builds on a series of papers on hashing-based approach: [Related Publications](https://www.cs.toronto.edu/~meel/publications.html)
If you use ApproxMC, please cite the following papers:
[AAAI-19](https://www.cs.toronto.edu/~meel/Papers/aaai19-sm.pdf), [in
CAV2020](https://www.cs.toronto.edu/~meel/Papers/cav20-sgm.pdf), and [in
CAV2023](https://arxiv.org/pdf/2305.09247).
[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). If you use sparse
XORs, please also cite the
[LICS20](https://www.cs.toronto.edu/~meel/publications/AM20.bib) paper.
ApproxMC builds on a series of papers on hashing-based approach: [Related
Publications](https://www.cs.toronto.edu/~meel/publications.html)

The benchmarks used in our evaluation can be found [here](https://zenodo.org/records/10449477).

## Old Versions
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 comments on commit 4a1604b

Please sign in to comment.