A piecewise linear constraint is a constraint that assumes different linear functions depending on the truth assignment of a literal. More...

#include <PiecewiseLinearConstraint.h>

Inheritance diagram for dlinear::PiecewiseLinearConstraint:

Public Member Functions
	PiecewiseLinearConstraint (const mpq_class lb=nullptr, const mpq_class ub=nullptr, Variable active_var={}, Variable inactive_var={}, Variable theory_var={}, Expression active_soi={0}, Expression inactive_soi={0}, PiecewiseConstraintState state=PiecewiseConstraintState::NOT_FIXED)
	Construct a new Piecewise Linear Constraint object.

virtual std::set< LiteralSet >	TightenBounds (BoundPreprocessor &preprocessor)=0
	Use the `preprocessor` to tighten the bounds of the constraint and hopefully fix its state to either active or inactive.

virtual std::ostream &	Print (std::ostream &os) const =0
	Print the constraint on the standard output.

virtual LiteralSet	Assumptions () const =0
	The assumptions used to guide the SAT solver towards the most promising sub-problems.

virtual LiteralSet	LearnedClauses () const =0
	Produce some learned clauses the SAT solver will use to prune the sub-problems this piecewise constraint will not be satisfied in.

void	UpdateBounds (const mpq_class &lb, const mpq_class &ub)
	Update the bounds of the constraint.

void	UpdateBounds (const mpq_class lb, const mpq_class ub)
	Update the bounds of the constraint.

virtual void	UpdateLowerBound (const mpq_class *lb)
	Update the lower bounds of the constraint.

virtual void	UpdateUpperBound (const mpq_class *ub)
	Update the upper bounds of the constraint.

mpq_class	Cost (const Environment &env) const
	Calculate the cost of the violation of the constraint.

mpq_class	Cost (const Environment &env, bool active) const
	Calculate the cost of the violation of the constraint forcing a specific state.

bool	has_lower_bound () const
	Check whether the constraint is lower bounded.

bool	has_upper_bound () const
	Check whether the constraint is upper bounded.

bool	fixed () const
	Check whether the constraint is fixed.

const mpq_class &	lower_bound () const
	Get read-only access to the lower bound of the constraint.

const mpq_class &	upper_bound () const
	Get read-only access to the upper bound of the constraint.

const Variable &	active_var () const
	Get read-only access to the boolean variable associated with the \( y = f_\text{active}(x) \) theory literal of the constraint.

const Variable &	inactive_var () const
	Get read-only access to the boolean variable associated with the \( y = f_\text{inactive}(x) \) theory literal of the constraint.

const Variable &	theory_var () const
	Get read-only access to the theory variable \( y \) of the constraint.

const Expression &	active_soi () const
	Get read-only access to the expression \( y - f_\text{active}(x) \) of the constraint.

const Expression &	inactive_soi () const
	Get read-only access to the expression \( y - f_\text{inactive}(x) \) of the constraint.

const Expression &	soi () const

PiecewiseConstraintState	state () const
	Get read-only access to the state of the constraint.

Static Public Attributes
static const Expression	zero_soi {0}
	Expression \( 0 \) used as a soi if the constraint is not fixed yet.

Protected Attributes
const mpq_class *	lower_bound_
	Lower bound of the constraint.

const mpq_class *	upper_bound_
	Upper bound of the constraint.

const Variable	active_var_
	Boolean variable associated with the \( y = f_\text{active}(x) \) theory literal.

const Variable	inactive_var_
	Boolean variable associated with the \( y = f_\text{inactive}(x) \) theory literal.

const Variable	theory_var_
	Theory variable \( y \).

const Expression	active_soi_
	Expression \( y - f_\text{active}(x) \).

const Expression	inactive_soi_
	Expression \( y - f_\text{inactive}(x) \).

PiecewiseConstraintState	state_
	State of the constraint.

Detailed Description

A piecewise linear constraint is a constraint that assumes different linear functions depending on the truth assignment of a literal.

This kind of constraints are in the form:

\[ y = \begin{cases} f_\text{active}(x) & \text{if } l \\ f_\text{inactive}(x) & \text{otherwise} \end{cases} \]

where \( f_\text{active}, f_\text{inactive} \) are linear functions of \( x \) and \( l \) is the literal that determines which of the two is assigned to \( y \). To prune some trivial cases, the class keeps a bound on the value of \( y \).

Definition at line 35 of file PiecewiseLinearConstraint.h.

Constructor & Destructor Documentation

◆ PiecewiseLinearConstraint()

dlinear::PiecewiseLinearConstraint::PiecewiseLinearConstraint	(	const mpq_class *	lb = nullptr,
		const mpq_class *	ub = nullptr,
		Variable	active_var = {},
		Variable	inactive_var = {},
		Variable	theory_var = {},
		Expression	active_soi = {0},
		Expression	inactive_soi = {0},
		PiecewiseConstraintState	state = PiecewiseConstraintState::NOT_FIXED )

explicit

Construct a new Piecewise Linear Constraint object.

Parameters

lb	lower bound of the constraint. If not specified, the constraint is unbounded from below (-inf)
ub	upper bound of the constraint. If not specified, the constraint is unbounded from above (+inf)
active_var	boolean variable associated with the \( y = f_\text{active}(x) \) theory literal
inactive_var	boolean variable associated with the \( y = f_\text{inactive}(x) \) theory literal
theory_var	theory variable \( y \)
active_soi	expression \( y - f_\text{active}(x) \)
inactive_soi	expression \( y - f_\text{inactive}(x) \)
state	state of the constraint

Definition at line 16 of file PiecewiseLinearConstraint.cpp.

Member Function Documentation

◆ active_soi()

const Expression & dlinear::PiecewiseLinearConstraint::active_soi ( ) const

inlinenodiscard

Get read-only access to the expression \( y - f_\text{active}(x) \) of the constraint.

Returns: expression \( y - f_\text{active}(x) \) of the constraint

Definition at line 156 of file PiecewiseLinearConstraint.h.

◆ active_var()

const Variable & dlinear::PiecewiseLinearConstraint::active_var ( ) const

inlinenodiscard

Get read-only access to the boolean variable associated with the \( y = f_\text{active}(x) \) theory literal of the constraint.

Returns: boolean variable associated with the \( y = f_\text{active}(x) \) theory literal of the constraint

Definition at line 150 of file PiecewiseLinearConstraint.h.

◆ Assumptions()

virtual LiteralSet dlinear::PiecewiseLinearConstraint::Assumptions ( ) const

nodiscardpure virtual

The assumptions used to guide the SAT solver towards the most promising sub-problems.

Returns: set of literals

Implemented in dlinear::LeakyReluConstraint, and dlinear::ReluConstraint.

◆ Cost() [1/2]

mpq_class dlinear::PiecewiseLinearConstraint::Cost ( const Environment & env ) const

nodiscard

Calculate the cost of the violation of the constraint.

Given a feasible solution of the LP problems where this constraint contributes to the objective function as a Sum Of Infeasibilities, calculate the amount of violation caused by its presence in the current state. If the constraint is not fixed yet, return \( 0 \).

Parameters

env	current assignment to all the theory variables

Returns: cost of the violation

Definition at line 77 of file PiecewiseLinearConstraint.cpp.

◆ Cost() [2/2]

mpq_class dlinear::PiecewiseLinearConstraint::Cost	(	const Environment &	env,
		bool	active ) const

nodiscard

Calculate the cost of the violation of the constraint forcing a specific state.

Given a feasible solution of the LP problems where this constraint contributes to the objective function as a Sum Of Infeasibilities, calculate the amount of violation caused by its presence in the current state.

Parameters

env	current assignment to all the theory variables
active	whether to consider the constraint as active or inactive

Returns: cost of the violation

Definition at line 87 of file PiecewiseLinearConstraint.cpp.

◆ fixed()

bool dlinear::PiecewiseLinearConstraint::fixed ( ) const

inlinenodiscard

Check whether the constraint is fixed.

Returns: true if the constraint is fixed; false if the constraint is not fixed

Definition at line 142 of file PiecewiseLinearConstraint.h.

◆ has_lower_bound()

bool dlinear::PiecewiseLinearConstraint::has_lower_bound ( ) const

inlinenodiscard

Check whether the constraint is lower bounded.

Returns: true if the constraint is lower bounded; false if the constraint is not lower bounded

Definition at line 138 of file PiecewiseLinearConstraint.h.

◆ has_upper_bound()

bool dlinear::PiecewiseLinearConstraint::has_upper_bound ( ) const

inlinenodiscard

Check whether the constraint is upper bounded.

Returns: true if the constraint is upper bounded; false if the constraint is not upper bounded

Definition at line 140 of file PiecewiseLinearConstraint.h.

◆ inactive_soi()

const Expression & dlinear::PiecewiseLinearConstraint::inactive_soi ( ) const

inlinenodiscard

Get read-only access to the expression \( y - f_\text{inactive}(x) \) of the constraint.

Returns: expression \( y - f_\text{inactive}(x) \) of the constraint

Definition at line 158 of file PiecewiseLinearConstraint.h.

◆ inactive_var()

const Variable & dlinear::PiecewiseLinearConstraint::inactive_var ( ) const

inlinenodiscard

Get read-only access to the boolean variable associated with the \( y = f_\text{inactive}(x) \) theory literal of the constraint.

Returns: boolean variable associated with the \( y = f_\text{inactive}(x) \) theory literal of the constraint

Definition at line 152 of file PiecewiseLinearConstraint.h.

◆ LearnedClauses()

virtual LiteralSet dlinear::PiecewiseLinearConstraint::LearnedClauses ( ) const

nodiscardpure virtual

Produce some learned clauses the SAT solver will use to prune the sub-problems this piecewise constraint will not be satisfied in.

Returns: set of literals

Implemented in dlinear::LeakyReluConstraint, and dlinear::ReluConstraint.

◆ lower_bound()

const mpq_class & dlinear::PiecewiseLinearConstraint::lower_bound ( ) const

nodiscard

Get read-only access to the lower bound of the constraint.

If the constraint does not have a lower bound

Returns: lower bound of the constraint

See also: -inf value is returned

Definition at line 36 of file PiecewiseLinearConstraint.cpp.

◆ Print()

virtual std::ostream & dlinear::PiecewiseLinearConstraint::Print ( std::ostream & os ) const

pure virtual

Print the constraint on the standard output.

Parameters

os	standard output

Returns: updated standard output

Implemented in dlinear::LeakyReluConstraint, and dlinear::ReluConstraint.

◆ soi()

const Expression & dlinear::PiecewiseLinearConstraint::soi ( ) const

nodiscard

Get read-only access to the current Sum of Infeatsibilities expression based on the state of the  constraint.

If the constraint is not fixed yet, return the expression \( 0 \)

Returns: current Sum of Infeatsibilities expression based on the state of the constraint

Definition at line 43 of file PiecewiseLinearConstraint.cpp.

◆ state()

PiecewiseConstraintState dlinear::PiecewiseLinearConstraint::state ( ) const

inlinenodiscard

Get read-only access to the state of the constraint.

Returns: state of the constraint

Definition at line 165 of file PiecewiseLinearConstraint.h.

◆ theory_var()

const Variable & dlinear::PiecewiseLinearConstraint::theory_var ( ) const

inlinenodiscard

Get read-only access to the theory variable \( y \) of the constraint.

Returns: theory variable \( y \) of the constraint

Definition at line 154 of file PiecewiseLinearConstraint.h.

◆ TightenBounds()

virtual std::set< LiteralSet > dlinear::PiecewiseLinearConstraint::TightenBounds ( BoundPreprocessor & preprocessor )

pure virtual

Use the preprocessor to tighten the bounds of the constraint and hopefully fix its state to either active or inactive.

Parameters

preprocessor preprocessor to use to tighten the bounds

Returns: explanation of why the inactive state of this constraint is unsat

Implemented in dlinear::LeakyReluConstraint, and dlinear::ReluConstraint.

◆ UpdateBounds() [1/2]

void dlinear::PiecewiseLinearConstraint::UpdateBounds	(	const mpq_class &	lb,
		const mpq_class &	ub )

Update the bounds of the constraint.

Precondition: the new lower bound must be less than or equal to the new upper bound; the new lower bound must be greater than or equal to the current lower bound; the new upper bound must be less than or equal to the current upper bound

Parameters

lb	lower bound of the constraint
ub	upper bound of the constraint

Definition at line 54 of file PiecewiseLinearConstraint.cpp.

◆ UpdateBounds() [2/2]

void dlinear::PiecewiseLinearConstraint::UpdateBounds	(	const mpq_class *	lb,
		const mpq_class *	ub )

Update the bounds of the constraint.

If any of the bounds is not specified, the corresponding bound is not updated.

Precondition: the new lower bound must be less than or equal to the new upper bound; the new lower bound must be greater than or equal to the current lower bound; the new upper bound must be less than or equal to the current upper bound

Parameters

lb	lower bound of the constraint
ub	upper bound of the constraint

Definition at line 59 of file PiecewiseLinearConstraint.cpp.

◆ UpdateLowerBound()

void dlinear::PiecewiseLinearConstraint::UpdateLowerBound ( const mpq_class * lb )

virtual

Update the lower bounds of the constraint.

Precondition: the new lower bound must be greater than or equal to the current lower bound

Parameters

lb	lower bound of the constraint

Reimplemented in dlinear::LeakyReluConstraint, and dlinear::ReluConstraint.

Definition at line 64 of file PiecewiseLinearConstraint.cpp.

◆ UpdateUpperBound()

void dlinear::PiecewiseLinearConstraint::UpdateUpperBound ( const mpq_class * ub )

virtual

Update the upper bounds of the constraint.

Precondition: the new upper bound must be less than or equal to the current upper bound

Parameters

ub	upper bound of the constraint

Reimplemented in dlinear::LeakyReluConstraint, and dlinear::ReluConstraint.

Definition at line 70 of file PiecewiseLinearConstraint.cpp.

◆ upper_bound()

const mpq_class & dlinear::PiecewiseLinearConstraint::upper_bound ( ) const

nodiscard

Get read-only access to the upper bound of the constraint.

If the constraint does not have an upper bound

Returns: upper bound of the constraint

See also: +inf value is returned

Definition at line 39 of file PiecewiseLinearConstraint.cpp.

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

dlinear/solver/PiecewiseLinearConstraint.h
dlinear/solver/PiecewiseLinearConstraint.cpp

Public Member Functions

Static Public Attributes

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ PiecewiseLinearConstraint()

Member Function Documentation

◆ active_soi()

◆ active_var()

◆ Assumptions()

◆ Cost() [1/2]

◆ Cost() [2/2]

◆ fixed()

◆ has_lower_bound()

◆ has_upper_bound()

◆ inactive_soi()

◆ inactive_var()

◆ LearnedClauses()

◆ lower_bound()

◆ Print()

◆ soi()

◆ state()

◆ theory_var()

◆ TightenBounds()

◆ UpdateBounds() [1/2]

◆ UpdateBounds() [2/2]

◆ UpdateLowerBound()

◆ UpdateUpperBound()

◆ upper_bound()