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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
|
================ CHANGES TO THE ORIGINAL CODE ==================================
The only CVC4 connections passed to minisat are the proxy (defined in sat.h) and
the context. The context is obtained from the SmtEngine, and the proxy is an
intermediary class that has all-access to the SatSolver so as to simplify the
interface to (possible) other sat solvers. These two are passed to minisat at
construction time and some additional flags are set. We use the SimpSolver
solver with simplifications.
To compare with original minisat code in SVN you can compare to revision 6 on
the trunk.
The PropEngine then uses the following
// Create the sat solver (this is the proxy, which will create minisat)
d_satSolver = new SatSolver(this, d_theoryEngine, d_context);
// Add some clauses
d_cnfStream->convertAndAssert(node);
// Check for satisfiabilty
bool result = d_satSolver->solve();
* Adding theory literals:
The newVar method has been changed from
Var Solver::newVar(bool sign, bool dvar)
to
Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
in order to mark the variables as theory literals. For that purpose there is a
new boolean array called "theory" that is true or false if the variables is for
a theory literal.
* Backtracking/Pushing
Backtracking in minisat is performed through the cancelUntil() method, which is
now modified to pop the context the appropriate number of times.
Minisat pushes the scope in the newDecisionLevel() method where we appropriately
also push the CVC4 context.
* Phase caching
In order to implement phase-caching (RSAT paper) we
(1) flag minisat to use the user-provided polarities first by setting the
minisat::SimpSolver::polarity_user flag when initializing the solver (in sat.h)
(2) when a variable is set (in uncheckedEnqueue()) we remember the value in the
"polarity" table.
* Asserting the theory literals
In the uncheckedEnqueue() method, if the literal is a theory literal (looking
in the "theory" table), it is passed to the prop engine thorough the proxy.
* Theory propagation (checking)
The BCP propagation method was changed from propagate to propagateBool and
another method propagateTheory is defined to do the theory propagation. The
propagate method now looks like
Clause* Solver::propagate()
{
Clause* confl = NULL;
while(qhead < trail.size()) {
confl = propagateBool();
if (confl != NULL) break;
confl = propagateTheory();
if (confl != NULL) break;
}
return confl;
}
The propagateBool method will perform the BCP on the newly assigned variables
in the trail, and if a conflict is found it will break. Otherwise, the theory
propagation is given a chance to check for satisfiability and maybe enqueue some
additional propagated literals.
* Conflict resolution
If a conflict is detected during theory propagation we can rely on the minisat
conflict resolution with a twist. Since a theory can return a conflict where
all literals are assigned at a level lower than the current level, we must
backtrack to the highest level of any literal in the conflict. This is done
already in the propagateTheory().
* Clause simplification
Minisat performs some simplifications on the clause database:
(1) variable elimination
(2) subsumtion
Subsumtion is complete even with theory reasoning, but eliminating theory
literals by resolution might be incomplete:
(x = 0 \vee x = 1) \wedge (x != 1 \vee y = 1) \wedge x = y
^^^^^ ^^^^^^
v ~v
would, after eliminating v, simplify to
(x = 0) wedge (y = 1) wedge (x = y) which is unsatisfiable
while x = 1, y = 1 is a satisfying assignment for the above.
Minisat does not perform variable elimination on the variables that are marked
as frozen (in the "frozen", SimSolver.h) table. We put all the theory literals
in the frozen table, which solves the incompleteness problem.
================ NOTES =========================================================
* Accessing the internals of the SAT solver
The non-public parts of the SAT solver are accessed via the static methods in
the SatSolver class. SatSolverProxy is declared as a friend of the
SatSolver and has all-privileges access to the internals -- use with care!!!
* Clause Database and CNF
The clause database consists of two parts:
vec<Clause*> clauses; // List of problem clauses.
vec<Clause*> learnts; // List of learnt clauses.
Clauses is the original problem clauses, and learnts are the clauses learned
during the search. I have disabled removal of satisfied problem clauses by
setting the remove_satisfied flag to false.
The learnt clauses get removed every once in a while by removing the half of
clauses with the low activity (reduceDB())
Since the clause database backtracks with the SMT solver, the CNF cache should
be context dependent and everything will be in sync.
* Adding a Clause
The only method in the interface that allows addition of clauses in MiniSAT is
bool Solver::addClause(vec<Lit>& ps),
but it only adds the problem clauses.
In order to add the clauses to the removable database the interface is now
bool Solver::addClause(vec<Lit>& ps, bool removable).
Clauses added with removable=true might get removed by the SAT solver when
compacting the database.
The question is whether to add the propagation/conflict lemmas as removable or
not?
* Literal Activities
We do not backtrack literal activities. This does not semantically change the
equivalence of the context, but does change solve times if the same problem is
run several times.
* Do we need to assign literals that only appear in satisfied clauses?
|
