search

crillab / d4

d4 Model Counter
GNU Lesser General Public License v3.0
14 stars 4 forks source link

Wrong result with projection #6

Closed symphorien closed 3 years ago

symphorien commented 3 years ago

Consider best.cnf:

p cnf 11 3
1 2 3 4 5 6 7 8 0
5 9 0
10 7 9 11 0

and project it on variable 6:

$ d4 -dDNNF -fpv=<(echo 6) best.cnf
[...]
s 1

but this is wrong because 1 5 10 6... and 1 5 10 -6... are valid models, so the expected answer is 2.

I minimized this with creduce. Reproduced with d4 revision d7544e4e2c89a148b444f02ee4e248b8c63193b3 (current main).

cc @jm62300

symphorien commented 3 years ago

Ah sorry, just after I click the submit button I remember that you told me to use -pv=NO https://github.com/crillab/d4/issues/4#issuecomment-853928676. This fixes the issue.