aboutsummaryrefslogtreecommitdiff
path: root/scripts/picosat-959/NEWS
diff options
context:
space:
mode:
authorKarel Kočí <cynerd@email.cz>2015-05-05 11:58:26 +0200
committerKarel Kočí <cynerd@email.cz>2015-05-05 11:58:26 +0200
commitdfe47d067a70f9781e3b431f6a685090bf87ff40 (patch)
tree5151ba40cdd422e9f9bbbba0398b2a569ba88311 /scripts/picosat-959/NEWS
parent289b0ce128cdca79676307646eef3d56c25c6dd2 (diff)
downloadlinux-conf-perf-dfe47d067a70f9781e3b431f6a685090bf87ff40.tar.gz
linux-conf-perf-dfe47d067a70f9781e3b431f6a685090bf87ff40.tar.bz2
linux-conf-perf-dfe47d067a70f9781e3b431f6a685090bf87ff40.zip
Add picosat version 959
Diffstat (limited to 'scripts/picosat-959/NEWS')
-rw-r--r--scripts/picosat-959/NEWS148
1 files changed, 148 insertions, 0 deletions
diff --git a/scripts/picosat-959/NEWS b/scripts/picosat-959/NEWS
new file mode 100644
index 0000000..4e9d76f
--- /dev/null
+++ b/scripts/picosat-959/NEWS
@@ -0,0 +1,148 @@
+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 <failedlits>' 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