ver 2.9.8
* Fixed problems with Gaussian elimination in case assumptions were used
ver 2.9.7
* Adding missing function definitions
* Converting all 3-long XORs into 4-long XORs before dumping simplified
problem
ver 2.9.6
* Better handling of memory
* Returning a vector of clauses with dumpOrigClauses()
* Counting number of lines read from CNF to give better error reporting
ver 2.9.5
* License is now MIT
* Moved all files under Solver
* Fixed some problems in Makefile -- thanks to Martin Albrecht for this
suggestion
ver 2.9.4 17/04/2012
* Fixed bug with size()/2 for blocked literal that was nondeterministic
Thanks to Philipp Jovanovic for this
* Fixed bug with uncomputed abstraction for clauses
ver 2.9.3 14/04/2012
* Fixed bug where execution was nondeterministic if used as a library
* Fixed bug where we went into an infinite loop after 48 hours when using
static restarts. Thanks to Philipp Jovanovic for this
* Fixed building issues with DISABLE_ZIP
ver 2.9.2 22/01/2012
Bugfixes:
* Bug in --maxsolutions fixed thanks to Martin Maurer
* CalcDefPolars was taking >10% time for certain problems. Fixed thanks to
Vegard Nossum
* Bug in StateSaver of saving&restoring double to unsigned fixed thanks to
Martin Maurer
* Cache cleaning is finally fixed
* Disabling part-finding as it made us loose 3+ points at SAT Comp'11
* Clauses after empty comments sometimes weren't parsed. Thanks to Remy Delmas
for noticing this
* Solutions were sometimes incorrect when using --maxsolutions=X
* Random variable picking was turned off after a short while. Thanks to
Martin Maurer for noticing this
* XOR-to-normal clause converting routine was buggy
* Failed literal probing's hyper-binary resolution engine was taking too
much time
* Performance regressions relative to branch that went into SatComp'11
have been worked on
* FPU check problem fixed thanks to Jerry James
* Printing problems related to multi-threading and startup in Main.cpp
fixed. Thanks to Martin Maurer for reporting this.
Improvements:
* Manpage thanks to Jerry James
* We don't exit(-1) any more, instead, whe throw. Thanks to Jerry James for
this
* Time-limiting in subsumption+strengthening+var-elim was not sufficient
* "strengthened" qualifier removed from Clause
* Way better subsumption+strengthening with 2- and 3-long clauses.
* Cache cleaning
ver 2.9.1 26/05/2011
* Subsumption is now in one go instead handling learnt&non-learnt in different
runs.
* Hyper-bin resolution is fixed(?). The algorithm has become too complex to
tell if it's correct -- a complete rewrite will be made for the next version
* Lots of Gaussian bugs have been fixed -- thanks go to Vegard Nossum
* A lot of compilation issues have been fixed to the point that the program
now compiles with "-pedantic -Wall -Werror" on many different systems.
Thanks for this go to: Martin Albrecht, Robert Aston, Martin Maurer, Vegard
Nossum and others on the CryptoMiniSat mailing list
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
