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
/*
* 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 MinimizingSolver.hpp
*
* Defines class MinimizingSolver which supports partial models.
*/
#ifndef __MinimizingSolver__
#define __MinimizingSolver__
#include "Forwards.hpp"
#include "Lib/DArray.hpp"
#include "Lib/DHSet.hpp"
#include "Lib/Int.hpp"
#include "Lib/ScopedPtr.hpp"
#include "Lib/Stack.hpp"
#include "Lib/DynamicHeap.hpp"
#include "Lib/ArrayMap.hpp"
#include "SATSolver.hpp"
namespace SAT {
using namespace Lib;
class MinimizingSolver : public SATSolver {
public:
MinimizingSolver(SATSolver* inner);
void randomizeForNextAssignment(unsigned maxVar) override {
_inner->randomizeForNextAssignment(maxVar); _assignmentValid = false;
}
void addClause(SATClause* cl) override;
VarAssignment getAssignment(unsigned var) override;
bool isZeroImplied(unsigned var) override;
void ensureVarCount(unsigned newVarCnt) override;
unsigned newVar() override {
DEBUG_CODE(unsigned oldVC = _varCnt);
ensureVarCount(_varCnt+1);
ASS_EQ(_varCnt,oldVC+1);
return _varCnt;
}
void suggestPolarity(unsigned var, unsigned pol) override { _inner->suggestPolarity(var,pol); }
Status solveUnderAssumptionsLimited(const SATLiteralStack& assumps, unsigned conflictCountLimit) override {
_assignmentValid = false;
return _inner->solveUnderAssumptionsLimited(assumps, conflictCountLimit);
}
SATLiteralStack failedAssumptions() override { return _inner->failedAssumptions(); }
SATClauseList *minimizePremises(SATClauseList *premises) override {
return _inner->minimizePremises(premises);
}
private:
bool admitsDontcare(unsigned var) {
ASS_G(var,0); ASS_LE(var,_varCnt);
return _watcher[var].isEmpty() && !_inner->isZeroImplied(var);
/**
* TODO: as an optimization, the _watcher stack for zero implied variables
* could be reset. It will not be needed anymore.
*/
}
void selectVariable(unsigned var);
bool tryPuttingToAnExistingWatch(SATClause* cl);
void putIntoIndex(SATClause* cl);
void processInnerAssignmentChanges();
void processUnprocessedAndFillHeap();
void updateAssignment();
unsigned _varCnt;
ScopedPtr<SATSolver> _inner;
/**
* If true, _asgn assignment corresponds to the assignment in
* the inner solver
*/
bool _assignmentValid;
/**
* Clauses of which we yet need to ensure they are satisfied
*
* Invariant: outside of this object when _assignmentValid, the stack is empty.
*/
SATClauseStack _unprocessed;
/**
* A total extension of the current assignment.
* The current assignment will report don't-care for those variables
* for which admitsDontcare is true.
*
* We define a literal "corresponding to variable var in _asgn"
* as SATLiteral(var,_asgn[var]). Used below.
*/
DArray<bool> _asgn;
/**
* Array of clauses made satisfied by giving up the don't-care value
* for a particular variable and using the value dictated by _asgn instead.
*
* The length of the array is _varCnt.
*/
DArray<SATClauseStack> _watcher;
typedef DArray<unsigned> CntArray;
/**
* Number of unsatisfied clauses for each literal
* corresponding to a variable in _asgn.
*
* Indexed by literal's var.
*
* The length of the array is _varCnt.
*/
CntArray _unsClCnt;
struct CntComparator
{
CntComparator(CntArray& ctr) : _ctr(ctr) {}
Comparison compare(unsigned v1, unsigned v2)
{
// DynamicHeap is minimal and we want maximum,
// so we need to swap the arguments
return Int::compare(_ctr[v2], _ctr[v1]);
}
CntArray& _ctr;
};
/**
* Heap "on top of" _unsClCnt to facilitate fast "extract max" operation.
*
* Heap is empty when _assignmentValid.
*/
DynamicHeap<unsigned, CntComparator, ArrayMap<size_t> > _heap;
/**
* Not yet satisfied clauses indexed by each variable
* whose corresponding literal in _asgn can make the clause true.
*
* A clause appears once for every such literal.
* All entries should be empty when _assignmentValid.
*
* The length of the array is _varCnt.
*/
DArray<SATClauseStack> _clIdx;
/**
* A set of satisfied clauses. To correctly maintain
* _unsClCnt, when there is more than one way to make clause
* satisfied.
*/
DHSet<SATClause*> _satisfiedClauses;
};
}
#endif // __MinimizingSolver__