ver 2.9.2 22/01/2011 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