diff options
Diffstat (limited to 'src/prop/bvminisat/doc/ReleaseNotes-2.2.0.txt')
| -rw-r--r-- | src/prop/bvminisat/doc/ReleaseNotes-2.2.0.txt | 79 |
1 files changed, 0 insertions, 79 deletions
diff --git a/src/prop/bvminisat/doc/ReleaseNotes-2.2.0.txt b/src/prop/bvminisat/doc/ReleaseNotes-2.2.0.txt deleted file mode 100644 index 7f084de2b..000000000 --- a/src/prop/bvminisat/doc/ReleaseNotes-2.2.0.txt +++ /dev/null @@ -1,79 +0,0 @@ -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). |