ISYMGANAK

Isymganak takes in a CNF formula F as input and returns count such that count is the number of solutions of F. This solver is built on top of symganak. To read more about technical algorithms in symganak, please refer to the paper

Installation

Dependencies

You need the following libraries:

System-wide (recommended):

• GMP (libgmp)
• GMP C++ bindings (libgmpxx)
• SQLite3 (libsqlite3)

Local or system-wide:

• Nauty
• igraph
• xxHash

Important note about toolchains

Build your dependencies with the same toolchain you use to build isymganak (same compiler and standard library). Mixing toolchains is a great way to waste an afternoon.

Building dependencies from source

To build Nauty, igraph, and xxHash from scratch, follow the detailed instructions in lib/README.md.

Compiling ISYMGANAK

To build isymganak, issue:

# install GMP/GMPXX/SQLite3 system-wide 
# using your distro's package manager.
git clone https://github.com/IbrahimElk/isymganak
cmake -S . -B build
cmake --build build

For Mac, pass option cmake -DDOPCC=OFF ... to cmake

Model Counting

To count, run:

build/isymganakker \
    -q \
    -t 3600 \
    -cs 3200 \
    -SBS 0 \
    -DBS 0 \
    -FG \ 
    -useL2 \
    -L2prop 17 \
    benchmarks/cnfgen/counting/count21-3.cnf

Issues, questions, bugs, etc

Please click on "issues" at the top and create a new issue.

Contributors

• Ibrahim El Kaddouri (ibrahim.elkaddouri@student.kuleuven.be)
• Vincent Derkinderen (vincent.derkinderen@cs.kuleuven.be )
• Timothy Van Bremen (timothy.vanbremen@cs.kuleuven.be)
• Shubham Sharma (sharma.shubham736@gmail.com)
• Mate Soos (soos.mate@gmail.com)
• Subhajit Roy (subhajit@iitk.ac.in)
• Kuldeep Meel (meel@comp.nus.edu.sg)