19#ifndef OR_TOOLS_SAT_SIMPLIFICATION_H_
20#define OR_TOOLS_SAT_SIMPLIFICATION_H_
27#include "absl/types/span.h"
35#include "ortools/sat/sat_parameters.pb.h"
54 void Add(
Literal x,
const absl::Span<const Literal> clause);
84 std::vector<Literal>
Clause(
int i)
const {
88 const int begin = clauses_start_[i];
89 const int end = i + 1 < clauses_start_.size() ? clauses_start_[i + 1]
90 : clauses_literals_.size();
91 std::vector<Literal> result(clauses_literals_.begin() + begin,
92 clauses_literals_.begin() + end);
93 for (
int j = 0; j < result.size(); ++j) {
94 if (result[j] == associated_literal_[i]) {
95 std::swap(result[0], result[j]);
109 const int initial_num_variables_;
114 std::vector<int> clauses_start_;
115 std::deque<Literal> clauses_literals_;
116 std::vector<Literal> associated_literal_;
149 : postsolver_(postsolver),
150 num_trivial_clauses_(0),
151 drat_proof_handler_(nullptr) {}
160 equiv_mapping_ = mapping;
166 void AddClause(absl::Span<const Literal> clause);
177 bool Presolve(
const std::vector<bool>& var_that_can_be_removed,
178 bool log_info =
false);
223 drat_proof_handler_ = drat_proof_handler;
228 bool ProcessClauseToSimplifyOthersUsingLiteral(
ClauseIndex clause_index,
234 void AddClauseInternal(std::vector<Literal>* clause);
239 void RemoveAndRegisterForPostsolveAllClauseContaining(
Literal x);
245 bool ProcessAllClauses();
249 Literal FindLiteralWithShortestOccurrenceList(
250 const std::vector<Literal>& clause);
251 LiteralIndex FindLiteralWithShortestOccurrenceListExcluding(
252 const std::vector<Literal>& clause,
Literal to_exclude);
264 void SimpleBva(LiteralIndex l);
267 void DisplayStats(
double elapsed_seconds);
277 void InitializePriorityQueue();
278 void UpdatePriorityQueue(BooleanVariable
var);
280 PQElement() : heap_index(-1), variable(-1),
weight(0.0) {}
283 void SetHeapIndex(
int h) { heap_index = h; }
284 int GetHeapIndex()
const {
return heap_index; }
288 bool operator<(
const PQElement& other)
const {
289 return weight > other.weight;
293 BooleanVariable variable;
301 void InitializeBvaPriorityQueue();
302 void UpdateBvaPriorityQueue(LiteralIndex lit);
303 void AddToBvaPriorityQueue(LiteralIndex lit);
304 struct BvaPqElement {
308 void SetHeapIndex(
int h) { heap_index = h; }
309 int GetHeapIndex()
const {
return heap_index; }
313 bool operator<(
const BvaPqElement& other)
const {
314 return weight < other.weight;
321 std::deque<BvaPqElement> bva_pq_elements_;
325 std::set<LiteralIndex> m_lit_;
326 std::vector<ClauseIndex> m_cls_;
328 std::vector<std::pair<LiteralIndex, ClauseIndex>> flattened_p_;
329 std::vector<Literal> tmp_new_clause_;
333 std::vector<bool> in_clause_to_process_;
334 std::deque<ClauseIndex> clause_to_process_;
338 std::vector<std::vector<Literal>> clauses_;
341 std::vector<uint64> signatures_;
342 int64 num_inspected_signatures_ = 0;
343 int64 num_inspected_literals_ = 0;
355 SatPostsolver* postsolver_;
360 int num_trivial_clauses_;
361 SatParameters parameters_;
362 DratProofHandler* drat_proof_handler_;
363 TimeLimit* time_limit_ =
nullptr;
382 LiteralIndex* opposite_literal,
383 int64* num_inspected_literals =
nullptr);
390 const std::vector<Literal>&
b, Literal l);
403 const std::vector<Literal>&
b, std::vector<Literal>* out);
408 const std::vector<Literal>&
b);
423 SatSolver* solver, SatPostsolver* postsolver,
424 DratProofHandler* drat_proof_handler,
438 std::unique_ptr<SatSolver>* solver, TimeLimit*
time_limit,
439 std::vector<bool>* solution ,
440 DratProofHandler* drat_proof_handler );
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
void Add(Literal x, const absl::Span< const Literal > clause)
SatPostsolver(int num_variables)
void FixVariable(Literal x)
void ApplyMapping(const absl::StrongVector< BooleanVariable, BooleanVariable > &mapping)
std::vector< bool > PostsolveSolution(const std::vector< bool > &solution)
std::vector< Literal > Clause(int i) const
std::vector< bool > ExtractAndPostsolveSolution(const SatSolver &solver)
void SetNumVariables(int num_variables)
const std::vector< Literal > & Clause(ClauseIndex ci) const
void LoadProblemIntoSatSolver(SatSolver *solver)
void AddBinaryClause(Literal a, Literal b)
void SetEquivalentLiteralMapping(const absl::StrongVector< LiteralIndex, LiteralIndex > &mapping)
void SetParameters(const SatParameters ¶ms)
absl::StrongVector< BooleanVariable, BooleanVariable > VariableMapping() const
void SetDratProofHandler(DratProofHandler *drat_proof_handler)
void AddClause(absl::Span< const Literal > clause)
bool ProcessClauseToSimplifyOthers(ClauseIndex clause_index)
void SetTimeLimit(TimeLimit *time_limit)
bool CrossProduct(Literal x)
SatPresolver(SatPostsolver *postsolver)
SharedTimeLimit * time_limit
int ComputeResolvantSize(Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b)
SatSolver::Status SolveWithPresolve(std::unique_ptr< SatSolver > *solver, TimeLimit *time_limit, std::vector< bool > *solution, DratProofHandler *drat_proof_handler)
LiteralIndex DifferAtGivenLiteral(const std::vector< Literal > &a, const std::vector< Literal > &b, Literal l)
bool ComputeResolvant(Literal x, const std::vector< Literal > &a, const std::vector< Literal > &b, std::vector< Literal > *out)
void ProbeAndFindEquivalentLiteral(SatSolver *solver, SatPostsolver *postsolver, DratProofHandler *drat_proof_handler, absl::StrongVector< LiteralIndex, LiteralIndex > *mapping)
bool SimplifyClause(const std::vector< Literal > &a, std::vector< Literal > *b, LiteralIndex *opposite_literal, int64 *num_inspected_literals)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...