NEWS

ver 3.3 9/07/2013
-> git rev 6138d6b30ede0cd2f11477aa4487f887422327b9
* Memory saving whenever possible
* A serious bug with disconnected components and satisfiable instances has
  been solved. Luckily it did not affect UNSAT instances
* A lot of bugs that could have come up if used as a library have been
  fixed. Library usage, however, may still contain bugs, though probably
  very few.

ver 3.2 29/04/2013
-> git rev bcbdc7ff6f2217eb4fb7446a2ee765a79526a7f8
* DRUP support
* fixed a number of variable replacement bugs
* added cache-based Stalmarck detection

ver 3.0 1/03/2011
-> git rev 988b0b3b320e830f7285212f342186b41f04ebf6 
* A redesigned architecture with many options and web statistics

ver 2.9.0 20/01/2011
* Added extended SCC and vivification using cached implications
* Reachability testing and related branching heuristic using cached
  implications
* Corrected subsumption code -- it is now more precise but slower
* Corrected original problem & learnt dumping. Binary clauses were wrongly
  dumped, and xor clauses were never dumped
* Better time-limiting on subsumption, var-elimination, etc.
* When a variable can be eliminated with no resulting clauses, it is elim-ed
* On-the-fly transitive self-subsuming resolution is now carried out based
  on short/long-term average clause sizes and glue numbers
* More stats are printed. CPU times in stats are better in case a recent
  (>2.6.26) version of the Linux kernel is used.
* Multi-threaded solving is no longer default since it hasn't been really
  tested in terms of performance
* Lots of debug code is now enabled by default. It slows down things by
  maybe 5% but keeps the code more sane
* gcc bug 47365  has been found and workaround is automated through the
  configure script. If you build using hand-crafted Makefiles, you will bump
  into this bug for sure.

ver 2.8.0beta5 2/11/2010
* reason[] was taken to be correct, when in fact it is not updated during
  canceling
* Subsumer::unEliminate() erased iterators from std::map that was not inside
  the map

ver 2.8.0beta4 31/10/2010
* class Watched is now tuned more towards operations that are executed 
  more. These now require no bit-shifting
* Bug fix: debug code left in from DimacsParser removed

ver 2.8.0beta3 30/10/2010
* Bug in hand-coded Tarjan's algorithm. We were manipulating the watchlists
  while using them. This lead to a segfault.
* Bug in replace() -- we were using replace(), but the clauses were not always
  attached (e.g. in ClauseDetacherReattacher) and so the added binary clause
  was not always l_Undef,l_Undef. A very subtle bug that could have caused
  solution-sanity problems
* Fixed bug with opening fileno(stdin)

ver 2.8.0beta2 28/10/2010
* Boost dependency removed through implementation of Tarjan's algorithm by
  hand. This also implies a much reduced memory footprint in case there were
  many binary clauses

ver 2.8.0beta1 27/10/2010
* Binary clauses are now implicit. This allows for _very_ large problems
  that contain mostly only binary clauses to work surprisingly well in terms
  of subsumption and self-subsuming resolution. Also, variable elimination
  should now be possible for these clauses (been tested problem with 120
  million binary clauses)
* Due to implicit binary clauses, we use Tarjan's algorithm, currently
  from Boost -- this dependency will be removed soon
* A preliminary multi-threading is possible. Unitary and binary clauses are
  shared between the threads at regular intervals. Threading is with OpenMP
  which should be available for all platforms
* Lots and lots of bugfixes. On many occasions, clauses and xor-clauses have
  been inserted into the watchlists when these clauses' variables were
  fixed, leading to some very bad effects.

ver 2.7.1 -- 10/10/2010
* Bug in DIMACS-parsing fixed. We couldn't read back the dumped clauses'
  learnt state properly, which lead to parsing problems. Thanks to
  Vlastislav Weiner for reporting this

ver 2.7.0 -- 5/10/2010
* Lots of documentation added. At least 1500 lines of in-line documentation
  is now available. This documentation can be extracted using the Doxygen
  tool
* Transitive on-the-fly self-subsuming resolution added for short clauses
  at the beginning of the solving (<80 million conflict literals).
* Preliminary learnt-clause parsing -- the dumped learnt clauses are now
  correctly parsed up to be learnt, and hence a preliminary of stop-
  solving & restart-solving cycle can be created
* Memory manager has been debugged. It was segfaulting on certain large
  instances. (thanks to Rob None for the multiple bug reports)
* Memory manager no longer needs to keep a map of old clauses<-> new
  clauses. This is now a direct-access table, speeding up memory
  consolidation considerably

ver 2.6.0 -- 16/08/2010
* No more separate watchlists for binary clauses. Class "Watched" knows
  what it watches. This reduces memory overhead, and reduces jump-around
  in code and data.
* Tertiary clauses are handled natively inside the watchlists just like
  binary clauses
* Watchlists are sorted to propagate binary clauses first, and tertiary
  clauses next, finally to propagate normal and xor clauses
* Clause subsumption has finally been cleared of a number of bugs. We now
  subsume with learnt clauses on a regular basis.
* 32-bit pointers are no longer used. Instead, a stack-based implementation
  is used, on the lines of the description of the solver lingeling by
  Armin Biere. This leads to minimal (~6%) speedup relative to the original
  scheme in CryptoMiniSat 2.5.1, but it enables 32-bit pointers on all
  architectures
* Asymmetric branching is now used. Clauses are sorted according to size,
  and the largest ones are shortened with asymm-branching. This brings
  large benefits, as often the largest clauses are responsible for a good
  number of the literals in the learnt clauses. Asymmetric branching thus
  reduces the learnt clause sizes, increasing their potential and making
  propagation faster
* On-the-fly self-subsuming resolution of learnt clauses is used to
  shorten them even further using binary and tertiary (i.e. natively
  stored) clauses.
* Since tertiary clauses are first to propagate after binary clauses, the
  number of tertiary clauses propagating is higher, leading to even less
  literals in the learnt clauses
* Printing has been updated. It is still not perfect, but we are making
  progress.
* Known regressions: xor clauses could potentially be propagated somewhat
  slower, statistics generator is currently broken

ver 2.5.2 -- 8/06/2010
* Fixing serious bug with xor-cutting. We no longer segfault if there are
  many XORs in the given problem

ver 2.5.1 -- 8/06/2010 --- 'The Obvious Child'
* Printing updates: everyting is printed much more nicely now
* Approximated degrees of literals in binary graph are not reset between
  calculations

ver 2.5.0 -- 7/06/2010 (SAT Race'10 version)
* A lot of performance bugs have been fixed. Activities of clauses were wrongly
  updated with their abstract representation during subsumtion for example.
  Also, we now use a well-tested set of magic constants instead of making
  them up using intuition. Apparently, intuition in the field of SAT leads
  to headaches and (in severe cases) to dementia.
* A lot of code has been added regarding binary clause graphs. It is now
  regularly cleaned from useless binary clauses. Also, the useless binary
  clauses are regularly generated to subsume and strenghthen other clauses
  with them -- and once used, these useless binary clauses are thrown away.
* Hyper-binary clauses are now generated using an algorithm relying purely
  on the datastrucures available in modern SAT solvers -- i.e. the fact that
  binary clauses have their own watchlists, and so allow for efficient
  propagation of the binary clauses separately from other clauses.

ver 2.4.2 -- 9/05/2010
* Gaussian elimination has finally been fixed. It can now be tried out with
  the command-line switch "--gaussuntil=X", where X is the maximum depth. I
  usually set 100, but this is probably a wrong default. You should experiment
  with your own cipher. NOTE: Gauss is still experimental. If it segfaults,
  please file a bug.
* The solver can now print out all the solutions to a problem. Simply use the
  "--maxsolutions=X" option, where X is the maximum number of solutions you
  need. You may use this option in conjunction with the very experimental
  "--greedyunbound" which unassigns some variables in such a way that the
  given solution is still correct, but some variables may not appear in it.
* Command line switches have been corrected. They are now all lower-case and
  use the prefix "--" instead of "-"

ver 2.4.1 -- 30/04/2010
Serious bug fixed that read data from change memory in subsume0, and
hyper-binary resolution has been disabled, since it caused satisfiable
instances to become unsatisfiable.

ver 2.4.0 -- 26/04/2010
The first real release of CryptoMiniSat v2. It contains the following set
of improvements:
    * XOR clauses are extracted at the beginning of the solving
    * Anti- or equivalent variables are detected at regular intervals
      and are replaced with one another, eliminating variables during
      solving
    * xor-clauses are regularly XOR-ed with one another such as to obtain
      binary XOR clauses. These binary xor-clauses are then treated as variable
      replacements instructions (i.e. "v1 XOR v2 = false" means that v1 is
      replaced with v2)
    * Phase calculation using Jeroslow and Wang, and phase saving with
      randomised search space exploration. The average branch depth is
      measured for each instance, and the solver makes a random phase
      flip with 1/avgBranchDepth probability
    * Random search burst are used to search unexplored areas of the
      search space at regular intervals
    * Automatic detection of cryptographic and industrial instances. Dynamic
      restart is used for industrial instances, and static restart for
      cryptographical instances. Detection is based on xor-clause percentage
      and variable activity stability.
    * Regular full restarts are performed to detect if the problem hasn't
      changed enough due to learnt clauses and assigned variables to behave
      more like a cryptographical instance than an industrial instance or
      vice-versa.
    * Both GLUCOSE-type learnt clause activity and MiniSat-type learnt clause
      activity heuristics are supported. During dynamic restarts, the GLUCOSE
      heuristic is used, while during static restarts, the MiniSat-type
      heuristic is used.
    * SatELite-type variable elimination, clause subsumption and clause
      strengthening is regularly performed. The occurrence lists are, however,
      not updated all the time such as the case is with PrecoSat. Instead,
      occurrences are calculated on per-use basis
    * On-the-fly subsumption is used to check whether the conflict clause
      automatically subsumes the clause that caused the conflict.
    * Binary clauses are propagated first before non-binary clauses are
      propagated.
    * 32-bit pointers are used for the watchlists on 64-bit architectures,
      using out the fact that most bits in the 64-bit pointer are actually fixed
    * Hyper-binary resolution is used when the hyper-binary clause subsumes
      any of the original clauses
    * Clauses are regularly scrubbed from variables that have been assigned
    * Preliminary blocked-clause elimination is used to remove pure literals
    * Distinct subproblems are regularly searched for and detected. These
      subproblems and solved with subsolvers. As a side-ntoe, this eliminates
      the original theoretical need for phase-saving (enabling the random
      flipping of phase, which is also used)
    * xor-clause subsumption is regularly performed
    * So-called dependent variables are removed along with their xor-clauses.
      This means that variables that only occur in one xor-clause and in no
      other clause are removed along with the XOR clause. Once the solving has
      finished, this xor-clause is re-introduced and a suitable value for the
      variable is found to satisfy the XOR.
    * Failed variable probing with both-propagated and binary XOR detection.
      All variables are successively propagated both to TRUE and FALSE. If one
      of these branches fails, the variable is assigned the other branch.
      If none fails, but the intersection of assignments is non-empty, those
      assignments are made. Essentially the same is done to non-binary XOR-s:
      if both v and !v propagate a given binary XOR, that XOR is learnt.
    * Designed to work as a library and as a drop-in replacement for MiniSat

ver 2.3.2 -- 28/12/2009
* further ints have been replaced with uints
* ZLIB can now be disabled
* Visual C++ 2008 can now compile the sources
* Statistics generation is much faster
  (thanks to Martin Maurer for spotting this)

ver 2.3.0 -- 17/12/2009
* binary learnts are converted to 2-long xors if possible, and eliminated
* lots of heuristics tuning
* Cleanclauses is now default instead of removeSatisfied in simplify()
* Stable in case used as a library
* Lots of regression tests added
* Cleaner logging
* ints have been replaced with uints (less warnings with -Wall)
* a lot of speedups for gauss -- packed, multi-matrix representation

ver 2.2 -- 20/11/2009
* xor-clause finding
* matrix finding
* var-replacing
* heuristics to disable gauss
* much better+cleaner stats generation (e.g. fcopy.cpp removed)
* lots of bug-fixing
* satelite added, with cryptominisat_ext.sh as a wrapper script

ver 2.1.1 -- 30/10/2009
* Learnt clause distribution stats
* Added regression testing

ver 2.1.0 -- 28/10/2009
* hand-made (non-GPL Bignum) packed representation of both matrix' rows
* removed dependency on GPL Bignum library

ver 2.0.1 -- 24/10/2009
* Added Gaussian elimination

ver 1.2.6 -- 24/10/2009
* Corrected unitialised maxRestarts


ver 1.2.6 -- 24/10/2009
* Corrected unitialised maxRestarts

ver 1.2.5 -- 24/10/2009
* Maximum restarts can be configured
* Better verbose debug printing

ver 1.2.4 -- 22/10/2009
* CryptoMiniSat is printed as the first line of the program
  (instead of "This is MiniSat 2.0 beta")

ver 1.2.3 -- 22/10/2009
* better README file
* better use of the automake autoconf toolchain

ver 1.2.2 -- 22/10/2009
* phase saving added (thank you, glucose solver team)
* better printing of statistics
* better explanation of statistics
* accept 'v' and 'var', 'g' and 'group'
* better parsing of 'v','var' and 'g','group'
* don't allow too long group and variable names
* branch length distribution added
* better Makefile.cvs
* cmake option added
* updated INSTALL instructions
* '-march=native' is default when using cmake

ver 1.1 -- 29/04/2009
* Renamed to CryptoMiniSat

ver 1.0 -- 15/04/2009
* Some updated statistics! Now average rank of guessed var is shown