abc/src/sat/bsat2/ReleaseNotes-2.2.0.txt

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