vegard / sha1-sat

SAT instance generator for SHA-1
GNU General Public License v3.0
47 stars 14 forks source link

Wrong number of clauses in CNF header #9

Open olegzaikin opened 1 year ago

olegzaikin commented 1 year ago

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 solvers, e.g. kissat, throw errors when parsing the CNF. Is it the case that some clauses are not written or just the header is wrong?

msoos commented 1 year ago

I believe I have fixed this in my version, check it out:

https://github.com/msoos/sha1-sat/

Mate

olegzaikin commented 1 year ago

Thanks, Mate!

Do you remember what was the reason of this issue?

Oleg