From 43d14031f96dfcd0f624a0589ab29b906ce34dd7 Mon Sep 17 00:00:00 2001 From: Gleb Belov Date: Sat, 20 Jul 2024 21:41:18 +1000 Subject: [PATCH] SolCheck docs: find violated constraints #200 --- doc/source/modeling-tools.rst | 36 +++++++++++++++++++++++++++-- include/mp/flat/problem_flattener.h | 11 +++++++-- 2 files changed, 43 insertions(+), 4 deletions(-) diff --git a/doc/source/modeling-tools.rst b/doc/source/modeling-tools.rst index c9dd531f6..eb7af0fcc 100644 --- a/doc/source/modeling-tools.rst +++ b/doc/source/modeling-tools.rst @@ -267,7 +267,7 @@ Consider the disjunction constraint With ``y=6.0000000001`` and ``z=9.9999999999``, and assuming the solver's feasibility tolerance is at a typical value (such as :math:`10^{-6}`), most Mathematical Programming solvers consider the disjunction satisfied. -And, from a practical viewpoint, it is (given finite-precision +And, from a practical viewpoint, it might be (given finite-precision computations). Our :ref:`Realistic checking mode ` does exactly this: @@ -285,8 +285,15 @@ In contrast, AMPL reports the constraint violated: That is, when expressions ``y<=6`` and ``z>=10`` are re-evaluated and their results substituted into ``C``, ``C`` holds false. +To check validity of a group of logical constraints in AMPL, +use a statement such as this: -The role of the :ref:`Idealistic mode ` +.. code-block:: ampl + + display {i in 1.._nlogcons: !_logcon[i].val} (_logconname[i]); + + +In contrast, the role of the :ref:`Idealistic mode ` is to warn the user about the fact, that even if the solver has a correct solution up to its tolerances (which is examined by the "realistic" mode), @@ -339,6 +346,21 @@ There is an absolute violation of 3 and relative violation of 1 in the objective Linear constraint `C2` has its absolute and relative violations reported. Lines marked with a `*` report :ref:`Realistic violations `. +If the relative violation is missing, the respective constraint has +right-hand side 0: + +.. code-block:: ampl + + WARNING: "Tolerance violations" + Type MaxAbs [Name] MaxRel [Name] + * algebraic con(s) 9E-03 - + *: Using the solver's aux variable values. + Documentation: mp.ampl.com/modeling-tools.html#automatic-solution-check. + + +For such constraints, the significance of the violation +depends on the left-hand side coefficients and variable values. + To check the violations, we can recompute objective value and constraint slacks, as follows: @@ -351,6 +373,15 @@ as follows: C2.slack = -1 +To check validity of a group of algebraic constraints in AMPL, +use a statement such as this: + +.. code-block:: ampl + + display {i in 1.._ncons: _con[i].slack < -1e-3} (_conname[i], _con[i].slack); + + + .. _constr-list: Expression list @@ -390,6 +421,7 @@ that the solver's reported solution violates checking tolerances. *: Using the solver's aux variable values. Documentation: mp.ampl.com/modeling-tools.html#automatic-solution-check. +Lines marked with a `*` report the "realistic" violations. Such warning can appear when solving the following example with Gurobi 11 which uses piecewise-linear approximation by default: diff --git a/include/mp/flat/problem_flattener.h b/include/mp/flat/problem_flattener.h index 702dd7383..f6c82e178 100644 --- a/include/mp/flat/problem_flattener.h +++ b/include/mp/flat/problem_flattener.h @@ -1236,10 +1236,17 @@ class ProblemFlattener : " following order: integer terms first, " " then real-valued ones; in each group, " " smaller-range terms first.\n" - "| 2 - Logicalize products of 2 binary terms.\n" + "| 2 - Logicalize products of 2 binary terms. Logicalizing " + " means that the product is converted to a conjunction. " + " If the solver does not support it natively (see acc:and), " + " the conjunction is linearized.\n" "| 4 - Logicalize products of >=3 binary terms.\n" "\n" - "Default: 1+4. Bits 2 or 4 imply bit 1.", + "Default: 1+4. That is, 2-term binary products which are not " + "part of a higher-order binary product, are not logicalized " + "by default.\n" + "\n" + "Bits 2 or 4 imply bit 1.", options_.prepro_products_, 0, 1023); }