sha1-sat

sha1-sat copied to clipboard

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...

olegzaikin

PB Encoding Buggy

3

Hi, Nice work, but there is a bug with the PB encoding of the sum modulo 32: The used encoding for add2 (similar issue exists for add5) is \sum_{i=0}^{31} 2^i...

StephanGocht

Practical Use Case Example

3

Hello and thanks again for the great project. I read the code, read your thesis and am intrigued. I have also seen some other modern research in this area which...

GregoryMorse

Windows translation

3

Thanks for this nice project. I got it working on Windows and will give relevant code snippets though conditional compilation and integration based on that would be needed to add...

GregoryMorse

$ ./main -h terminate called after throwing an instance of 'boost::exception_detail::clone_implboost::exception_detail::error_info_injector' what(): unknown option -h zsh: abort (core dumped) ./main -h

msoos