sharpASP - Exact ASP Counting with Compact Encodings

• GMPlib

Clone the repository including all the submodules via

git clone --recursive [email protected]/meelgroup/sharpASP.git

To build sharpASP(D4):

cd d4
make 

To build sharpASP(ganak):

cd ganak-asp && cd script
./build_norm.sh

To build sharpASP(sharpsat-td):

cd sharpsat-td
./setupdev.sh

The input CNFs are available here. The CNFs are in completion + copy format. The CNFs can be used as SharpASP input file without any processing.

We run our experiment in linux system

Make sure that the complied binaries of D4, sharpSAT-TD, ganak, and flow_cutter_pace17 exist in the current directory

Run sharpASP(GANAK) using the following command (with input: asp_normalized-hamiltonian_cycle.random-graph-20-4-16.zip.lp.cnf): The input file contains Completion & Copy of program

./ganak -noPCC -cs 4000 -noIBCP asp_normalized-hamiltonian_cycle.random-graph-20-4-16.zip.lp.cnf

Run sharpASP(sharpSAT-TD) using the following command:

./sharpSAT -decot 100 -decow 100 -tmpdir . -cs 4000 CNF/asp_normalized-hamiltonian_cycle.random-graph-20-4-16.zip.lp.cnf

Run sharpASP(D4) using the following command:

./d4 -pv=NO -mc CNF/asp_normalized-hamiltonian_cycle.random-graph-20-4-16.zip.lp.cnf

The experimental log files are available here.