OR-Tools  8.2
drat_checker.h
Go to the documentation of this file.
1// Copyright 2010-2018 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6// http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
14#ifndef OR_TOOLS_SAT_DRAT_CHECKER_H_
15#define OR_TOOLS_SAT_DRAT_CHECKER_H_
16
17#include <memory>
18#include <vector>
19
20#include "absl/container/flat_hash_set.h"
21#include "absl/types/span.h"
25
26namespace operations_research {
27namespace sat {
28
29// Index of a clause (>= 0).
30DEFINE_INT_TYPE(ClauseIndex, int);
31const ClauseIndex kNoClauseIndex(-1);
32
33// DRAT is a SAT proof format that allows a simple program to check that a
34// problem is really UNSAT. The description of the format and a checker are
35// available at http://www.cs.utexas.edu/~marijn/drat-trim/. This class checks
36// that a DRAT proof is valid.
37//
38// Note that DRAT proofs are often huge (can be GB), and can take about as much
39// time to check as it takes to find the proof in the first place!
41 public:
44
45 // Returns the number of Boolean variables used in the problem and infered
46 // clauses.
47 int num_variables() const { return num_variables_; }
48
49 // Adds a clause of the problem that must be checked. The problem clauses must
50 // be added first, before any infered clause. The given clause must not
51 // contain a literal and its negation. Must not be called after Check().
52 void AddProblemClause(absl::Span<const Literal> clause);
53
54 // Adds a clause which is infered from the problem clauses and the previously
55 // infered clauses (that are have not been deleted). Infered clauses must be
56 // added after the problem clauses. Clauses with the Reverse Asymetric
57 // Tautology (RAT) property for literal l must start with this literal. The
58 // given clause must not contain a literal and its negation. Must not be
59 // called after Check().
60 void AddInferedClause(absl::Span<const Literal> clause);
61
62 // Deletes a problem or infered clause. The order of the literals does not
63 // matter. In particular, it can be different from the order that was used
64 // when the clause was added. Must not be called after Check().
65 void DeleteClause(absl::Span<const Literal> clause);
66
67 // Checks that the infered clauses form a DRAT proof that the problem clauses
68 // are UNSAT. For this the last added infered clause must be the empty clause
69 // and each infered clause must have either the Reverse Unit Propagation (RUP)
70 // or the Reverse Asymetric Tautology (RAT) property with respect to the
71 // problem clauses and the previously infered clauses which are not deleted.
72 // Returns VALID if the proof is valid, INVALID if it is not, and UNKNOWN if
73 // the check timed out.
74 // WARNING: no new clause must be added or deleted after this method has been
75 // called.
76 enum Status {
80 };
81 Status Check(double max_time_in_seconds);
82
83 // Returns a subproblem of the original problem that is already UNSAT. The
84 // result is undefined if Check() was not previously called, or did not return
85 // true.
86 std::vector<std::vector<Literal>> GetUnsatSubProblem() const;
87
88 // Returns a DRAT proof that GetUnsatSubProblem() is UNSAT. The result is
89 // undefined if Check() was not previously called, or did not return true.
90 std::vector<std::vector<Literal>> GetOptimizedProof() const;
91
92 private:
93 // A problem or infered clause. The literals are specified as a subrange of
94 // 'literals_' (namely the subrange from 'first_literal_index' to
95 // 'first_literal_index' + 'num_literals' - 1), and are sorted in increasing
96 // order *before Check() is called*.
97 struct Clause {
98 // The index of the first literal of this clause in 'literals_'.
99 int first_literal_index;
100 // The number of literals of this clause.
101 int num_literals;
102
103 // The clause literal to use to check the RAT property, or kNoLiteralIndex
104 // for problem clauses and empty infered clauses.
105 LiteralIndex rat_literal_index = kNoLiteralIndex;
106
107 // The *current* number of copies of this clause. This number is incremented
108 // each time a copy of the clause is added, and decremented each time a copy
109 // is deleted. When this number reaches 0, the clause is actually marked as
110 // deleted (see 'deleted_index'). If other copies are added after this
111 // number reached 0, a new clause is added (because a Clause lifetime is a
112 // single interval of ClauseIndex values; therefore, in order to represent a
113 // lifetime made of several intervals, several Clause are used).
114 int num_copies = 1;
115
116 // The index in 'clauses_' from which this clause is deleted (inclusive).
117 // For instance, with AddProblemClause(c0), AddProblemClause(c1),
118 // DeleteClause(c0), AddProblemClause(c2), ... if c0's index is 0, then its
119 // deleted_index is 2. Meaning that when checking a clause whose index is
120 // larger than or equal to 2 (e.g. c2), c0 can be ignored.
121 ClauseIndex deleted_index = ClauseIndex(std::numeric_limits<int>::max());
122
123 // The indices of the clauses (with at least two literals) which are deleted
124 // just after this clause.
125 std::vector<ClauseIndex> deleted_clauses;
126
127 // Whether this clause is actually needed to check the DRAT proof.
128 bool is_needed_for_proof = false;
129 // Whether this clause is actually needed to check the current step (i.e. an
130 // infered clause) of the DRAT proof. This bool is always false, except in
131 // MarkAsNeededForProof() that uses it temporarily.
132 bool tmp_is_needed_for_proof_step = false;
133
134 Clause(int first_literal_index, int num_literals);
135
136 // Returns true if this clause is deleted before the given clause.
137 bool IsDeleted(ClauseIndex clause_index) const;
138 };
139
140 // A literal to assign to true during boolean constraint propagation. When a
141 // literal is assigned, new literals can be found that also need to be
142 // assigned to true (via unit clauses). In this case they are pushed on a
143 // stack of LiteralToAssign values, to be processed later on (the use of this
144 // stack avoids recursive calls to the boolean constraint propagation method
145 // AssignAndPropagate()).
146 struct LiteralToAssign {
147 // The literal that must be assigned to true.
148 Literal literal;
149 // The index of the clause from which this assignment was deduced. This is
150 // kNoClauseIndex for the clause we are currently checking (whose literals
151 // are all falsified to check if a conflict can be derived). Otherwise this
152 // is the index of a unit clause with unit literal 'literal' that was found
153 // during boolean constraint propagation.
154 ClauseIndex source_clause_index;
155 };
156
157 // Hash function for clauses.
158 struct ClauseHash {
159 DratChecker* checker;
160 explicit ClauseHash(DratChecker* checker) : checker(checker) {}
161 std::size_t operator()(const ClauseIndex clause_index) const;
162 };
163
164 // Equality function for clauses.
165 struct ClauseEquiv {
166 DratChecker* checker;
167 explicit ClauseEquiv(DratChecker* checker) : checker(checker) {}
168 bool operator()(const ClauseIndex clause_index1,
169 const ClauseIndex clause_index2) const;
170 };
171
172 // Adds a clause and returns its index.
173 ClauseIndex AddClause(absl::Span<const Literal> clause);
174
175 // Removes the last clause added to 'clauses_'.
176 void RemoveLastClause();
177
178 // Returns the literals of the given clause in increasing order.
179 absl::Span<const Literal> Literals(const Clause& clause) const;
180
181 // Initializes the data structures used to check the DRAT proof.
182 void Init();
183
184 // Adds 2 watch literals for the given clause.
185 void WatchClause(ClauseIndex clause_index);
186
187 // Returns true if, by assigning all the literals of 'clause' to false, a
188 // conflict can be found with boolean constraint propagation, using the non
189 // deleted clauses whose index is strictly less than 'num_clauses'. If so,
190 // marks the clauses actually used in this process as needed to check to DRAT
191 // proof.
192 bool HasRupProperty(ClauseIndex num_clauses,
193 absl::Span<const Literal> clause);
194
195 // Assigns 'literal' to true in 'assignment_' (and pushes it to 'assigned_'),
196 // records its source clause 'source_clause_index' in 'assignment_source_',
197 // and uses the watched literals to find all the clauses (whose index is less
198 // than 'num_clauses') that become unit due to this assignment. For each unit
199 // clause found, pushes its unit literal on top of
200 // 'high_priority_literals_to_assign_' or 'low_priority_literals_to_assign_'.
201 // Returns kNoClauseIndex if no falsified clause is found, or the index of the
202 // first found falsified clause otherwise.
203 ClauseIndex AssignAndPropagate(ClauseIndex num_clauses, Literal literal,
204 ClauseIndex source_clause_index);
205
206 // Marks the given clause as needed to check the DRAT proof, as well as the
207 // other clauses which were used to check this clause (these are found from
208 // 'unit_stack_', containing the clauses that became unit in
209 // AssignAndPropagate, and from 'assignment_source_', containing for each
210 // variable the clause that caused its assignment).
211 void MarkAsNeededForProof(Clause* clause);
212
213 // Returns the clauses whose index is in [begin,end) which are needed for the
214 // proof. The result is undefined if Check() was not previously called, or did
215 // not return true.
216 std::vector<std::vector<Literal>> GetClausesNeededForProof(
217 ClauseIndex begin, ClauseIndex end) const;
218
219 void LogStatistics(int64 duration_nanos) const;
220
221 // The index of the first infered clause in 'clauses_', or kNoClauseIndex if
222 // there is no infered clause.
223 ClauseIndex first_infered_clause_index_;
224
225 // The problem clauses, followed by the infered clauses.
227
228 // A content addressable set of the non-deleted clauses in clauses_. After
229 // adding a clause to clauses_, this set can be used to find if the same
230 // clause was previously added (i.e if a find using the new clause index
231 // returns a previous index) and not yet deleted.
232 absl::flat_hash_set<ClauseIndex, ClauseHash, ClauseEquiv> clause_set_;
233
234 // All the literals used in 'clauses_'.
235 std::vector<Literal> literals_;
236
237 // The number of Boolean variables used in the clauses.
238 int num_variables_;
239
240 // ---------------------------------------------------------------------------
241 // Data initialized in Init() and used in Check() to check the DRAT proof.
242
243 // The literals that have been assigned so far (this is used to unassign them
244 // after a clause has been checked, before checking the next one).
245 std::vector<Literal> assigned_;
246
247 // The current assignment values of literals_.
248 VariablesAssignment assignment_;
249
250 // For each variable, the index of the unit clause that caused its assignment,
251 // or kNoClauseIndex if the variable is not assigned, or was assigned to
252 // falsify the clause that is currently being checked.
254
255 // The stack of literals that remain to be assigned to true during boolean
256 // constraint propagation, with high priority (unit clauses which are already
257 // marked as needed for the proof are given higher priority than the others
258 // during boolean constraint propagation. According to 'Trimming while
259 // Checking Clausal Proofs', this heuristics reduces the final number of
260 // clauses that are marked as needed for the proof, and therefore the
261 // verification time, in a majority of cases -- but not all).
262 std::vector<LiteralToAssign> high_priority_literals_to_assign_;
263
264 // The stack of literals that remain to be assigned to true during boolean
265 // constraint propagation, with low priority (see above).
266 std::vector<LiteralToAssign> low_priority_literals_to_assign_;
267
268 // For each literal, the list of clauses in which this literal is watched.
269 // Invariant 1: the literals with indices first_watched_literal_index and
270 // second_watched_literal_index of each clause with at least two literals are
271 // watched.
272 // Invariant 2: watched literals are non-falsified if the clause is not
273 // satisfied (in more details: if a clause c is contained in
274 // 'watched_literals_[l]' for literal l, then either c is satisfied with
275 // 'assignment_', or l is unassigned or assigned to true).
277
278 // The list of clauses with only one literal. This is needed for boolean
279 // constraint propagation, in addition to watched literals, because watched
280 // literals can only be used with clauses having at least two literals.
281 std::vector<ClauseIndex> single_literal_clauses_;
282
283 // The stack of clauses that have become unit during boolean constraint
284 // propagation, in HasRupProperty().
285 std::vector<ClauseIndex> unit_stack_;
286
287 // A temporary assignment, always fully unassigned except in Resolve().
288 VariablesAssignment tmp_assignment_;
289
290 // ---------------------------------------------------------------------------
291 // Statistics
292
293 // The number of infered clauses having the RAT property (but not the RUP
294 // property).
295 int num_rat_checks_;
296};
297
298// Returns true if the given clause contains the given literal. This works in
299// O(clause.size()).
300bool ContainsLiteral(absl::Span<const Literal> clause, Literal literal);
301
302// Returns true if 'complementary_literal' is the unique complementary literal
303// in the two given clauses. If so the resolvent of these clauses (i.e. their
304// union with 'complementary_literal' and its negation removed) is set in
305// 'resolvent'. 'clause' must contain 'complementary_literal', while
306// 'other_clause' must contain its negation. 'assignment' must have at least as
307// many variables as each clause, and they must all be unassigned. They are
308// still unassigned upon return.
309bool Resolve(absl::Span<const Literal> clause,
310 absl::Span<const Literal> other_clause,
311 Literal complementary_literal, VariablesAssignment* assignment,
312 std::vector<Literal>* resolvent);
313
314// Adds to the given drat checker the problem clauses from the file at the given
315// path, which must be in DIMACS format. Returns true iff the file was
316// successfully parsed.
317bool AddProblemClauses(const std::string& file_path, DratChecker* drat_checker);
318
319// Adds to the given drat checker the infered and deleted clauses from the file
320// at the given path, which must be in DRAT format. Returns true iff the file
321// was successfully parsed.
322bool AddInferedAndDeletedClauses(const std::string& file_path,
323 DratChecker* drat_checker);
324
325// The file formats that can be used to save a list of clauses.
329};
330
331// Prints the given clauses in the file at the given path, using the given file
332// format. Returns true iff the file was successfully written.
333bool PrintClauses(const std::string& file_path, SatFormat format,
334 const std::vector<std::vector<Literal>>& clauses,
335 int num_variables);
336
337} // namespace sat
338} // namespace operations_research
339
340#endif // OR_TOOLS_SAT_DRAT_CHECKER_H_
int64 max
Definition: alldiff_cst.cc:139
void AddInferedClause(absl::Span< const Literal > clause)
Definition: drat_checker.cc:69
void DeleteClause(absl::Span< const Literal > clause)
Status Check(double max_time_in_seconds)
std::vector< std::vector< Literal > > GetUnsatSubProblem() const
void AddProblemClause(absl::Span< const Literal > clause)
Definition: drat_checker.cc:56
std::vector< std::vector< Literal > > GetOptimizedProof() const
int64_t int64
const LiteralIndex kNoLiteralIndex(-1)
bool PrintClauses(const std::string &file_path, SatFormat format, const std::vector< std::vector< Literal > > &clauses, int num_variables)
DEFINE_INT_TYPE(ClauseIndex, int)
bool Resolve(absl::Span< const Literal > clause, absl::Span< const Literal > other_clause, Literal complementary_literal, VariablesAssignment *assignment, std::vector< Literal > *resolvent)
bool AddInferedAndDeletedClauses(const std::string &file_path, DratChecker *drat_checker)
const ClauseIndex kNoClauseIndex(-1)
bool ContainsLiteral(absl::Span< const Literal > clause, Literal literal)
bool AddProblemClauses(const std::string &file_path, DratChecker *drat_checker)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
Literal literal
Definition: optimization.cc:84