diff options
Diffstat (limited to 'src/prop/minisat/doc/ReleaseNotes-2.2.0.txt')
-rw-r--r-- | src/prop/minisat/doc/ReleaseNotes-2.2.0.txt | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/src/prop/minisat/doc/ReleaseNotes-2.2.0.txt b/src/prop/minisat/doc/ReleaseNotes-2.2.0.txt new file mode 100644 index 000000000..7f084de2b --- /dev/null +++ b/src/prop/minisat/doc/ReleaseNotes-2.2.0.txt @@ -0,0 +1,79 @@ +Release Notes for MiniSat 2.2.0 +=============================== + +Changes since version 2.0: + + * Started using a more standard release numbering. + + * Includes some now well-known heuristics: phase-saving and luby + restarts. The old heuristics are still present and can be activated + if needed. + + * Detection/Handling of out-of-memory and vector capacity + overflow. This is fairly new and relatively untested. + + * Simple resource controls: CPU-time, memory, number of + conflicts/decisions. + + * CPU-time limiting is implemented by a more general, but simple, + asynchronous interruption feature. This means that the solving + procedure can be interrupted from another thread or in a signal + handler. + + * Improved portability with respect to building on Solaris and with + Visual Studio. This is not regularly tested and chances are that + this have been broken since, but should be fairly easy to fix if + so. + + * Changed C++ file-extention to the less problematic ".cc". + + * Source code is now namespace-protected + + * Introducing a new Clause Memory Allocator that brings reduced + memory consumption on 64-bit architechtures and improved + performance (to some extent). The allocator uses a region-based + approach were all references to clauses are represented as a 32-bit + index into a global memory region that contains all clauses. To + free up and compact memory it uses a simple copying garbage + collector. + + * Improved unit-propagation by Blocking Literals. For each entry in + the watcher lists, pair the pointer to a clause with some + (arbitrary) literal from the clause. The idea is that if the + literal is currently true (i.e. the clause is satisfied) the + watchers of the clause does not need to be altered. This can thus + be detected without touching the clause's memory at all. As often + as can be done cheaply, the blocking literal for entries to the + watcher list of a literal 'p' is set to the other literal watched + in the corresponding clause. + + * Basic command-line/option handling system. Makes it easy to specify + options in the class that they affect, and whenever that class is + used in an executable, parsing of options and help messages are + brought in automatically. + + * General clean-up and various minor bug-fixes. + + * Changed implementation of variable-elimination/model-extension: + + - The interface is changed so that arbitrary remembering is no longer + possible. If you need to mention some variable again in the future, + this variable has to be frozen. + + - When eliminating a variable, only clauses that contain the variable + with one sign is necessary to store. Thereby making the other sign + a "default" value when extending models. + + - The memory consumption for eliminated clauses is further improved + by storing all eliminated clauses in a single contiguous vector. + + * Some common utility code (I/O, Parsing, CPU-time, etc) is ripped + out and placed in a separate "utils" directory. + + * The DIMACS parse is refactored so that it can be reused in other + applications (not very elegant, but at least possible). + + * Some simple improvements to scalability of preprocessing, using + more lazy clause removal from data-structures and a couple of + ad-hoc limits (the longest clause that can be produced in variable + elimination, and the longest clause used in backward subsumption). |