14#ifndef OR_TOOLS_SAT_DRAT_CHECKER_H_
15#define OR_TOOLS_SAT_DRAT_CHECKER_H_
20#include "absl/container/flat_hash_set.h"
21#include "absl/types/span.h"
99 int first_literal_index;
125 std::vector<ClauseIndex> deleted_clauses;
128 bool is_needed_for_proof =
false;
132 bool tmp_is_needed_for_proof_step =
false;
134 Clause(
int first_literal_index,
int num_literals);
137 bool IsDeleted(ClauseIndex clause_index)
const;
146 struct LiteralToAssign {
154 ClauseIndex source_clause_index;
160 explicit ClauseHash(
DratChecker* checker) : checker(checker) {}
161 std::size_t operator()(
const ClauseIndex clause_index)
const;
167 explicit ClauseEquiv(
DratChecker* checker) : checker(checker) {}
168 bool operator()(
const ClauseIndex clause_index1,
169 const ClauseIndex clause_index2)
const;
173 ClauseIndex AddClause(absl::Span<const Literal> clause);
176 void RemoveLastClause();
179 absl::Span<const Literal> Literals(
const Clause& clause)
const;
185 void WatchClause(ClauseIndex clause_index);
192 bool HasRupProperty(ClauseIndex num_clauses,
193 absl::Span<const Literal> clause);
203 ClauseIndex AssignAndPropagate(ClauseIndex num_clauses, Literal
literal,
204 ClauseIndex source_clause_index);
211 void MarkAsNeededForProof(Clause* clause);
216 std::vector<std::vector<Literal>> GetClausesNeededForProof(
217 ClauseIndex begin, ClauseIndex end)
const;
219 void LogStatistics(
int64 duration_nanos)
const;
223 ClauseIndex first_infered_clause_index_;
232 absl::flat_hash_set<ClauseIndex, ClauseHash, ClauseEquiv> clause_set_;
235 std::vector<Literal> literals_;
245 std::vector<Literal> assigned_;
248 VariablesAssignment assignment_;
262 std::vector<LiteralToAssign> high_priority_literals_to_assign_;
266 std::vector<LiteralToAssign> low_priority_literals_to_assign_;
281 std::vector<ClauseIndex> single_literal_clauses_;
285 std::vector<ClauseIndex> unit_stack_;
288 VariablesAssignment tmp_assignment_;
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);
323 DratChecker* drat_checker);
334 const std::vector<std::vector<Literal>>& clauses,
void AddInferedClause(absl::Span< const Literal > clause)
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)
int num_variables() const
std::vector< std::vector< Literal > > GetOptimizedProof() const
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...