diff options
Diffstat (limited to 'src/prop/cryptominisat/NEWS')
| -rw-r--r-- | src/prop/cryptominisat/NEWS | 334 |
1 files changed, 334 insertions, 0 deletions
diff --git a/src/prop/cryptominisat/NEWS b/src/prop/cryptominisat/NEWS new file mode 100644 index 000000000..48494c540 --- /dev/null +++ b/src/prop/cryptominisat/NEWS @@ -0,0 +1,334 @@ +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 |