Oleg Zaikin

Unclear how to extract all models in cautious enumeration

3

Hi. I need to find all models (satisfying assignments) of a CNF, so I run clasp with --models=0. When --enum-mode=bt or --enum-mode=record are set, then all models are found as...

Wrong number of clauses in CNF header

2

The command `./main --cnf --rounds=80 --hash-bits=160 > instance.cnf` builds a CNF with the header p cnf 13408 **478924** However, in fact the CNF contains **478636** clauses. That is why some...

Add an example for Algorithm Configuration facade

4

I am going to use SMAC3 to tune a CDCL SAT solver's parameters to minimize the total runtime on a set of instances (CNFs). I suppose that the Algorithm Configuration...