SAT求解器minisat

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