src/HOL/Tools/sat_solver.ML
2006-09-02 ago zchaff_with_proofs: proof is a reference now
2006-08-31 ago read_dimacs_cnf_file ignores more comment lines
2006-07-19 ago MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
2006-07-17 ago butlast removed (use fst o split_last instead)
2006-07-17 ago support for MiniSat proof traces added
2006-07-07 ago added support for MiniSat 1.14
2006-03-05 ago fixed a typo in a comment
2006-01-14 ago sane ERROR handling;
2005-09-24 ago bugfix in "zchaff_with_proofs"
2005-09-24 ago parse_std_result_file renamed to read_std_result_file
2005-09-22 ago solver "auto" does not reverse the list of solvers anymore
2005-09-21 ago zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
2005-09-21 ago introduced AList module
2005-09-20 ago bugfix in "zchaff_with_proofs"
2005-09-20 ago using curried Inttab.update_new function now
2005-09-19 ago SAT solver interface modified to support proofs of unsatisfiability
2005-07-26 ago write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
2005-07-26 ago replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
2005-07-26 ago write_dimacs_sat_file writes outer parentheses again
2005-07-26 ago replaced calls to PropLogic.defcnf by PropLogic.auxcnf
2005-07-21 ago write_dimacs_sat_file now generates slightly smaller files
2005-06-05 ago replaced File.sysify_path by Path.pack;
2005-03-11 ago minor Library.option related modifications
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-11-25 ago added ZCHAFF_VERSION
2004-11-24 ago Removed a "Matches are not exhaustive" warning
2004-11-23 ago external solvers may now overwrite existing temporary files
2004-11-19 ago solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
2004-08-14 ago bugfix in read_dimacs_cnf_file
2004-07-12 ago read_dimacs_cnf_file added
2004-06-22 ago faster conversion into DIMACS CNF and DIMACS SAT format
2004-06-17 ago new SAT solver interface
2004-05-26 ago solver "auto" now issues a warning when it uses solver "enumerate"
2004-05-17 ago Comments fixed
2004-05-04 ago redundant clause removed
2004-04-02 ago fixed dpll solver (now uses NNF)
2004-03-26 ago satsolver=dpll
2004-03-26 ago Installed solvers now determined at call time (as opposed to compile time)
2004-03-11 ago SML/NJ compatibility fixes
2004-03-10 ago Internal and external SAT solvers