Bug Report

[muhammadusman93]

We observed two kinds of failures in Ganak: 1) crashes and 2) faulty output for projected model counting. Included below are some example CNF formulas that illustrate the failures. A more comprehensive suite of (1) formulas that we generated using our bounded-exhaustive test input generator that creates CNF files; and (2) CNF files derived from Alloy models in the standard Alloy distribution (http://alloy.lcs.mit.edu/alloy/download.html) is available at: https://github.com/testmodelcounter/testmc Ganak fails on many of these examples, possibly due to the same bugs. Some of these CNF files also show failures in other model counters, which we are separately submitting as bugs reports.

Console Output that shows crash; the formula is unsatisfiable so the count should be 0 but Ganak produces an assertion failure:

musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ cat exampleb.cnf c ind 1 0 p cnf 1 2 1 0 -1 0 musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ python3 ganak.py exampleb.cnf rm: cannot remove 'mis.out': No such file or directory rm: cannot remove 'mis.timeout': No such file or directory c Outputting solution to console c GANAK version 1.0.0 The value of delta is 0.05 The value of hashrange is 64x1 ganak: /home/musman/Desktop/ganak/src/instance.h:215: ClauseIndex Instance::addClause(std::vector<LiteralID>&): Assertion!isUnitClause(literals[0].neg())' failed. The total user time taken by ganak is: 0.0`

================================================================

Console Output that shows incorrect count for projected model counting -- running the tool as specified in ReadMe; count should be 2, but Ganak reports 3:

musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ cat examplea.cnf c ind 1 0 p cnf 2 1 1 2 0 musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ python3 ganak.py examplea.cnf rm: cannot remove 'mis.out': No such file or directory rm: cannot remove 'mis.timeout': No such file or directory c Outputting solution to console c GANAK version 1.0.0 The value of delta is 0.05 The value of hashrange is 64x1 Solving examplea.cnf variables (all/used/free): 2/2/0 clauses (all/long/binary/unit): 1/0/1/0 Warning! Sampling set is present but projected model counting is turned off by the user Sampling set size: 1 Sampling set: 1

Preprocessing .. DONE variables (all/used/free): 2/2/0 clauses (all/long/binary/unit): 1/0/1/0 Maximum cache size: 2000 MB

We have solved halfed We have solved halfed

variables (total / active / free) 2/2/0 clauses (removed) 1 (0) decisions 1 Max. decision level 1 conflicts 0 conflict clauses (all/bin/unit) 0/0/0

failed literals found by implicit BCP 0 implicit BCP miss rate 0% bytes cache size 20234600 bytes cache (overall) 20234600 bytes cache components (overall) 192 bytes cache (infra / comps) 20234408/192 bytes pure comp data (curr) 8 bytes pure comp data (overall) 8 bytes cache with sysoverh (curr) 320 bytes cache with sysoverh (overall) 320 cache (lookup / stores / hits) 1/2/0 cache miss rate 100% avg. variable count (stores / hits) 2/0

# solutions 3 # END

time: 0.001563s

The total user time taken by ganak is: 0.0

================================================================

Console Output that shows incorrect count for projected model counting -- using the new “-p” option; count should be 2 but Ganak reports 3:

musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ cat examplea.cnf c ind 1 0 p cnf 2 1 1 2 0 musman@musman-Alienware-15-R4:~/Desktop/ganak/build$ python3 ganak.py -p examplea.cnf rm: cannot remove 'mis.out': No such file or directory rm: cannot remove 'mis.timeout': No such file or directory c Outputting solution to console c GANAK version 1.0.0 The value of delta is 0.05 The value of hashrange is 64x1 Solving examplea.cnf variables (all/used/free): 2/2/0 clauses (all/long/binary/unit): 1/0/1/0 Sampling set is present, performing projected model counting Sampling set size: 1 Sampling set: 1

Preprocessing .. DONE variables (all/used/free): 2/2/0 clauses (all/long/binary/unit): 1/0/1/0 Maximum cache size: 2000 MB

We have solved halfed We have solved halfed

variables (total / active / free) 2/2/0 clauses (removed) 1 (0) decisions 1 Max. decision level 1 conflicts 0 conflict clauses (all/bin/unit) 0/0/0

failed literals found by implicit BCP 0 implicit BCP miss rate 0% bytes cache size 20234600 bytes cache (overall) 20234600 bytes cache components (overall) 192 bytes cache (infra / comps) 20234408/192 bytes pure comp data (curr) 8 bytes pure comp data (overall) 8 bytes cache with sysoverh (curr) 320 bytes cache with sysoverh (overall) 320 cache (lookup / stores / hits) 1/2/0 cache miss rate 100% avg. variable count (stores / hits) 2/0

# solutions 3 # END

time: 0.001452s

The total user time taken by ganak is: 0.0

[smsharma1]

Thank you so much @muhammadusman93 for pointing out the bugs. I have resolved them and the solver is giving me correct answers for the test cases you have mentioned. Please let me know if you need any help.