1 news for release 91x since 846
2 ------------------------------
4 * propagation of binary clauses until completion
6 * fixed API usage 'assume;sat;sat'
8 * literals move to front (LMTF) during traversal of visited clauses
10 * switched from inner/outer to Luby style restart scheduling
12 * less agressive reduce schedule
14 * replaced watched literals with head and tail pointers
16 * add 'picosat_failed_assumption', which allows to avoid tracing and core
17 generation, if one is only interested in assumptions in the core
19 * fixed a BUG in the generic iterator code of clauses
20 (should rarely happen unless you use a very sophisticated malloc lib)
22 news for release 846 since 632
23 ------------------------------
25 * cleaned up assumption handling (actually removed buggy optimization)
27 * incremental core generation
29 * experimental 'all different constraint' handling as in our FMCAD'08 paper
33 - picosat_add_ado_lit (add all different object literal)
34 - picosat_deref_top_level (deref top level assignment)
35 - picosat_changed (check whether extension was possible)
36 - picosat_measure_all_calls (per default do not measure adding time)
37 - picosat_set_prefix (set prefix for messages)
39 * 64 bit port (and compilation options)
41 * optional NVSIDS visualization code
43 * resource controlled failed literal implementation
45 * disconnect long clauses satisfied at lower decision level
47 * controlling restarts