From 4a1604ba1b58e81f00a87cc061cf714b3483dac1 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 3 Jun 2024 15:25:24 -0400 Subject: [PATCH] Updating readme --- README.md | 90 ++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 63 insertions(+), 27 deletions(-) diff --git a/README.md b/README.md index 09ae12a..ac2a25d 100644 --- a/README.md +++ b/README.md @@ -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 @@ -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 @@ -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: @@ -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 @@ -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.