diff --git a/dlinear/libs/libgmp.h b/dlinear/libs/libgmp.h index 12bfbe64..0f8b377f 100644 --- a/dlinear/libs/libgmp.h +++ b/dlinear/libs/libgmp.h @@ -86,8 +86,7 @@ inline mpq_t &to_mpq_t(mpq_class &cla) { return *reinterpret_cast(cla.g * Cast a mpq_t to a mpq_class. * * This works because the internal representation of a mpq_class is exactly - * the same as that of a mpq_t (and, because we only take a reference, no - * constructor or destructor is ever called). + * the same as that of a mpq_t (and, because we only take a reference, no constructor or destructor is ever called). * @param mpq mpq_t to cast * @return mpq_class reference */ @@ -97,8 +96,7 @@ inline const mpq_class &to_mpq_class(const mpq_t &mpq) { return reinterpret_cast * Cast a mpq_t to a mpq_class. * * This works because the internal representation of a mpq_class is exactly - * the same as that of a mpq_t (and, because we only take a reference, no - * constructor or destructor is ever called). + * the same as that of a mpq_t (and, because we only take a reference, no constructor or destructor is ever called). * @param mpq mpq_t to cast * @return mpq_class reference */ @@ -106,9 +104,9 @@ inline mpq_class &to_mpq_class(mpq_t &mpq) { return reinterpret_cast(array)[-1] : 0; } /** diff --git a/dlinear/parser/Driver.h b/dlinear/parser/Driver.h index b91357c2..87ac1b91 100644 --- a/dlinear/parser/Driver.h +++ b/dlinear/parser/Driver.h @@ -153,6 +153,12 @@ class Driver { [[nodiscard]] const Stats &stats() const { return stats_; } protected: + /** + * Parse the stream. + * @param in input stream + * @return true if successfully parsed + * @return false if an error occurred + */ virtual bool ParseStreamCore(std::istream &in) = 0; std::string stream_name_; ///< The name of the stream being parsed. diff --git a/dlinear/parser/mps/BoundType.cpp b/dlinear/parser/mps/BoundType.cpp index fc4124cb..b77f855c 100644 --- a/dlinear/parser/mps/BoundType.cpp +++ b/dlinear/parser/mps/BoundType.cpp @@ -16,6 +16,7 @@ BoundType ParseBoundType(const std::string& bound_type) { return ParseBoundType( BoundType ParseBoundType(const char bound_type[]) { while (*bound_type == ' ') ++bound_type; + DLINEAR_ASSERT(strlen(bound_type) == 2, "Bound type must be exactly 2 characters long"); if (bound_type[2] != '\0' && bound_type[2] != ' ') DLINEAR_RUNTIME_ERROR_FMT("Invalid bound type: '{}'", bound_type); if ((bound_type[0] == 'l' || bound_type[0] == 'L') && (bound_type[1] == 'o' || bound_type[1] == 'O')) { return BoundType::LO; diff --git a/dlinear/parser/mps/BoundType.h b/dlinear/parser/mps/BoundType.h index ad8473c7..9c331d29 100644 --- a/dlinear/parser/mps/BoundType.h +++ b/dlinear/parser/mps/BoundType.h @@ -71,7 +71,7 @@ BoundType ParseBoundType(const std::string &bound_type); * * Any leading or trailing spaces are ignored. * The input is case-insensitive. - * + * @pre The input must be exactly 2 characters long. * @param bound_type C-string representation of the bound type * @return corresponding bound type */ diff --git a/dlinear/parser/mps/Driver.h b/dlinear/parser/mps/Driver.h index c3903e2c..3e9de7ab 100644 --- a/dlinear/parser/mps/Driver.h +++ b/dlinear/parser/mps/Driver.h @@ -187,16 +187,30 @@ class MpsDriver : public Driver { */ void End(); + /** @getter{problem_name, MpsDriver} */ [[nodiscard]] const std::string &problem_name() const { return problem_name_; } + /** @getsetter{problem_name, MpsDriver} */ std::string &m_problem_name() { return problem_name_; } + /** @checker{enabled, strict mps} */ [[nodiscard]] bool strict_mps() const { return strict_mps_; } + /** + * Set the strict mps mode. + * @param b new value of the strict mps mode + */ void set_strict_mps(bool b) { strict_mps_ = b; } + /** @getter{number of assertions, MpsDriver} */ [[nodiscard]] std::size_t n_assertions() const { return rhs_.size() + bounds_.size(); } + /** @checker{enabled, minimization} */ [[nodiscard]] bool is_min() const { return is_min_; } + /** @getter{objective row name, MpsDriver} */ [[nodiscard]] const std::string &obj_row() const { return obj_row_; } + /** @getter{scanner, MpsDriver} */ + [[nodiscard]] MpsScanner *scanner() { return scanner_; } - MpsScanner *scanner() { return scanner_; } - + /** + * Print the problem in the smt2 format. + * @param os output stream + */ void ToSmt2(std::ostream &os) const; private: diff --git a/dlinear/parser/mps/Sense.h b/dlinear/parser/mps/Sense.h index 2ddaffcc..38434f7a 100644 --- a/dlinear/parser/mps/Sense.h +++ b/dlinear/parser/mps/Sense.h @@ -37,7 +37,6 @@ enum class Sense { * * Any leading or trailing spaces are ignored. * The input is case-insensitive. - * * @param sense string representation of the sense * @return corresponding sense */ @@ -52,7 +51,6 @@ Sense ParseSense(const std::string &sense); * * Any leading or trailing spaces are ignored. * The input is case-insensitive. - * * @param sense C-style string representation of the sense * @return corresponding sense */ @@ -66,7 +64,6 @@ Sense ParseSense(const char sense[]); * - 'N' * * The input is case-insensitive. - * * @param sense character representation of the sense * @return corresponding sense */ diff --git a/dlinear/solver/Bound.h b/dlinear/solver/Bound.h index 3ce7e0c5..e83a84a4 100644 --- a/dlinear/solver/Bound.h +++ b/dlinear/solver/Bound.h @@ -14,7 +14,13 @@ namespace dlinear { -/** Bound. It is a tuple of value, bound type and index */ +/** + * Tuple containing the value, bound type and theory literal associated with the bound. + * + * It may also contain an explanation for the existence of the bound used to produce an explanation. + * @note For efficiency purposes, the value is just a pointer to the actual value. + * Therefore, it is important to ensure that the value is not deallocated while the bound is in use. + */ struct Bound { Bound() = default; Bound(const mpq_class* value_, LpColBound lp_bound_, Literal theory_literal_, LiteralSet explanation_) diff --git a/dlinear/solver/BoundPreprocessor.h b/dlinear/solver/BoundPreprocessor.h index 4c449b9a..9ce08104 100644 --- a/dlinear/solver/BoundPreprocessor.h +++ b/dlinear/solver/BoundPreprocessor.h @@ -39,21 +39,112 @@ class BoundPreprocessor { using Explanations = std::set; using VarToEqBinomialMap = std::unordered_map; + /** + * Construct a new Bound Preprocessor object using the @p predicate_abstractor. + * @param predicate_abstractor predicate abstractor containing the map between the variables and the literals + */ explicit BoundPreprocessor(const PredicateAbstractor& predicate_abstractor); + /** + * Add a theory variable to the preprocessor. + * + * It will create a new entry in the theory_bounds_ map. + * @param var theory variable to add + */ void AddVariable(const Variable& var); + /** + * Preprocess all the @p enabled_literals. + * + * It will enable the literals and propagate the bounds. + * If a conflict is detected, it will return the set of explanations. + * Enabled literals are cached and will not be enabled again in the future. + * @param enabled_literals literals to enable + * @return set of explanations from the enabled literals if a conflict is detected + * @return empty set if no conflict is detected + */ std::set EnableLiterals(const std::vector& enabled_literals); + /** + * Preprocess all the @p enabled_literals. + * + * It will enable the literals and propagate the bounds. + * If a conflict is detected, it will return the set of explanations. + * Enabled literals are cached and will not be enabled again in the future. + * @param enabled_literals literals to enable + * @param[out] explanations set of explanations from the enabled literals if a conflict is detected + */ void EnableLiterals(const std::vector& enabled_literals, std::set& explanation); + /** + * Enable the literal @p lit. + * + * It will enable the literal and propagate the bounds. + * If a conflict is detected, it will return the set of explanations. + * Enabled literals are cached and will not be enabled again in the future. + * @param lit literal to enable + * @return set of explanations from the enabled literal if a conflict is detected + * @return empty set if no conflict is detected + */ std::set EnableLiteral(const Literal& lit); + /** + * Enable the literal @p lit. + * + * It will enable the literal and propagate the bounds. + * If a conflict is detected, it will return the set of explanations. + * Enabled literals are cached and will not be enabled again in the future. + * @param lit literal to enable + * @param[out] explanations set of explanations from the enabled literal if a conflict is detected + */ void EnableLiteral(const Literal& lit, std::set& explanations); + /** + * Process all enabled literals. + * + * It will process the enabled literals and propagate the bounds. + * The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated. + * If a conflict is detected, it will return the set of explanations. + * @return set of explanations from the enabled literals if a conflict is detected + * @return empty set if no conflict is detected + */ Explanations Process(); + /** + * Process all enabled literals. + * + * It will process the enabled literals and propagate the bounds. + * The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated. + * If a conflict is detected, it will return the set of explanations. + * @param[out] explanations set of explanations from the enabled literals if a conflict is detected + */ void Process(Explanations& explanations); + /** + * Process the enabled literals @p enabled_literals. + * + * It will process the enabled literals and propagate the bounds. + * The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated. + * If a conflict is detected, it will return the set of explanations. + * @param enabled_literals literals to enable + * @return set of explanations from the enabled literals if a conflict is detected + * @return empty set if no conflict is detected + */ Explanations Process(const LiteralSet& enabled_literals); + /** + * Process the enabled literals @p enabled_literals. + * + * It will process the enabled literals and propagate the bounds. + * The bounds are propagated based on the BoundPropagationType and the formulae will be evaluated. + * If a conflict is detected, it will return the set of explanations. + * @param enabled_literals literals to enable + * @param[out] explanations set of explanations from the enabled literals if a conflict is detected + */ void Process(const LiteralSet& enabled_literals, Explanations& explanations); + /** + * Get the active explanation for the variable @p var. + * + * It will return the explanation for the variable @p var, justifying the active bounds. + * @param var variable to get the explanation for + * @param[out] explanation explanation for the variable @p var + */ void GetActiveExplanation(const Variable& var, LiteralSet& explanation); /** @@ -66,7 +157,19 @@ class BoundPreprocessor { */ void SetInfinityBounds(const Variable& var, const mpq_class& lb, const mpq_class& ub); + /** + * Clear the preprocessor. + * + * It will clear the environment, the theory bounds, and the enabled literals. + */ void Clear(); + /** + * Clear the preprocessor using the @p fixed_preprocessor. + * + * It will clear the environment, the theory bounds, and the enabled literals by copying the values from the + * @p fixed_preprocessor. + * @param fixed_preprocessor preprocessor to use as a reference + */ void Clear(const BoundPreprocessor& fixed_preprocessor); /** @getter{configuration, BoundPreprocessor} */ diff --git a/dlinear/solver/CadicalSatSolver.h b/dlinear/solver/CadicalSatSolver.h index a0312422..b01135a6 100644 --- a/dlinear/solver/CadicalSatSolver.h +++ b/dlinear/solver/CadicalSatSolver.h @@ -57,8 +57,8 @@ class CadicalSatSolver : public SatSolver { private: [[nodiscard]] std::set GetMainActiveLiterals() override; - CaDiCaL::Solver sat_{}; - int next_var_id_{1}; + CaDiCaL::Solver sat_{}; ///< SAT solver + int next_var_id_{1}; ///< Next variable id }; } // namespace dlinear diff --git a/dlinear/solver/ContextImpl.cpp b/dlinear/solver/ContextImpl.cpp index 4519daae..d93c0357 100644 --- a/dlinear/solver/ContextImpl.cpp +++ b/dlinear/solver/ContextImpl.cpp @@ -69,8 +69,8 @@ Context::Impl::Impl(Config &config, SmtSolverOutput *const output) } void Context::Impl::Assert(const Formula &f) { - if (is_true(f)) return; // Skip trivially true assertions. - if (is_false(f)) { // The formula is false. No point in adding it to the SAT solver. There is no point in continuing + if (is_true(f)) return; // Skip trivially true assertions. + if (is_false(f)) { // The formula is false. No point in adding it to the SAT solver. There is no point in continuing stack_.push_back(f); return; } diff --git a/docs/Installation.md b/docs/Installation.md index 48a642a5..ba5fc4be 100644 --- a/docs/Installation.md +++ b/docs/Installation.md @@ -60,7 +60,7 @@ sudo dpkg -i bazel-bin/dlinear/dlinear.deb ```bash # Add the PPA -sudo add-apt-repository ppa:dlinear/dlinear +sudo add-apt-repository ppa:tendto/dlinear # Update the package list sudo apt update # Install dlinear diff --git a/docs/Theory.md b/docs/Theory.md index ca0acb29..527bd302 100644 --- a/docs/Theory.md +++ b/docs/Theory.md @@ -41,8 +41,8 @@ The fundamental property is that the new formula is satisfiable if and only if t The transformation uses three basic operators: -| Original | $ p \iff \text{formula} $ | In CNF | -| ----------- | ----------------------------------------------------- | ------------------------------------------------------------------------- | +| Original | $ p \iff \text{formula} $ | In CNF | +| ----------- | ------------------------------------------------------------------- | ------------------------------------------------------------------------- | | $\neg a$ | $(\neg a \Longrightarrow p) \land (p \Longrightarrow \neg a)$ | $(a \lor p) \land (\neg a \lor \neg p)$ | | $a \land b$ | $(a \land b \Longrightarrow p) \land (p \Longrightarrow a \land b)$ | $(\neg a \lor \neg b \lor p) \land (a \lor \neg p) \land (b \lor \neg p)$ | | $a \lor b$ | $(a \lor b \Longrightarrow p) \land (p \Longrightarrow a \lor b)$ | $(a \lor b \lor \neg p) \land (\neg a \lor p) \land (\neg b \lor p)$ | diff --git a/docs/Todo.md b/docs/Todo.md index 873196b8..2e4a69f7 100644 --- a/docs/Todo.md +++ b/docs/Todo.md @@ -31,7 +31,7 @@ - [ ] Use Ubuntu 23.04+ for gcc 13+ support - [ ] Return multiple explanations instead of just one when dealing with active constraints - [ ] Improve iterations over nq bounds -- [x] Add symbolic preprocessor for constraints in the form of $x \lessgtr y$ +- [x] Add symbolic preprocessor for constraints in the form of $x <> y$ - [ ] Remove completely free variables, especially from nq constraints - [ ] Investigate out of memory - [x] Handle conflicting constraints in preprocessor diff --git a/docs/proofs/.gitignore b/docs/proofs/.gitignore deleted file mode 100644 index 907b30be..00000000 --- a/docs/proofs/.gitignore +++ /dev/null @@ -1,303 +0,0 @@ -## Core latex/pdflatex auxiliary files: -*.aux -*.lof -*.log -*.lot -*.fls -*.out -*.toc -*.fmt -*.fot -*.cb -*.cb2 -.*.lb - -## Intermediate documents: -*.dvi -*.xdv -*-converted-to.* -# these rules might exclude image files for figures etc. -# *.ps -# *.eps -# *.pdf - -## Generated if empty string is given at "Please type another file name for output:" -*.pdf - -## Bibliography auxiliary files (bibtex/biblatex/biber): -*.bbl -*.bcf -*.blg -*-blx.aux -index-blx.bib -*.run.xml - -## Build tool auxiliary files: -*.fdb_latexmk -*.synctex -*.synctex(busy) -*.synctex.gz -*.synctex.gz(busy) -*.pdfsync - -## Build tool directories for auxiliary files -# latexrun -latex.out/ - -## Auxiliary and intermediate files from other packages: -# algorithms -*.alg -*.loa - -# achemso -acs-*.bib - -# amsthm -*.thm - -# beamer -*.nav -*.pre -*.snm -*.vrb - -# changes -*.soc - -# comment -*.cut - -# cprotect -*.cpt - -# elsarticle (documentclass of Elsevier journals) -*.spl - -# endnotes -*.ent - -# fixme -*.lox - -# feynmf/feynmp -*.mf -*.mp -*.t[1-9] -*.t[1-9][0-9] -*.tfm - -#(r)(e)ledmac/(r)(e)ledpar -*.end -*.?end -*.[1-9] -*.[1-9][0-9] -*.[1-9][0-9][0-9] -*.[1-9]R -*.[1-9][0-9]R -*.[1-9][0-9][0-9]R -*.eledsec[1-9] -*.eledsec[1-9]R -*.eledsec[1-9][0-9] -*.eledsec[1-9][0-9]R -*.eledsec[1-9][0-9][0-9] -*.eledsec[1-9][0-9][0-9]R - -# glossaries -*.acn -*.acr -*.glg -*.glo -*.gls -*.glsdefs -*.lzo -*.lzs -*.slg -*.slo -*.sls - -# uncomment this for glossaries-extra (will ignore makeindex's style files!) -*.ist - -# gnuplot -*.gnuplot -*.table - -# gnuplottex -*-gnuplottex-* - -# gregoriotex -*.gaux -*.glog -*.gtex - -# htlatex -*.4ct -*.4tc -*.idv -*.lg -*.trc -*.xref - -# hyperref -*.brf - -# knitr -*-concordance.tex -# TODO Uncomment the next line if you use knitr and want to ignore its generated tikz files -# *.tikz -*-tikzDictionary - -# listings -*.lol - -# luatexja-ruby -*.ltjruby - -# makeidx -*.idx -*.ilg -*.ind - -# minitoc -*.maf -*.mlf -*.mlt -*.mtc[0-9]* -*.slf[0-9]* -*.slt[0-9]* -*.stc[0-9]* - -# minted -_minted* -*.pyg - -# morewrites -*.mw - -# newpax -*.newpax - -# nomencl -*.nlg -*.nlo -*.nls - -# pax -*.pax - -# pdfpcnotes -*.pdfpc - -# sagetex -*.sagetex.sage -*.sagetex.py -*.sagetex.scmd - -# scrwfile -*.wrt - -# svg -svg-inkscape/ - -# sympy -*.sout -*.sympy -sympy-plots-for-*.tex/ - -# pdfcomment -*.upa -*.upb - -# pythontex -*.pytxcode -pythontex-files-*/ - -# tcolorbox -*.listing - -# thmtools -*.loe - -# TikZ & PGF -*.dpth -*.md5 -*.auxlock - -# titletoc -*.ptc - -# todonotes -*.tdo - -# vhistory -*.hst -*.ver - -# easy-todo -*.lod - -# xcolor -*.xcp - -# xmpincl -*.xmpi - -# xindy -*.xdy - -# xypic precompiled matrices and outlines -*.xyc -*.xyd - -# endfloat -*.ttt -*.fff - -# Latexian -TSWLatexianTemp* - -## Editors: -# WinEdt -*.bak -*.sav - -# Texpad -.texpadtmp - -# LyX -*.lyx~ - -# Kile -*.backup - -# gummi -.*.swp - -# KBibTeX -*~[0-9]* - -# TeXnicCenter -*.tps - -# auto folder when using emacs and auctex -./auto/* -*.el - -# expex forward references with \gathertags -*-tags.tex - -# standalone packages -*.sta - -# Makeindex log files -*.lpz - -# xwatermark package -*.xwm - -# REVTeX puts footnotes in the bibliography by default, unless the nofootinbib -# option is specified. Footnotes are the stored in a file with suffix Notes.bib. -# Uncomment the next line to have this generated file ignored. -#*Notes.bib - -sources/ diff --git a/docs/proofs/index.tex b/docs/proofs/index.tex deleted file mode 100644 index 05dcd8e4..00000000 --- a/docs/proofs/index.tex +++ /dev/null @@ -1,198 +0,0 @@ -\documentclass[preview,border=12pt,varwidth]{report} -\usepackage{amsthm} -\usepackage{amssymb} -\usepackage{amsmath} -\usepackage{hyperref} - -\title{Strict inequalities in linear programming problems for SMT solving} -\author{Ernesto Casabalanca} -\date{\today} - -\renewcommand*{\equationautorefname}{} -\newcommand{\framedtext}[1]{% -\par% -\noindent\fbox{% - \parbox{\dimexpr\linewidth-2\fboxsep-2\fboxrule}{#1}% -}% -} - -\newtheorem{theorem}{Theorem} -\newtheorem{definition}{Definition} - -\begin{document} -\maketitle - -\section*{Definitions} - -\begin{definition} - A \textbf{linear programming problem} is a mathematical optimization where the goal is to maximise or minimise a linear \textbf{objective function} subject to a set of linear \textbf{constraints}. The general form of a linear programming problem is - - \begin{align*} - \text{Maximise (or minimise) } \quad & c_1x_1 + c_2x_2 + \ldots + c_nx_n \\ - \text{subject to } \quad & a_{11} x_1 + a_{12} x_2 + \ldots + a_{1n} x_n \gtreqless b_1 \\ - & a_{21} x_1 + a_{22} x_2 + \ldots + a_{2n} x_n \gtreqless b_2 \\ - & \vdots \\ - & a_{m1} x_1 + a_{m2} x_2 + \ldots + a_{mn} x_n \gtreqless b_m \\ - \end{align*} - - where $x_1, x_2, \ldots, x_n \in \mathbb{R}$ are \textbf{decision variables}, $c_1, c_2, \ldots, c_n \in \mathbb{R}$ are coefficients of the objective function, $a_{11}, a_{12}, \ldots, a_{mn} \in \mathbb{R}$ are coefficients of the constraints, and $b_1, b_2, \ldots, b_m \in \mathbb{R}$ are constants. -\end{definition} - -\begin{definition} - A linear programming problem is said to be in \textbf{standard form} if the objective function is to be maximised, the constraints are of the form $\leq$, and all the decision variables are non-negative. - - \begin{align*} - \text{Maximise } \quad & c_1x_1 + c_2x_2 + \ldots + c_nx_n \\ - \text{subject to } \quad & a_{11} x_1 + a_{12} x_2 + \ldots + a_{1n} x_n \leq b_1 \\ - & a_{21} x_1 + a_{22} x_2 + \ldots + a_{2n} x_n \leq b_2 \\ - & \vdots \\ - & a_{m1} x_1 + a_{m2} x_2 + \ldots + a_{mn} x_n \leq b_m \\ - & x_1, x_2, \ldots, x_n \geq 0 \\ - \end{align*} -\end{definition} - -\begin{theorem} - It is always possible to convert a linear programming problem from standard form to general form as long as the goal is to either maximise or minimise the objective function and the constraints are of the form $\le, \ge, =$. -\end{theorem} -\begin{proof} - It is useful to enumerate all the possible violations of the standard form and how they can be removed. - \begin{itemize} - \item \textbf{Minimisation problem}: the objective function can be multiplied by $-1$ to convert it to a maximisation problem, since $\min(f(x)) = -\max(-f(x))$. - \item \textbf{Constraints with $\geq$}: they can be multiplied by $-1$ to convert them to the form $\leq$. - \item \textbf{Constraints with $=$}: they can be replaced by two constraints of the form $\leq$ and $\geq$. - The latter is to be converted, as seen above. - \item \textbf{Unrestricted decision variables} can be replaced by the difference of two non-negative variables. - \end{itemize} -\end{proof} - -\begin{definition} - Constraints can be of different types: - - \begin{itemize} - \item \textbf{Strict inequality}: is an inequality that is either $<$ or $>$ - \item \textbf{Non-strict inequality}: is an inequality that is either $\leq$ or $\geq$ - \item \textbf{Not-equality}: an inequality $\neq$ - \item \textbf{Equality}: an equality $=$ - \end{itemize} -\end{definition} - -Standard linear programming problems only deal with non-strict inequalities and equalities. - -\section*{Feasibility} - -\begin{definition} - A linear programming problem is \textbf{feasible} if there exists a solution that satisfies all the constraints. -\end{definition} - - -\begin{definition} - An \textbf{objective value} is the value of the objective function obtained by assigning a set of values to the decision variables corresponding to a feasible solution. - The objective value is said to be \textbf{optimal} if it is the maximum (or minimum) value of the objective function over the feasible region. -\end{definition} - -Verifying the feasibility of a linear programming problem is a core step in solving SMT problems dealing with \textbf{QF\_LIA} and \textbf{QF\_LRA} logics. -There is no reason to find the optimal solution. Hence, the objective function is usually set to the constant $0$. - -Unfortunately, LP solvers do not tackle strict inequalities since that would cause the feasible region to become an open set. -Finding the optimal solution would not make sense, for maximum and minimum do not exist over open sets. -In SMT problems, though, such constraints can arise very often, such as when negating any other non-strict inequality. - -The common approach to deal with this issue in floating point LP solvers is to subtract an arbitrarily small $\epsilon$ to the right-hand side of each strict inequality, making them non-strict. -While valid, using this technique implies the choice of a suitable $\epsilon$ value, which introduces an, albeit controllable, error. -What happens, for instance, if the system is still infeasible after the alteration? -Is the $\epsilon$ value too large, or is the problem inherently infeasible? - -\subsection*{Relaxing strict inequalities} - -A different approach to deal with strict inequalities is to introduce a new variable we will call \textbf{strict variable}, $t$, that will be used to convert strict inequalities into non-strict ones. -To simplify the notation, we only consider $<$ strict inequalities, but the same reasoning can be applied to $>$, since they can always be converted to $<$ by multiplying both sides by $-1$. -Indicate with $J$ the set of indexes of strict inequality constraints and with $K$ the set of indexes for all other constraints. - -The idea is to replace each strict inequality -\begin{align*} - \sum_{i=1}^{n} a_{ji}x_{i} < b_j, \quad \forall j \in J -\end{align*} -with equivalent non strict inequalities using the strict variable $t$: -\begin{align*} - \sum_{i=1}^{n} a_{ji}x_{i} + t \le b_j, \quad \forall j \in J \\ - t > 0 -\end{align*} - -This change would only move the strict inequality problem to the bound on $t$. -However, it is possible to go a step further and relax the newly introduced bound by changing the objective function to maximise to $t$. -The original problem we want to verify the feasibility of - -\begin{equation} - \label{eq:lp-original} - \begin{split} - \text{Maximise } \quad & 0 \\ - \text{subject to } \quad & \sum_{i=1}^{n} a_{ji}x_{i} < b_j, \quad \forall j \in J \\ - \quad & \sum_{i=1}^{n} a_{ki}x_{i} \le b_k, \quad \forall k \in K \\ - & x_i \ge 0, \quad i \in \{1, 2, \ldots, n\}, - \end{split} -\end{equation} - -can be relaxed to - -\begin{equation} - \label{eq:lp-relaxed} - \begin{split} - \text{Maximise } \quad & t \\ - \text{subject to } \quad & \sum_{i=1}^{n} a_{ji}x_{i} + t \le b_j, \quad \forall j \in J \\ - \quad & \sum_{i=1}^{n} a_{ki}x_{i} \le b_k, \quad \forall k \in K \\ - & x_i \ge 0 , \quad i \in \{1, 2, \ldots, n\} \\ - & t \ge 0 - \end{split} -\end{equation} - -\begin{theorem} - The original problem \eqref{eq:lp-original} is feasible if and only if the relaxed problem \eqref{eq:lp-relaxed} is feasible and there exists a solution where the objective value is greater than $0$. -\end{theorem} - -\begin{proof} - Without loss of generality, assume that both linear programming problems are in standard form. - Let $J$ be the set of indexes of strict inequality constraints, and $K$ be the set of indexes for all other constraints. - \\ - \framedtext{\eqref{eq:lp-original} feasible $\implies$ \eqref{eq:lp-relaxed} feasible $\land$ \eqref{eq:lp-relaxed} objective value $> 0$} \\ - - If the original problem is feasible, then there exists a solution, a set of values to be assigned to the decision variables $x_1, x_2, \ldots, x_n$, that satisfies all the constraints. - For the strict inequality constraints to be satisfied, it means that there exists a value $\delta_j > 0, \quad j \in J$ such that - \begin{align*} - \sum_{i=1}^{n} a_{ji}x_{i} + \delta_j = b_j, \quad \forall j \in J - \end{align*} - Let $\bar{t} = \min(\delta_j), \quad j \in J$. - The expression becomes - \begin{align*} - \sum_{i=1}^{n} a_{ji}x_{i} + \bar{t} \le b_j, \quad \forall j \in J \\ - \bar{t} > 0 - \end{align*} - which is the formulation of the previously strict constraints used in the relaxed problem. - All other constraints have been left unchanged, therefore the solution to the original problem can be used to satisfy the constraints of the relaxed problem by also setting $t = \bar{t}$ which is greater than $0$. - Hence, the objective value of the relaxed problem is $> 0$. - \\ - \framedtext{\eqref{eq:lp-relaxed} feasible $\land$ \eqref{eq:lp-relaxed} objective value $> 0$ $\implies$ \eqref{eq:lp-original} feasible} \\ - - The solution to the relaxed problem already satisfies all the non-strict constraints of the original problem. - The objective value is greater than $0$; therefore, $t > 0$. - Since all relaxed constraints in the form - \begin{align*} - \sum_{i=1}^{n} a_{ji}x_{i} + t \le b_j, \quad \forall j \in J \\ - t > 0 - \end{align*} - are satisfied the original strict inequality constraints - \begin{align*} - \sum_{i=1}^{n} a_{ji}x_{i} < b_j, \quad \forall j \in J - \end{align*} - are also satisfied. - Hence, the original problem is feasible. -\end{proof} - -\subsection*{Not equal constraints} - -A similar line of reasoning can be applied to not equal constraints, with a major difference. -Two strict inequalities are needed to check whether the constraint is satisfied, one for each direction. -Since checking both at the same time with an OR conjunction is not possible, the original problem must be split into two. -If the number of not equal constraints is $m$, then $2^m$ problems must be solved. -If any of them is feasible, then it is possible to conclude that the original problem is feasible. - -\end{document} \ No newline at end of file