14#ifndef OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_
15#define OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_
21#include "absl/types/span.h"
74 void AddClause(absl::Span<const Literal> clause);
95 void MapClause(absl::Span<const Literal> clause);
101 std::vector<Literal> values_;
107 std::unique_ptr<DratChecker> drat_checker_;
108 std::unique_ptr<DratWriter> drat_writer_;
void SetNumVariables(int num_variables)
void DeleteClause(absl::Span< const Literal > clause)
DratChecker::Status Check(double max_time_in_seconds)
void AddProblemClause(absl::Span< const Literal > clause)
void ApplyMapping(const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
void AddClause(absl::Span< const Literal > clause)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...