This site provides access to the source code of our model counter dualiza and related programs to generate the benchmarks used in our ICTAI'18 paper.

It can read simple boolean formulas in limboole syntax, CNF in DIMACS format as well as AIGs in AIGER.

Sibylle Möhle, Armin Biere. Dualizing Projected Model Counting. To be published in Proc. 30th Intl. Conf. on Tools with Artificial Intelligence (ICTAI'18), 8 pages, IEEE Computer Society, 2018.
[ paper | dualiza ]

Source Code

Latest version is available on GitHub as https://github.com/arminbiere/dualiza.

[ dualiza-github-1.0.0-b641f50.tar.xz ]
[ dualiza-00b-9e9f8e0.tar.xz | clause.sh | nrp.c ]