A ReLU constraint is a kind of piecewise linear constraint. More...

#include <ReluConstraint.h>

Inheritance diagram for dlinear::ReluConstraint:

Public Member Functions
	ReluConstraint (const Variable &relu_var, const Expression &e, const PredicateAbstractor &pa)
	Construct a new Relu Constraint object.

	ReluConstraint (Variable active_var, Variable inactive_var, Variable relu_var, Expression active_soi)
	Construct a new Relu Constraint object.

void	UpdateUpperBound (const mpq_class *upper_bound) override
	Update the upper bounds of the constraint.

void	UpdateLowerBound (const mpq_class *lower_bound) override
	Update the lower bounds of the constraint.

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

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

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

std::ostream &	Print (std::ostream &os) const override
	Print the constraint on the standard output.

Public Member Functions inherited from 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)
	Construct a new Piecewise Linear Constraint object.

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.

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 mpq_class	zero {0}
	Zero constant all the pointers to the default lower bound will point to.

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

Additional Inherited Members
Protected Attributes inherited from dlinear::PiecewiseLinearConstraint
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 ReLU constraint is a kind of piecewise linear constraint.

It is used as an activation function in a Neural Network. The ReLU function is defined as:

\[ y = \begin{cases} x & \text{if } x > 0 \\ 0 & \text{otherwise} \end{cases} \]

Definition at line 29 of file ReluConstraint.h.

Constructor & Destructor Documentation

◆ ReluConstraint() [1/2]

dlinear::ReluConstraint::ReluConstraint	(	const Variable &	relu_var,
		const Expression &	e,
		const PredicateAbstractor &	pa )

Construct a new Relu Constraint object.

Given the standard ReLU definition, where relu_var is \( y \) and e is \( x \), we store the following:

inactive_formula is the formula \( y = 0 \)
active_formula is the formula \( y = x \)
active_soi is the sum of infeasibility \( y - x \) used if the constraint is active.
Parameters

relu_var theory variable \( y \)

e expression \( x \)

pa predicate abstractor used to convert the formula to a boolean variable

Definition at line 18 of file ReluConstraint.cpp.

◆ ReluConstraint() [2/2]

dlinear::ReluConstraint::ReluConstraint	(	Variable	active_var,
		Variable	inactive_var,
		Variable	relu_var,
		Expression	active_soi )

Construct a new Relu Constraint object.

Given the standard ReLU definition, the three theory variables are:

inactive_var is the boolean variable associated with the formula \( y = 0 \)
active_var is the boolean variable associated with the formula \( y = x \)

relu_var is the theory variable \( y \)

Parameters

active_var	boolean variable associated with the formula \( y = x \)
inactive_var	boolean variable associated with the formula \( y = 0 \)
relu_var	theory variable \( y \)
active_soi	sum of infeasibility \( y - x \) used if the constraint is active. It must be \( 0 \) for the constraint to be satisfied

Definition at line 21 of file ReluConstraint.cpp.

Member Function Documentation

◆ Assumptions()

LiteralSet dlinear::ReluConstraint::Assumptions ( ) const

nodiscardoverridevirtual

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

Returns: set of literals

Implements dlinear::PiecewiseLinearConstraint.

Definition at line 60 of file ReluConstraint.cpp.

◆ LearnedClauses()

LiteralSet dlinear::ReluConstraint::LearnedClauses ( ) const

nodiscardoverridevirtual

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

Implements dlinear::PiecewiseLinearConstraint.

Definition at line 66 of file ReluConstraint.cpp.

◆ Print()

std::ostream & dlinear::ReluConstraint::Print ( std::ostream & os ) const

overridevirtual

Print the constraint on the standard output.

Parameters

os	standard output

Returns: updated standard output

Implements dlinear::PiecewiseLinearConstraint.

Definition at line 74 of file ReluConstraint.cpp.

◆ TightenBounds()

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

overridevirtual

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

Implements dlinear::PiecewiseLinearConstraint.

Definition at line 44 of file ReluConstraint.cpp.

◆ UpdateLowerBound()

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

overridevirtual

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 from dlinear::PiecewiseLinearConstraint.

Definition at line 25 of file ReluConstraint.cpp.

◆ UpdateUpperBound()

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

overridevirtual

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 from dlinear::PiecewiseLinearConstraint.

Definition at line 32 of file ReluConstraint.cpp.

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

dlinear/solver/ReluConstraint.h
dlinear/solver/ReluConstraint.cpp

relu_var	theory variable \( y \)
e	expression \( x \)
pa	predicate abstractor used to convert the formula to a boolean variable

Public Member Functions

Static Public Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ ReluConstraint() [1/2]

◆ ReluConstraint() [2/2]

Member Function Documentation

◆ Assumptions()

◆ LearnedClauses()

◆ Print()

◆ TightenBounds()

◆ UpdateLowerBound()

◆ UpdateUpperBound()