-
Notifications
You must be signed in to change notification settings - Fork 1
MiniSat v1.14
License
msoos/minisat-v1.14
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
MiniSat v1.14 / MiniSat-p v1.14 ======================================== This version is a cleaned up version of the MiniSat solver entering the SAT 2005 competition. Some of the most low-level optimization has been removed for the sake of clarity, resulting in a 5-10% performance degradation. The guard on "too-many-calls" in 'simplifyDB()' has also been improved. If uttermost performance is needed, use the competition version, also available at the MiniSat page (www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/). Several things has changed inside MiniSat since the first version, documented in the paper "An Extensible SAT Solver". The most important is the lack of support for non-clausal constraints in this version. Please use MiniSat v1.12b if you need this. Other changes are special treatment of binary clauses for efficiency (messes up the code a bit, but gives quite a speedup), improved variable order (still VSIDS based, but works MUCH better than in previous MiniSat versions!), conflict clause minimization (by Niklas Sörensson), and a better Main module (for those of you who use MiniSat as a stand-alone solver). The MiniSat-p version also supports proof logging, sacrificing the binary clauses trick for clarity (some 10-20% slower). For scalability, we decided to keep the proof only on disk. This frees up memory for the working set of conflict clauses, and allows for bigger-than-memory proofs to be produced (which can happen, even if you garbage collect the proof). For information about upcomming changes, please review the TODO file.
About
MiniSat v1.14
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published