# Exponential example for simplex used in SMT solvers

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: • 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. – Auberon Jun 4 '16 at 14:11
• not sure i understood you: in the original (optimization) simplex, there is an example  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 , but I don't know such example.... – Ayrat Jun 4 '16 at 15:49
• So you're looking for an example so that finding a feasible solution takes exponential time using simplex (or other standard LP solving algorithms)? – Auberon Jun 4 '16 at 16:16