Repository files navigation

Pepin is a DNF streaming counting tool that gives the number of approximatepoints in a volume given a set of n-dimensional boxes that may intersect. Thinkof it as a tool that takes a set of cubes in space and approximates the totalvolume of all cubes. The related research paper, published at IJCAI 2023 isEngineering an Efficient ApproximateDNF-Counter.

The tool takes in a set of cubes from a DNF file, such as this, that has 10dimensions, and 2 cubes:

$ cat myfile.dnfp dnf 20 21 2 3 01 -5 0

And outputs a probabilistically approximate count.

We suggest downloading areleased binary.You can also use it via Nix: simplyinstall Nix and then:

nix shell github:meelgroup/pepin

You will then have thepepin binary available in your path.

If you want to build it from source, you can do so with the following commands:

sudo apt-get install libgmp-dev zlib1g-dev cmake build-essential gitgit clone https://github.com/meelgroup/pepinmkdir buildcd buildcmake ..make

Run it via:

./pepin --epsilon 0.15 --delta 0.1 myfile.dnf[...]c [dnfs] Low-precision approx num points: 348672

Notice that the cube1 2 3 has2**17=131072 points, and1 -5 has2**18=262144, so a total of 393216. But they overlap,1 2 3 -5 is countedtwice. So the exact number is: 327680. Hence, we over-approximated a bit here.The error is1.0-348672/327680=-0.064, so about 6.4%. This is well below theadvertised 15% error allowed (i.e. epsilon 0.15).

Pepin is a streaming, weighted approximate model. Because it works with datastreams, you must declare the weights of all literals before you start thestream. Hence, the weights need to be declared at the top of the DNF file. Hereis an example:

$ cat myfile-weighted.dnfp dnf 20 2w 1 2/3w 2 3/41 2 3 01 -5 0

The weights of variables 1 and 2 are now declared to be 2/3 and 3/4,respectively. The rest of the variables will have weight 1/2 by default.

Currently, the algorithm can only return estimate after the exact number ofclauses have been passed in as promised. This means you must have thep dnf VARS CLS header correct in your DNF file or the tool will not work.

You can install the library withsudo make install. Then, the installedheader filepepin/pepin.h can be used as a library:

#include<pepin/pepin.h>#include<iostream>#include<iomanip>#include<vector>usingnamespacePepinNS;intmain() {  Pepin pepin;  pepin.new_vars(20);  pepin.set_n_cls(2);typedef std::vector<Lit> CL;  pepin.add_clause(CL{itol(1),itol(2),itol(3)});  pepin.add_clause(CL{itol(1),itol(-5)});auto weigh_nsols = pepin.get_low_prec_appx_weighted_sol();  std::cout <<"Solution:" << std::scientific << *weigh_nsols <<"std::endl;  return 0;}

The library is clean -- it cleans up after itself, you can have more than onein memory, you can even run them in parallel, if you wish.

You can fuzz by building DNFKLM fromhere, putting the resultingDNFKLM binary intobuild/, and then:

cd buildln -s ../scripts/*../build_norm.shmkdir -f tests./fuzz_test.py

You can checkfuzz_test.py to adjust etc.

MIT license all the way through