backends/picosat/NEWS

   1 news for release 91x since 846
   2 ------------------------------
   3
   4 * propagation of binary clauses until completion
   5
   6 * fixed API usage 'assume;sat;sat'
   7
   8 * literals move to front (LMTF) during traversal of visited clauses
   9
  10 * switched from inner/outer to Luby style restart scheduling
  11
  12 * less agressive reduce schedule
  13
  14 * replaced watched literals with head and tail pointers
  15
  16 * add 'picosat_failed_assumption', which allows to avoid tracing and core
  17   generation, if one is only interested in assumptions in the core
  18
  19 * fixed a BUG in the generic iterator code of clauses
  20   (should rarely happen unless you use a very sophisticated malloc lib)
  21
  22 news for release 846 since 632
  23 ------------------------------
  24
  25 * cleaned up assumption handling (actually removed buggy optimization)
  26
  27 * incremental core generation
  28
  29 * experimental 'all different constraint' handling as in our FMCAD'08 paper
  30
  31 * new API calls:
  32
  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)
  38
  39 * 64 bit port (and compilation options)
  40
  41 * optional NVSIDS visualization code
  42
  43 * resource controlled failed literal implementation
  44
  45 * disconnect long clauses satisfied at lower decision level
  46
  47 * controlling restarts