operations_research::sat::LinearBooleanProblemWrapper Class Reference

This implement the implicit contract needed by the SatCnfReader class. More...

#include <sat_cnf_reader.h>

Public Member Functions
	LinearBooleanProblemWrapper (LinearBooleanProblem *p)
void	SetSizeAndPostprocess (int num_variables, int num_slacks)
void	AddConstraint (absl::Span< const int > clause, bool last_is_slack=false)
void	AddObjectiveTerm (int literal, int64_t value)
void	SetObjectiveOffset (int64_t offset)

Detailed Description

This implement the implicit contract needed by the SatCnfReader class.

Definition at line 38 of file sat_cnf_reader.h.

Constructor & Destructor Documentation

LinearBooleanProblemWrapper()

operations_research::sat::LinearBooleanProblemWrapper::LinearBooleanProblemWrapper ( LinearBooleanProblem * p )

inlineexplicit

Definition at line 40 of file sat_cnf_reader.h.

Member Function Documentation

AddConstraint()

void operations_research::sat::LinearBooleanProblemWrapper::AddConstraint ( absl::Span< const int > clause, bool last_is_slack = false )

inline

If last_is_slack is true, then the last literal is assumed to be a slack with index in [-num_slacks, num_slacks]. We will re-index it at the end in SetSizeAndPostprocess().

Definition at line 61 of file sat_cnf_reader.h.

AddObjectiveTerm()

void operations_research::sat::LinearBooleanProblemWrapper::AddObjectiveTerm ( int literal, int64_t value )

inline

Definition at line 74 of file sat_cnf_reader.h.

SetObjectiveOffset()

void operations_research::sat::LinearBooleanProblemWrapper::SetObjectiveOffset ( int64_t offset )

inline

Definition at line 80 of file sat_cnf_reader.h.

SetSizeAndPostprocess()

void operations_research::sat::LinearBooleanProblemWrapper::SetSizeAndPostprocess ( int num_variables, int num_slacks )

inline

In the new 2022 .wcnf format, we don't know the number of variable before hand (no header). So when this is called (after all the constraint have been added), we need to re-index the slack so that they are after the variable of the original problem.

Definition at line 46 of file sat_cnf_reader.h.

---

The documentation for this class was generated from the following file:

• ortools/sat/sat_cnf_reader.h