search

meelgroup / bosphorus

Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter
Other
67 stars 18 forks source link

cnf to anf conversion makes it unsat #41

Closed gvarga2 closed 1 year ago

gvarga2 commented 1 year ago

Hi Mate!

I have a cnf file, maybe a little bit big: p cnf 40397 108920 sat.cnf.gz

My problem is that while it is easily solved by cryptominisat, after I convert it into anf, it will be unsatisfiable.

I do the conversion using the docker image:

docker run --rm -v `pwd`/:/dat/ msoos/bosphorus --cnfread /dat/sat.cnf --anfwrite /dat/sat.anf

It's unsat with --xl 0, but sat with --el 0, so I guess the ElimLin causes it somehow. I tried to make the cnf smaller, but then the issue was not reproducible. Do you have any idea? Am I doing something wrong?

Thanks!

Regards, Gábor

gvarga2 commented 1 year ago

Oh, now I see that the docker image is not the latest version, building it from scratch seems to work.

msoos commented 1 year ago

Oh, glad it works from non-Docker. Yeah, the Docker is outdated, I should remove it. Thanks for letting me know!

Mate