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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
Release Notes for MiniSat 2.2.0
===============================
Changes since version 2.0:
* Started using a more standard release numbering.
* Includes some now well-known heuristics: phase-saving and luby
restarts. The old heuristics are still present and can be activated
if needed.
* Detection/Handling of out-of-memory and vector capacity
overflow. This is fairly new and relatively untested.
* Simple resource controls: CPU-time, memory, number of
conflicts/decisions.
* CPU-time limiting is implemented by a more general, but simple,
asynchronous interruption feature. This means that the solving
procedure can be interrupted from another thread or in a signal
handler.
* Improved portability with respect to building on Solaris and with
Visual Studio. This is not regularly tested and chances are that
this have been broken since, but should be fairly easy to fix if
so.
* Changed C++ file-extention to the less problematic ".cc".
* Source code is now namespace-protected
* Introducing a new Clause Memory Allocator that brings reduced
memory consumption on 64-bit architechtures and improved
performance (to some extent). The allocator uses a region-based
approach were all references to clauses are represented as a 32-bit
index into a global memory region that contains all clauses. To
free up and compact memory it uses a simple copying garbage
collector.
* Improved unit-propagation by Blocking Literals. For each entry in
the watcher lists, pair the pointer to a clause with some
(arbitrary) literal from the clause. The idea is that if the
literal is currently true (i.e. the clause is satisfied) the
watchers of the clause does not need to be altered. This can thus
be detected without touching the clause's memory at all. As often
as can be done cheaply, the blocking literal for entries to the
watcher list of a literal 'p' is set to the other literal watched
in the corresponding clause.
* Basic command-line/option handling system. Makes it easy to specify
options in the class that they affect, and whenever that class is
used in an executable, parsing of options and help messages are
brought in automatically.
* General clean-up and various minor bug-fixes.
* Changed implementation of variable-elimination/model-extension:
- The interface is changed so that arbitrary remembering is no longer
possible. If you need to mention some variable again in the future,
this variable has to be frozen.
- When eliminating a variable, only clauses that contain the variable
with one sign is necessary to store. Thereby making the other sign
a "default" value when extending models.
- The memory consumption for eliminated clauses is further improved
by storing all eliminated clauses in a single contiguous vector.
* Some common utility code (I/O, Parsing, CPU-time, etc) is ripped
out and placed in a separate "utils" directory.
* The DIMACS parse is refactored so that it can be reused in other
applications (not very elegant, but at least possible).
* Some simple improvements to scalability of preprocessing, using
more lazy clause removal from data-structures and a couple of
ad-hoc limits (the longest clause that can be produced in variable
elimination, and the longest clause used in backward subsumption).
|
