18 #include "absl/memory/memory.h"
27 : variable_index_(0), drat_checker_(new
DratChecker()) {}
32 drat_writer_(new
DratWriter(in_binary_format, output)) {
34 drat_checker_ = absl::make_unique<DratChecker>();
41 for (BooleanVariable v(0); v < mapping.
size(); ++v) {
42 const BooleanVariable image = mapping[v];
44 if (image >= new_mapping.
size())
48 v < reverse_mapping_.
size() ? reverse_mapping_[v] : v;
52 std::swap(new_mapping, reverse_mapping_);
57 while (reverse_mapping_.
size() < num_variables) {
58 reverse_mapping_.
push_back(BooleanVariable(variable_index_++));
63 reverse_mapping_.
push_back(BooleanVariable(variable_index_++));
67 if (drat_checker_ !=
nullptr) {
68 drat_checker_->AddProblemClause(clause);
74 if (drat_checker_ !=
nullptr) {
75 drat_checker_->AddInferedClause(values_);
77 if (drat_writer_ !=
nullptr) {
78 drat_writer_->AddClause(values_);
84 if (drat_checker_ !=
nullptr) {
85 drat_checker_->DeleteClause(values_);
87 if (drat_writer_ !=
nullptr) {
88 drat_writer_->DeleteClause(values_);
93 if (drat_checker_ !=
nullptr) {
95 drat_checker_->AddInferedClause({});
96 return drat_checker_->Check(max_time_in_seconds);
98 return DratChecker::Status::UNKNOWN;
101 void DratProofHandler::MapClause(absl::Span<const Literal> clause) {
103 for (
const Literal l : clause) {
105 const Literal original_literal =
106 Literal(reverse_mapping_[l.Variable()], l.IsPositive());
107 values_.push_back(original_literal);
113 std::sort(values_.begin(), values_.end(), [](Literal
a, Literal
b) {
114 return std::abs(a.SignedValue()) > std::abs(b.SignedValue());
#define CHECK_LT(val1, val2)
#define CHECK_EQ(val1, val2)
#define CHECK_GE(val1, val2)
#define CHECK_NE(val1, val2)
void resize(size_type new_size)
void push_back(const value_type &x)
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)
const BooleanVariable kNoBooleanVariable(-1)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...