search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
814 stars 178 forks source link

"Improvement" on Minisat - also useful for CMS? #123

Closed capiman closed 10 years ago

capiman commented 10 years ago

This was just published in Minisat mailing list:

http://www.jair.org/papers/paper4016.html

PDF: http://www.jair.org/media/4016/live-4016-7398-jair.pdf

"The main point of the paper is a theoretical one, but I was able to speed up propagation in Minisat by 29%. Don't be too excited because that was only with all learning etc switched off. When I turned learning back on again any improvement disappeared. "

Link to source code changes against Minisat: http://www.jair.org/media/4016/live-4016-7401-jair.tgz

msoos commented 10 years ago

Thanks. I'll take this into account. Unfortunately, a lot of these things are not very reliable. Watchlist sizes can vary between 2 and 20'000. The data the author presents doesn't seem to indicate what types of problems did he try. The difference could be enormous. So, I'll keep this in mind, thanks. But I'll be cautious. Especially about stuff like: "Circular unit propagates notably faster than Stock when features of MiniSat not related to unit propagation were removed" --> it's not so hard to make MiniSat do more prop/s if you remove stuff not related to unit propagation.

capiman commented 10 years ago

Regarding which data types used: On page 16 and 17 (especially footnote of page 17) he wrote:

"Instances from the SAT 2005 competition (Le Berre & Simon, 2006) were used." and footnote 5

"http://www.lri.fr/~simon/contest/results/download/distrib-benchs-random-sat2005.tar.bz2, distrib-benchs-crafted-sat2005.tar.bz2, and distrib-benchs-industrial-sat2005.tar.bz2."

msoos commented 10 years ago

Yeah, I read his email to the MiniSat mailing list. Once he turned on learning, all speedup was gone. Closing. :(