Complete solver using SoPlex. More...

#include <CompleteSoplexTheorySolver.h>

Inheritance diagram for dlinear::CompleteSoplexTheorySolver:

Classes
struct	NqExplanation
	Structure used to store the infeasibility explanation of a subset of non-equal constraints. More...

Public Member Functions
Explanations	EnableLiteral (const Literal &lit) override
	Activate the literal that had previously been added to the theory solver.

void	AddVariable (const Variable &var) override
	Add a variable (column) to the theory solver.

void	AddLiteral (const Variable &formula_var, const Formula &formula) override
	Add a Literal to the theory solver.

void	Reset () override
	Reset the linear problem.

Public Member Functions inherited from dlinear::SoplexTheorySolver
void	AddVariable (const Variable &var) override
	Add a variable (column) to the theory solver.

void	AddLiterals () override
	Add a vector of literals to the theory solver.

void	Consolidate (const Box &box) override
	Consolidate the solver.

void	Reset () override
	Reset the linear problem.

Public Member Functions inherited from dlinear::TheorySolver
	TheorySolver (const PredicateAbstractor &predicate_abstractor, const std::string &class_name="TheorySolver")
	Construct a new Theory Solver object.

virtual Explanations	PreprocessFixedLiterals (const LiteralSet &fixed_literals)
	Add the fixed literals to the theory solver.

Explanations	EnableLiterals (std::span< const Literal > theory_literals)
	Activate the literals that have previously been added to the theory solver.

const Box &	model () const
	Get read-only access to the model that satisfies all the constraints of the TheorySolver.

const Config &	config () const
	Get read-only access to the configuration of the TheorySolver.

const PredicateAbstractor &	predicate_abstractor () const
	Get read-only access to the predicate abstractor of the TheorySolver.

const std::map< Variable::Id, int > &	var_to_theory_col () const
	Get read-only access to the map of variables to the theory columns of the TheorySolver.

const std::vector< Variable > &	theory_col_to_var () const
	Get read-only access to the map of theory columns to the variables of the TheorySolver.

const std::map< Variable::Id, int > &	lit_to_theory_row () const
	Get read-only access to the map of literals to the theory rows of the TheorySolver.

const std::vector< Literal > &	theory_row_to_lit () const
	Get read-only access to the map of theory rows to the literals of the TheorySolver.

const BoundVectorMap &	theory_bounds () const
	Get read-only access to the bounds of each theory variable of the TheorySolver.

const BoundVectorMap &	fixed_theory_bounds () const
	Get read-only access to the fixed bounds of each theory variable of the TheorySolver.

const BoundPreprocessor &	preprocessor () const
	Get read-only access to the bound preprocessor of the TheorySolver.

BoundPreprocessor &	m_preprocessor ()
	Get read-write access to the bound preprocessor of the TheorySolver.

const BoundPreprocessor &	fixed_preprocessor () const
	Get read-only access to the fixed bound preprocessor of the TheorySolver.

BoundPreprocessor &	m_fixed_preprocessor ()
	Get read-write access to the fixed bound preprocessor of the TheorySolver.

std::size_t	theory_row_count () const
	Get read-only access to the number of rows of the TheorySolver.

std::size_t	theory_col_count () const
	Get read-only access to the number of columns of the TheorySolver.

std::set< Literal >	enabled_literals () const
	Get read-only access to the vector of enabled literals of the TheorySolver.

SatResult	CheckSat (const Box &box, mpq_class *actual_precision, std::set< LiteralSet > &explanations)
	Check the satisfiability of the theory.

virtual SatResult	CheckSatCore (mpq_class *actual_precision, std::set< LiteralSet > &explanations)=0
	Check the satisfiability of the theory.

const IterationStats &	stats () const
	Get the statistics of the theory solver.

Private Member Functions
void	EnableSpxVarBound () override
	Set the bounds of the variables in the LP solver.

void	EnableSpxRow (int spx_row, bool truth) override
	Enable the `spx_row` row for the LP solver.

SatResult	SpxCheckSat ()
	Internal method to check the satisfiability of the current LP problem.

void	UpdateExplanationStrictInfeasible ()
	Update the explanation with the current LP solution.

void	UpdateExplanationInfeasible ()
	Update the explanation with the infeasible core.

void	Consolidate (const Box &box) override
	Consolidate the solver.

void	EnableNqLiteral (int spx_row, bool truth)
	Enable the non-equal constraint at row `spx_row` based on the given `truth`.

void	EnableNqLiterals (const std::vector< bool > &nq_status, bool force=false)
	Enable the non-equal constraints based on the current iterator value `nq_status`.

void	DisableNqLiterals (const std::set< std::size_t > &nq_constraints)
	Disable the non-equal constraints in the given set.

bool	UpdateBitIncrementIteratorBasedOnExplanation (BitIncrementIterator &bit_iterator)
	Update the BitIncrementIterator `bit_iterator` based on the current explanation.

std::set< std::size_t >	IteratorNqRowsInLastExplanation () const
	Find the non-equal rows in the current explanation.

void	GetExplanation (Explanations &explanations)
	Add a new explanation to `explanations` from theory_rows_to_explanations_.

Private Attributes
std::vector< int >	nq_row_to_theory_rows_
	Index of row with a non-equal-to constraint in the order they appear mapped to the corresponding spx_row.

std::vector< bool >	last_nq_status_
	Last status of the non-equal constraints.

std::set< int >	last_theory_rows_to_explanation_
	Last set of theory rows that are part of the explanation.

std::set< std::set< int > >	theory_rows_to_explanations_
	Set that contains all the explanation the solver produced.

std::map< std::set< std::size_t >, NqExplanation >	nq_explanations_
	Map of non-equal explanations.

bool	locked_solver_
	Flag to indicate if the solver is locked. A locked solver will always return UNSAT.

std::set< std::pair< std::size_t, bool > >	single_nq_rows_
	Set of non-equal rows that appear alone in the explanation, with the current assignment.

Static Private Attributes
static const mpq_class	strict_col_lb_ {0}
	Zero. Used for the strict variable lower bound.

static const mpq_class	strict_col_ub_ {1}
	One. Used for the strict variable upper bound.

Additional Inherited Members
Public Types inherited from dlinear::TheorySolver
using	Bound = std::tuple<const Variable &, LpColBound, const mpq_class &>
	Bound on the variable.

using	Violation = BoundIterator
	Bound iterator over some violated bounds.

using	Explanations = std::set<LiteralSet>
	Set of explanations of the conflict.

Protected Types inherited from dlinear::TheorySolver
enum class	BoundViolationType { NO_BOUND_VIOLATION , LOWER_BOUND_VIOLATION , UPPER_BOUND_VIOLATION }
	Enum used to describe how the bounds on a variable participate in the infeasibility result of an LP problem. More...

Protected Member Functions inherited from dlinear::SoplexTheorySolver
void	UpdateModelBounds () override
	Update each variable in the model with the bounds passed to the theory solver.

void	UpdateModelSolution () override
	Update the model with the solution obtained from the LP solver.

void	UpdateExplanation (LiteralSet &explanation) override
	Use the result from the theory solver to update the explanation with the conflict that has been detected.

void	EnableSpxRow (int spx_row)
	Enable the `spx_row` row for the LP solver.

void	DisableSpxRows ()
	Disable all disabled spx rows from the LP solver.

soplex::DSVectorRational	ParseRowCoeff (const Formula &formula)
	Parse a `formula` and return the vector of coefficients to apply to the decisional variables.

void	SetSPXVarCoeff (soplex::DSVectorRational &coeffs, const Variable &var, const mpq_class &value) const
	Set the coefficients to apply to `var` on a specific row.

void	GetSpxInfeasibilityRay (soplex::VectorRational &farkas_ray)
	Get the infeasibility ray of the LP problem.

void	GetSpxInfeasibilityRay (soplex::VectorRational &farkas_ray, std::vector< BoundViolationType > &bounds_ray)
	Get the infeasibility rays of the LP problem.

std::vector< std::pair< int, soplex::Rational > >	GetActiveRows ()
	Get all active rows in the current solution.

std::vector< std::pair< int, soplex::Rational > >	GetActiveRows (const std::vector< int > &spx_rows)
	Get active rows in the current solution among the rows in `spx_rows`.

std::optional< soplex::Rational >	IsRowActive (int spx_row)
	Check if the `spx_row` is active.

bool	IsRowActive (int spx_row, const soplex::Rational &value)
	Check if the `spx_row` is active with value `value`.

Protected Member Functions inherited from dlinear::TheorySolver
void	UpdateExplanations (Explanations &explanations)
	Use the result from the theory solver to update the explanations with the conflict that has been detected.

Protected Attributes inherited from dlinear::SoplexTheorySolver
soplex::SoPlex	spx_
	SoPlex exact LP solver.

soplex::LPColSetRational	spx_cols_
	Columns of the LP problem.

soplex::LPRowSetRational	spx_rows_
	Rows of the LP problem.

std::vector< mpq_class >	spx_rhs_
	Right-hand side of the rows.

std::vector< LpRowSense >	spx_sense_
	Sense of the rows.

Protected Attributes inherited from dlinear::TheorySolver
const Config &	config_
	Configuration of the theory solver.

bool	is_consolidated_
	Whether the solver has been consolidated.

const PredicateAbstractor &	predicate_abstractor_
	Predicate abstractor used to create the theory solver.

std::map< Variable::Id, int >	var_to_theory_col_
	Variable ⇔ theory column.

std::vector< Variable >	theory_col_to_var_
	Theory column ⇔ Variable.

std::map< Variable::Id, int >	lit_to_theory_row_
	Literal ⇔ theory row.

std::vector< Literal >	theory_row_to_lit_
	Theory row ⇔ Literal The row is the constraint used by the theory solver.

std::vector< bool >	theory_rows_state_
	Whether each theory row is enabled or not.

BoundPreprocessor	fixed_preprocessor_
	Preprocessor for the bounds. Only computed on fixed literal theories.

BoundPreprocessor	preprocessor_
	Preprocessor for the bounds.

Box	model_
	Model produced by the theory solver.

IterationStats	stats_
	Statistics of the theory solver.

Static Protected Attributes inherited from dlinear::SoplexTheorySolver
static mpq_class	infinity_ {soplex::infinity}
	Positive infinity.

static mpq_class	ninfinity_ {-soplex::infinity}
	Negative infinity.

Detailed Description

Complete solver using SoPlex.

The linear is problem exactly, also dealing with strict inequalities. As a tradeoff, the objective function is used internally, so it is not possible to maximise or minimise an arbitrary expression.

Definition at line 39 of file CompleteSoplexTheorySolver.h.

Member Function Documentation

◆ AddLiteral()

void dlinear::CompleteSoplexTheorySolver::AddLiteral	(	const Variable &	formula_var,
		const Formula &	formula )

overridevirtual

Add a Literal to the theory solver.

A Literal is formed by a variable that corresponds to a theory formula inside the PredicateAbstractor and the formula itself

Parameters

formula_var	boolean variable that corresponds to the theory formula
formula	symbolic formula that represents the theory formula

Implements dlinear::TheorySolver.

Definition at line 63 of file CompleteSoplexTheorySolver.cpp.

◆ AddVariable()

void dlinear::CompleteSoplexTheorySolver::AddVariable ( const Variable & var )

overridevirtual

Add a variable (column) to the theory solver.

Parameters

var	variable to add

Implements dlinear::TheorySolver.

Definition at line 56 of file CompleteSoplexTheorySolver.cpp.

◆ Consolidate()

void dlinear::CompleteSoplexTheorySolver::Consolidate ( const Box & box )

overrideprivatevirtual

Consolidate the solver.

This method must be called after all the literals have been added to the solver and before calling any other method. Once the solver has been consolidated, no more literals can be added to it. A previously added literal can be enabled using the EnableLiteral method and disabled with Reset.

Note: A solver can be consolidated only once. If you need to change the variables or constraints, you must create a new theory solver.

Parameters

box	box with the bounds for the variables

Reimplemented from dlinear::TheorySolver.

Definition at line 233 of file CompleteSoplexTheorySolver.cpp.

◆ DisableNqLiterals()

void dlinear::CompleteSoplexTheorySolver::DisableNqLiterals ( const std::set< std::size_t > & nq_constraints )

private

Disable the non-equal constraints in the given set.

Each element of nq_constraints is the index of the non-equal constraint that should be disabled. The corresponding row in the LP problem will become a free row. The effect can be undone by calling EnableNqLiterals with force = true.

Note: The indexes in nq_constraints will be converted back to the theory_rows using nq_row_to_theory_rows_.

Parameters

nq_constraints indexes of the non-equal constraints to be disabled

See also: EnableNqLiterals

Definition at line 286 of file CompleteSoplexTheorySolver.cpp.

◆ EnableLiteral()

CompleteSoplexTheorySolver::Explanations dlinear::CompleteSoplexTheorySolver::EnableLiteral ( const Literal & lit )

overridevirtual

Activate the literal that had previously been added to the theory solver.

If the literal is a row inside the TheorySolver, then the the corresponding constraint is activated by giving it the proper values.

If the literal is a simple bound on the variable (column), some additional checks are made. Theory solvers struggle to handle problems with inverted bounds. It is convenient to have a method that checks them beforehand. If at least a bound is inverted, the problem is UNSAT, since it is impossible to satisfy the constraint. An explanation is produced and returned to the SAT solver.

Parameters

lit	literal to activate

Returns: an explanation with the literals that correspond to the conflicting bounds; an empty optional if no conflicts are detected at this step

Implements dlinear::TheorySolver.

Definition at line 93 of file CompleteSoplexTheorySolver.cpp.

◆ EnableNqLiteral()

void dlinear::CompleteSoplexTheorySolver::EnableNqLiteral	(	int	spx_row,
		bool	truth )

private

Enable the non-equal constraint at row spx_row based on the given truth.

The boolean value of truth indicates if the corresponding non-equal should be converted to

\[ \begin{cases} \text{lhs} < \text{rhs} & \text{if truth} = \text{false} \newline \text{lhs} > \text{rhs} & \text{if truth} = \text{true} \end{cases} \]

Parameters

spx_row	the row in the LP problem to be enabled
truth	the sense of the non-equal constraint

See also: EnableNqLiterals

Definition at line 253 of file CompleteSoplexTheorySolver.cpp.

◆ EnableNqLiterals()

void dlinear::CompleteSoplexTheorySolver::EnableNqLiterals	(	const std::vector< bool > &	nq_status,
		bool	force = false )

private

Enable the non-equal constraints based on the current iterator value nq_status.

Each element of nq_status is a boolean that indicates if the corresponding non-equal should be converted to a \( < \) (if false) or \( > \) (if true) constraint. If nq_status is empty (there are no not-equal constraints), this will do nothing.

Note: The indexes in nq_constraints will be converted back to the theory_rows using nq_row_to_theory_rows_.

Warning: Rows where the last_nq_status_ is equal to the current nq_status will not be updated, unless force is set to true.

Parameters

nq_status the current state of the non-equal constraints

See also: DisableNqLiterals

Definition at line 276 of file CompleteSoplexTheorySolver.cpp.

◆ EnableSpxRow()

void dlinear::CompleteSoplexTheorySolver::EnableSpxRow	(	int	spx_row,
		bool	truth )

overrideprivatevirtual

Enable the spx_row row for the LP solver.

Precondition: The row's coefficients must have been set correctly before calling this function

Parameters

spx_row	index of the row to enable
truth	truth value of the row

Implements dlinear::SoplexTheorySolver.

Definition at line 446 of file CompleteSoplexTheorySolver.cpp.

◆ EnableSpxVarBound()

void dlinear::CompleteSoplexTheorySolver::EnableSpxVarBound ( )

overrideprivatevirtual

Set the bounds of the variables in the LP solver.

Reimplemented from dlinear::SoplexTheorySolver.

Definition at line 431 of file CompleteSoplexTheorySolver.cpp.

◆ GetExplanation()

void dlinear::CompleteSoplexTheorySolver::GetExplanation ( Explanations & explanations )

private

Add a new explanation to explanations from theory_rows_to_explanations_.

Parameters

[out] explanations the set of explanations to add the new explanation to

Definition at line 353 of file CompleteSoplexTheorySolver.cpp.

◆ IteratorNqRowsInLastExplanation()

std::set< size_t > dlinear::CompleteSoplexTheorySolver::IteratorNqRowsInLastExplanation ( ) const

private

Find the non-equal rows in the current explanation.

Returns: vector of the non-equal rows in the current explanation

Definition at line 366 of file CompleteSoplexTheorySolver.cpp.

◆ Reset()

void dlinear::CompleteSoplexTheorySolver::Reset ( )

overridevirtual

Reset the linear problem.

All constraints' state will be set to disabled and the bounds for each variable will be cleared.

Note: The variables and constraints themselves will not be modified. If you need to change them, you must create a new theory solver.

Reimplemented from dlinear::TheorySolver.

Definition at line 223 of file CompleteSoplexTheorySolver.cpp.

◆ SpxCheckSat()

SatResult dlinear::CompleteSoplexTheorySolver::SpxCheckSat ( )

private

Internal method to check the satisfiability of the current LP problem.

It invokes the LP solver and returns the result. If the LP problem is infeasible (or strictly infeasible), it will also update the explanation.

Precondition: The expected precision must be 0.

Returns: The result of the SAT check

See also: theory_rows_to_explanations_.

Definition at line 192 of file CompleteSoplexTheorySolver.cpp.

◆ UpdateBitIncrementIteratorBasedOnExplanation()

bool dlinear::CompleteSoplexTheorySolver::UpdateBitIncrementIteratorBasedOnExplanation ( BitIncrementIterator & bit_iterator )

private

Update the BitIncrementIterator bit_iterator based on the current explanation.

The bit_iterator is used to explore the sub-problems produced by considering the non-equal constraints. It uses some heuristics to update the iterator based on the current explanation to skip redundant sub-problems. Once an infeasibility is detected, the IteratorNqRowsInLastExplanation method is used to determine which non-equal constraints are part of the explanation. If there is only one non-equal row responsible, the iterator learns to skip all future subproblems that contain that row in the same configuration. All the non-equal rows in the explanation are then temporarily disabled, to find any other infeasibilities, repeating the process untill what remains is feasible. The explanation collected this way are stored in the appropriate nq_explanations_. Configurations that have been visited before are immediately skipped. If all possible configurations of a subset non-equal rows have been explored, we can return immediately knowing the problem is infeasible.

Precondition: The subproblem without the non-equal constraints must be feasible.

Parameters

bit_iterator the iterator used to explore the sub-problems to be updated

Returns: true if the loop should continue to enumerate the sub-problems; false if there is no point in continuing the loop and it can be stopped with the current explanation

Definition at line 377 of file CompleteSoplexTheorySolver.cpp.

◆ UpdateExplanationStrictInfeasible()

void dlinear::CompleteSoplexTheorySolver::UpdateExplanationStrictInfeasible ( )

private

Update the explanation with the current LP solution.

A solution has been found, but a strict inequality has been violated. The explanation must be updated using an artificial infeasibility core.

Definition at line 319 of file CompleteSoplexTheorySolver.cpp.

Member Data Documentation

◆ last_nq_status_

std::vector<bool> dlinear::CompleteSoplexTheorySolver::last_nq_status_

private

Last status of the non-equal constraints.

Keeps track last sense of the constraints: \( < \) (false) or \( > \) (true).

Definition at line 171 of file CompleteSoplexTheorySolver.h.

◆ single_nq_rows_

std::set<std::pair<std::size_t, bool> > dlinear::CompleteSoplexTheorySolver::single_nq_rows_

private

Set of non-equal rows that appear alone in the explanation, with the current assignment.

Can be inverted at the next iteration

Definition at line 181 of file CompleteSoplexTheorySolver.h.

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

dlinear/solver/CompleteSoplexTheorySolver.h
dlinear/solver/CompleteSoplexTheorySolver.cpp

Classes

Public Member Functions

Private Member Functions

Private Attributes

Static Private Attributes

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ AddLiteral()

◆ AddVariable()

◆ Consolidate()

◆ DisableNqLiterals()

◆ EnableLiteral()

◆ EnableNqLiteral()

◆ EnableNqLiterals()

◆ EnableSpxRow()

◆ EnableSpxVarBound()

◆ GetExplanation()

◆ IteratorNqRowsInLastExplanation()

◆ Reset()

◆ SpxCheckSat()

◆ UpdateBitIncrementIteratorBasedOnExplanation()

◆ UpdateExplanationStrictInfeasible()

Member Data Documentation

◆ last_nq_status_

◆ single_nq_rows_