news for release 965 since 959 ------------------------------ * ADC code works again (spotted by Himanshu Jain) * include into R projects (with Christoph Muessel) (--rcode) * fixed 'undefined' + 'ptrdiff_' issues (thanks to Christoph Muessel) * added 'picosat_set_interrupt' and '-a ' command line option * fixed various issues pointed out by Stefan Hengelein: - fixed incremental usage of 'picosat_adjust' - added CPP fixes (STATS, NO_BINARY_CLAUSE versus TRACE mix-ups) - removed redundant explicit set to zero on reset * fixed various usage bugs with 'picomus' (thanks to Stefan Hengelein) * removed '-fno-strict-aliasing' (thanks to Jerry James) news for release 959 since 953 ------------------------------ * fixed header comments * fixed minor compilation issues * fixed unitialized memory access problem for 'picosat_deref_partial' and another issue with partial models * added 'picosat_add_arg' and 'picosat_add_lits' * '--plain' and 'picosat_set_plain' to disable failed literal probing * new '#define PICOSAT_REENTRANT_API' in 'picosat.h' * added manager so no more global variables (allows multiple instances, requires manager object) news for release 951 since 941 ------------------------------ * cleaned up code (based on comments by Donald Knuth) * lreduce=O(conflicts^.5) * added 'picosat_visits' and 'picosat_decisions' * added '--partial' command line option * added 'picosat_deref_partial' and 'picosat_save_original_clauses' * added 'picomcs' as example for MSS computation news for release 941 since 936 ------------------------------ * added 'picogcnf' * added All-SAT mode ('--all' command line option) * statistics include time spent in failed literal preprocessing (probing) * 'picosat_failed_context' for 'push & pop' (and tested failed assumptions for 'push & pop') * 'picosat_simplify' for forced garbage collection * undefined NFL, defined NADC (= failed literals on, ADC's off) * 'picosat_push' and 'picosat_pop' (beta version) * fixed some issues related to binary clause handling and generating list of failed assumptions news for release 936 since 935 ------------------------------ * simple minimal unsatisfiable core (MUS) extractor 'picomus' (example for using 'picosat_mus_assumptions' and 'picosat_coreclause') * added 'picosat_mus_assumptions' * added 'picosat_{set_}propagations' * new 'int' return value for 'picosat_enable_trace_generation' to check for trace code being compiled news for release 935 since 926 ------------------------------ * added 'picosat_failed_assumptions' (plural) * new '-A ' command line option * fixed failed assumption issues * added 'picosat_remove_learned' * added 'picosat_reset_{phases,scores}' * added 'picosat_set_less_important_lit' * added 'picosat_res' news for release 926 since 846 ------------------------------ * random initial phase (API of 'picosat_set_default_phase' changed) * fixed accumulative failed assumption (multiple times) * fixed missing original clause in core generation with assumptions * fixed debugging code for memory allocation * shared library in addition to static library * removed potential UNKNOWN result without decision limit * added picosat_set_more_important_lit * added picosat_coreclause * propagation of binary clauses until completion * fixed API usage 'assume;sat;sat' * literals move to front (LMTF) during traversal of visited clauses * switched from inner/outer to Luby style restart scheduling * less agressive reduce schedule * replaced watched literals with head and tail pointers * add 'picosat_failed_assumption', which allows to avoid tracing and core generation, if one is only interested in assumptions in the core * fixed a BUG in the generic iterator code of clauses (should rarely happen unless you use a very sophisticated malloc lib) news for release 846 since 632 ------------------------------ * cleaned up assumption handling (actually removed buggy optimization) * incremental core generation * experimental 'all different constraint' handling as in our FMCAD'08 paper * new API calls: - picosat_add_ado_lit (add all different object literal) - picosat_deref_top_level (deref top level assignment) - picosat_changed (check whether extension was possible) - picosat_measure_all_calls (per default do not measure adding time) - picosat_set_prefix (set prefix for messages) * 64 bit port (and compilation options) * optional NVSIDS visualization code * resource controlled failed literal implementation * disconnect long clauses satisfied at lower decision level * controlling restarts