Cabal package minisat-solver 0.1 Released Oct. 24nd 2016
========================================
* Modified by Peter Selinger to export the solutions via API, rather than
printing them to stdout.
* Modified by Peter Selinger for coding style and removed some dead code.
bc_minisat_all v1.1.0 Released Sep. 30th 2015
========================================
* Supported solution counting with GMP library.
* Supported interruption signal handling and deleted timelimit-related functionality instead.
* Changed names of some macros.
* Added functionality for continuing search by simulating the previous decisions after backtracking to the root level.
bc_minisat_all v1.0.0 Released Jul. 27th 2015
========================================
* Generalization is now renamed to simplification, and several bugs are fixed in the simplification part.
* Furthermore, the following change was made:
** The former part of simplification is implemented by traversing implication graph, which is more efficient than scanning the whole CNF.
** The latter part is organized and some bugs are corrected.
* Added functionality for setting timelimit and periodically reporting progress.
* Added functionality for including GNU MP bignum library so that a huge number of solutions can be precisely counted.
* Fixed the bug of not handling the case that blocking clases happen to be empty in solver_search().
* Deleted solver_generalize_naive() because it is useless.
minisat_all v2.0.1 Released Jun. 23rd 2015
========================================
* Added a license description (LICENSE.minisat_all).
minisat_all v2.0.0 Released April 30th 2015
========================================
* Fixed the bug of inserting a problem line by wrongly calling fseek in solver_solve().
** Problem line is no longer inserted.
* Improved a blocking clause computation according to the following paper:
** Y. Yu, P. Subramanyan, N. Tsiskaridze, S. Malik: "All-SAT using Minimal Blocking Clauses", in Proc. of the 27th International Conference on VLSI Design and the 13th International Conference on Embedded Systems, pp.86-91, 2014.
minisat_all v1.0.0 Released April 16th 2015
========================================
* This software computes the following problem , which is called ALLSAT.
INPUT: a CNF (given in DIMACS CNF format) of a Boolean function f
OUTPUT: all satisying assignments to the CNF.
* Installation
Executing make in the top directory.
* Usage
$ minisat_all in.dat (out.dat)
* If you just want to obtain a list of all satisfying assignments, specify output file as above.
Then all assignments are written in DIMACS CNF format.
* This software is a common implementation of ALLSAT solver using SAT solver
* Two generalization methods of found solutions are implemented: see the two functions solver_generalize_faster and solver_generalize_naive in solver.c.
* They can be switched by defining macro in Makefile
* Also, another method without generalization is implemented, which is just to avoid rediscovery of found solutions.
* Contact
Takahisa Toda <toda.takahisa(at)gmail.com>
Graduate School of Information Systems, the University of Electro-Communications
1-5-1 Chofugaoka, Chofu, Tokyo 182-8585, Japan
MiniSat-C v1.14.1
========================================
* Fixed some serious bugs.
* Tweaked to be Visual Studio friendly (by Alan Mishchenko).
This disabled reading of gzipped DIMACS files and signal handling, but none
of these features are essential (and easy to re-enable, if wanted).
MiniSat-C v1.14
========================================
Ok, we get it. You hate C++. You hate templates. We agree; C++ is a
seriously messed up language. Although we are more pragmatic about the
quirks and maldesigns in C++, we sympathize with you. So here is a
pure C version of MiniSat, put together by Niklas Sörensson.