1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
news for release 91x since 846
------------------------------
* 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
|
