6
$\begingroup$

The original simplex algorithm requires an exponential number of pivot operations in the worst case, e.g., if run on the Klee-Minty example [3,4].

What about the simplex algorithm used in SMT solvers [1,2]? Could you provide an example where it requires exponential time?

The algorithm I have in mind is by Bruno Dutertre and Leonardo de Moura in [1,2], and is presumably used in all modern SMT solvers. The algorithm introduces one slack variable per constraint, the slack variables have lower and upper bounds; and the problem is that of feasibility instead of optimization.

I tried to modify the Klee-Minty example [3,4], but failed so far. Kroening & Strichman contains this question as an exercise, so you can also hint instead of answering.

  1. Integrating Simplex with DPLL(T) by Bruno Dutertre and Leonardo de Moura:

  2. Decision Procedures: an Algorithmic Point of View by Daniel Kroening and Ofer Strichman

  3. Klee-Minty Polytope Shows Exponential Time Complexity of Simplex Method

  4. Picture of the Klee-Minty cube:

enter image description here

Improve this question
$\endgroup$
3
  • $\begingroup$ I don't know much about SMT solvers but perhaps problems where the number of variables/constraints is exponential in function of some parameter of the problem. $\endgroup$
    – Auberon
    Jun 4, 2016 at 14:11
  • $\begingroup$ not sure i understood you: in the original (optimization) simplex, there is an example [4] that requires exp number of pivot operations to achieve the optimal value -- but this is for optimization, not for feasibility (on the original example, the very first point is already feasible). Likely, the exp example (if exists) for feasibility for original simplex algorithm can be easy-adapted for the particular simplex version [1], but I don't know such example.... $\endgroup$
    – Ayrat
    Jun 4, 2016 at 15:49
  • $\begingroup$ So you're looking for an example so that finding a feasible solution takes exponential time using simplex (or other standard LP solving algorithms)? $\endgroup$
    – Auberon
    Jun 4, 2016 at 16:16

1 Answer 1

Reset to default
-1
$\begingroup$

Here, you can find hard examples for DPLL. http://www.ioc.ee/~tarmo/tday-torve/itsykson-slides.pdf

For instance, it can be very slow for Tseitin formulas and for some unsatisfaisable formulas (it will try many solutions).

I hope it will give you some hints :)

Improve this answer
$\endgroup$
1
  • $\begingroup$ thanks, but your ref is about DPLL (boolean formulas), rather than about simplex (that solves linear arithmetic (conjunctive fragment)) $\endgroup$
    – Ayrat
    May 25, 2016 at 12:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.