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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
/*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*/
/**
* @file SATSolver.hpp
* Defines class SATSolver.
*/
#ifndef __SATSolver__
#define __SATSolver__
#include "SATLiteral.hpp"
#include "Lib/Random.hpp"
#include "Lib/Stack.hpp"
#include "Lib/VirtualIterator.hpp"
#include <climits>
namespace SAT {
enum class VarAssignment {
TRUE,
FALSE,
DONT_CARE, // to represent partial models
NOT_KNOWN
};
inline std::ostream& operator<<(std::ostream& out, VarAssignment const& a)
{
switch (a) {
case VarAssignment::TRUE: return out << "TRUE";
case VarAssignment::FALSE: return out << "FALSE";
case VarAssignment::DONT_CARE: return out << "DONT_CARE";
case VarAssignment::NOT_KNOWN: return out << "NOT_KNOWN";
default: ASSERTION_VIOLATION; return out << "INVALID STATUS";
}
}
enum class Status {
SATISFIABLE,
UNSATISFIABLE,
/**
* Solving for just a bounded number of conflicts may return UNKNOWN.
**/
UNKNOWN
};
inline std::ostream& operator<<(std::ostream& out, Status const& s)
{
switch (s) {
case Status::SATISFIABLE: return out << "SATISFIABLE";
case Status::UNSATISFIABLE: return out << "UNSATISFIABLE";
case Status::UNKNOWN: return out << "UNKNOWN";
default: ASSERTION_VIOLATION; return out << "INVALID STATUS";
}
}
class SATSolver {
public:
virtual ~SATSolver() = default;
/**
* Add a clause to the solver.
*
* In the clause each variable occurs at most once. (No repeated literals, no tautologies.)
*
* Memory-wise, the clause is NOT owned by the solver. Yet it shouldn't be destroyed while the solver lives.
* TODO: This is not ideal and should be addressed! (reference counting?)
*/
virtual void addClause(SATClause* cl) = 0;
void addClausesIter(SATClauseIterator cit) {
while (cit.hasNext()) {
addClause(cit.next());
}
}
/**
* Solve under the given set of assumptions @b assumps.
*
* If UNSATISFIABLE is returned, a subsequent call to
* failedAssumptions() returns a subset of these
* that are already sufficient for the unsatisfiability.
*
* If conflictCountLimit==0,
* do only unit propagation, if conflictCountLimit==UINT_MAX, do
* full satisfiability check, and for values in between, restrict
* the number of conflicts, and in case it is reached, stop with
* solving and assign the status to UNKNOWN.
*
*/
virtual Status solveUnderAssumptionsLimited(const SATLiteralStack& assumps, unsigned conflictCountLimit) = 0;
/**
* Return a list of failed assumptions from the last solverUnderAssumptions call.
* Assumes the last call returned UNSAT
*
* Usually corresponds to the solver's internal unsat core.
*/
virtual SATLiteralStack failedAssumptions() = 0;
// various shorthands for `solveUnderAssumptionsLimited`
Status solveUnderAssumptions(const SATLiteralStack& assumps, bool onlyPropagate=false) {
return solveUnderAssumptionsLimited(assumps, onlyPropagate ? 0u : UINT_MAX);
}
Status solveLimited(unsigned conflictCountLimit) {
SATLiteralStack assumptions;
return solveUnderAssumptionsLimited(assumptions, conflictCountLimit);
}
Status solve(bool onlyPropagate = false) {
return solveLimited(onlyPropagate ? 0 : std::numeric_limits<unsigned>::max());
}
/**
* If status is @c SATISFIABLE, return assignment of variable @c var
*/
virtual VarAssignment getAssignment(unsigned var) = 0;
/**
* If status is @c SATISFIABLE, return true if the assignment of @c var is
* implied only by unit propagation (i.e. does not depend on any decisions)
*/
virtual bool isZeroImplied(unsigned var) = 0;
/**
* Ensure that clauses mentioning variables 1..newVarCnt can be handled.
*
* See also newVar for a different (and conceptually incompatible)
* way for managing variables in the solver.
*/
virtual void ensureVarCount(unsigned newVarCnt) = 0;
/**
* Allocate a slot for a new (previously unused) variable in the solver
* and return the variable.
*
* Variables start from 1 and keep increasing by 1.
*/
virtual unsigned newVar() = 0;
virtual void suggestPolarity(unsigned var, unsigned pol) = 0;
/**
* Suggest random polarity for variables up to maxVar (inclusive),
* so that the next call to solver will tend to produce
* a different model (provided the status will be satisfiable).
*/
virtual void randomizeForNextAssignment(unsigned maxVar) {
for (unsigned var=1; var <= maxVar; var++) {
suggestPolarity(var,Random::getBit());
}
}
/**
* If status is @c SATISFIABLE, return assignment of variable @c var
*/
bool trueInAssignment(SATLiteral lit)
{
VarAssignment asgn = getAssignment(lit.var());
VarAssignment desired = lit.positive() ? VarAssignment::TRUE : VarAssignment::FALSE;
return asgn==desired;
}
/**
* Apply fixpoint minimization to already obtained failed assumption set
* and return the result (as failedAssumptions).
*/
SATLiteralStack explicitlyMinimizedFailedAssumptions(bool onlyPropagate=false, bool randomize = false) {
return explicitlyMinimizedFailedAssumptions(onlyPropagate ? 0u : UINT_MAX, randomize);
}
SATLiteralStack explicitlyMinimizedFailedAssumptions(unsigned conflictCountLimit, bool randomize);
/**
* Assuming that the last solving call was unsatisfiable,
* try to produce a minimal set of premises that it still unsatisfiable
* (with respect to assumptions)
*
* `premises` should be all the clauses asserted so far:
* usually you would get this from ProofProducingSATSolver.
*/
virtual SATClauseList *minimizePremises(SATClauseList *premises) = 0;
};
}
#endif // __SATSolver__