Repository files navigation

ApproxMCv6 is a state-of-the-art approximate model counter utilizing animproved version of CryptoMiniSat to give approximate model counts to problemsof size and complexity that were not possible before.

This work is the culmination of work by a number of people, including but notlimited to, Mate Soos, Jiong Yang, Stephan Gocht, Yash Pote, and Kuldeep S.Meel. Publications: publishedinAAAI-19,inCAV2020, andinCAV2023. A large part of the work is inCryptoMiniSat.

ApproxMC handles CNF formulas and performs approximate counting.

1. If you are interested in exact model counting, visit our exact counterGanak
2. If you are instead interested in DNF formulas, visit our approximate DNFcounterPepin.

Install using pip:

pip install pyapproxmc

Then you can use it as:

importpyapproxmcc=pyapproxmc.Counter()c.add_clause([1,2,3])c.add_clause([3,20])count=c.count()print("Approximate count is: %d*2**%d"% (count[0],count[1]))

The above will print thatApproximate count is: 11*2**16. Since the largestvariable in the clauses was 20, the system contained 2**20 (i.e. 1048576)potential models. However, some of these models were prohibited by the twoclauses, and so only approximately 11*2**16 (i.e. 720896) models remained.

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

importpyapproxmcc=pyapproxmc.Counter()c.add_clause([1,2,3])c.add_clause([3,20])count=c.count(range(1,10))print("Approximate count is: %d*2**%d"% (count[0],count[1]))

This now printsApproximate count is: 7*2**6, which corresponds to theapproximate count of models, projected over variables 1..10.

To build on Linux, you will need the following:

sudo apt-get install build-essential cmakeapt-get install libgmp3-dev

Then, build CryptoMiniSat, Arjun, and ApproxMC:

# not required but very usefulsudo apt-get install zlib1g-devgit clone https://github.com/meelgroup/cadicalcd cadicalgit checkout mate-only-libraries-1.8.0./configuremakecd ..git clone https://github.com/meelgroup/cadibackcd cadibackgit checkout mate./configuremakecd ..git clone https://github.com/msoos/cryptominisatcd cryptominisatmkdir build&&cd buildcmake ..makecd ../..git clone https://github.com/meelgroup/sbvacd sbvamkdir build&&cd buildcmake ..makecd ../..git clone https://github.com/meelgroup/arjuncd arjunmkdir build&&cd buildcmake ..makecd ../..git clone https://github.com/meelgroup/approxmccd approxmcmkdir build&&cd buildcmake ..makesudo make installsudo ldconfig

First, you must translate your problem to CNF and just pass your file as inputto ApproxMC. Then issue./approxmc myfile.cnf, it will print the number ofsolutions of formula.

For some applications, one is not interested in solutions over all thevariables and instead interested in counting the number of unique solutions toa subset of variables, called sampling set (also called a "projection set").ApproxMC allows you to specify the sampling set using the following modifiedversion of DIMACS format:

$ cat myfile.cnfc p show 1 3 4 6 7 8 10 0p cnf 500 13 4 0

Above, using thec 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 variables1,2...500. This line must end with a 0. The solution that ApproxMC will begiving is essentially answering the question: how many different combination ofsettings to this variables are there that satisfy this problem? Naturally, ifyour sampling set only contains 7 variables, then the maximum number ofsolutions can only be at most 2^7 = 128. This is true even if your CNF hasthousands of variables.

In our case, the maximum number of solutions could at most be 2^7=128, but ourCNF should be restricting this. Let's see:

$ approxmc --seed 5 myfile.cnfc ApproxMC version 3.0[...]c CryptoMiniSat SHA revision [...]c Using code from'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'[...][appmc] using seed: 5[appmc] Samplingset size: 7[appmc] Sampling set: 1, 3, 4, 6, 7, 8, 10,[appmc] Using start iteration 0[appmc] [    0.00 ] bounded_sol_count lookingfor   73 solutions -- hashes active: 0[appmc] [    0.01 ] bounded_sol_count lookingfor   73 solutions -- hashes active: 1[appmc] [    0.01 ] bounded_sol_count lookingfor   73 solutions -- hashes active: 0[...][appmc] FINISHED ApproxMC T: 0.04 sc [appmc] Number of solutions is: 48*2**1s mc 96

ApproxMC reports that we have approximately96 (=48*2) solutions to the CNF's independent support. This is because for variables 3 and 4 we have banned thefalse,false solution, so out of their 4 possible settings, one is banned. Therefore, we have2^5 * (4-1) = 96 solutions.

ApproxMC provides so-called "PAC", or Probably Approximately Correct, guarantees. In less fancy words, the system guarantees that the solution found is within a certain tolerance (called "epsilon") with a certain probability (called "delta"). The default tolerance and probability, i.e. epsilon and delta values, are set to 0.8 and 0.2, respectively. Both values are configurable.

The system can be used as a library:

#include<approxmc/approxmc.h>#include<vector>#include<complex>#include<cassert>using std::vector;usingnamespaceApproxMC;usingnamespaceCMSat;intmain() {    AppMC appmc;    appmc.new_vars(10);    vector<Lit> clause;//add "-3 4 0"    clause.clear();    clause.push_back(Lit(2,true));    clause.push_back(Lit(3,false));    appmc.add_clause(clause);//add "3 -4 0"    clause.clear();    clause.push_back(Lit(2,false));    clause.push_back(Lit(3,true));    appmc.add_clause(clause);    SolCount c = appmc.count();uint32_t cnt =std::pow(2, c.hashCount)*c.cellSolCount;assert(cnt ==std::pow(2,9));return0;}

Note: this is beta version release, not recommended for general use. We arecurrently working on a tight integration of sparse XORs into ApproxMC based onourLICS-20 paper. Youcan turn on the sparse XORs using the flag--sparse 1 but beware as reported inLICS-20 paper, this may slow down solving in some cases. It is likely to give asignificant speedup if the number of solutions is very large.

Please click on "issues" at the top andcreate a new issue. All issues are responded to promptly.

If you use ApproxMC, please cite the following papers:AAAI-19,inCAV2020, andinCAV2023.CAV20,AAAI19 andIJCAI16. If you use sparseXORs, please also cite theLICS20 paper.ApproxMC builds on a series of papers on hashing-based approach:RelatedPublications

The benchmarks used in our evaluation can be foundhere.