Repository files navigation

ApproxMCv6 is a state-of-the-art approximate model counter usingArjun andCryptoMiniSat to give probabilisticapproximate model counts to problems of size and complexity that were notpossible 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.

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.

It is strongly recommended to not build, but to use the precompiledbinaries as in ourrelease.The second best thing to use is Nix. Simplyinstallnix and then:

nix shell github:meelgroup/approxmc

Then you will haveapproxmc binary available and ready to use.

If this is somehow not what you want, you can also build it. See theGitHubAction for thespecific set of steps.

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] Sampling set size: 7[appmc] Sampling set: 1, 3, 4, 6, 7, 8, 10,[appmc] Using start iteration 0[appmc] [    0.00 ] bounded_sol_count looking for   73 solutions -- hashes active: 0[appmc] [    0.01 ] bounded_sol_count looking for   73 solutions -- hashes active: 1[appmc] [    0.01 ] bounded_sol_count looking for   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'sindependent 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 foundis within a certain tolerance (called "epsilon") with a certain probability(called "delta"). The default tolerance and probability, i.e. epsilon and deltavalues, are set to 0.8 and 0.2, respectively. Both values are configurable.

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.

The system can be used as a library:

#include<approxmc/approxmc.h>#include<vector>#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 newissue. All issues are respondedto 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.