-
An Exponential Lower Bound for Zadeh's pivot rule
Authors:
Yann Disser,
Oliver Friedmann,
Alexander V. Hopp
Abstract:
The question whether the Simplex Algorithm admits an efficient pivot rule remains one of the most important open questions in discrete optimization. While many natural, deterministic pivot rules are known to yield exponential running times, the random-facet rule was shown to have a subexponential running time. For a long time, Zadeh's rule remained the most prominent candidate for the first determ…
▽ More
The question whether the Simplex Algorithm admits an efficient pivot rule remains one of the most important open questions in discrete optimization. While many natural, deterministic pivot rules are known to yield exponential running times, the random-facet rule was shown to have a subexponential running time. For a long time, Zadeh's rule remained the most prominent candidate for the first deterministic pivot rule with subexponential running time. We present a lower bound construction that shows that Zadeh's rule is in fact exponential in the worst case. Our construction is based on a close relation to the Strategy Improvement Algorithm for Parity Games and the Policy Iteration Algorithm for Markov Decision Processes, and we also obtain exponential lower bounds for Zadeh's rule in these contexts.
△ Less
Submitted 30 October, 2020; v1 submitted 4 November, 2019;
originally announced November 2019.
-
Errata for: A subexponential lower bound for the Random Facet algorithm for Parity Games
Authors:
Oliver Friedmann,
Thomas Dueholm Hansen,
Uri Zwick
Abstract:
In Friedmann, Hansen, and Zwick (2011) we claimed that the expected number of pivoting steps performed by the Random-Facet algorithm of Kalai and of Matousek, Sharir, and Welzl is equal to the expected number of pivoting steps performed by Random-Facet^*, a variant of Random-Facet that bases its random decisions on one random permutation. We then obtained a lower bound on the expected number of pi…
▽ More
In Friedmann, Hansen, and Zwick (2011) we claimed that the expected number of pivoting steps performed by the Random-Facet algorithm of Kalai and of Matousek, Sharir, and Welzl is equal to the expected number of pivoting steps performed by Random-Facet^*, a variant of Random-Facet that bases its random decisions on one random permutation. We then obtained a lower bound on the expected number of pivoting steps performed by Random-Facet^* and claimed that the same lower bound holds also for Random-Facet. Unfortunately, the claim that the expected numbers of steps performed by Random-Facet and Random-Facet^* are the same is false. We provide here simple examples that show that the expected numbers of steps performed by the two algorithms are not the same.
△ Less
Submitted 29 October, 2014;
originally announced October 2014.
-
Random-Facet and Random-Bland require subexponential time even for shortest paths
Authors:
Oliver Friedmann,
Thomas Dueholm Hansen,
Uri Zwick
Abstract:
The Random-Facet algorithm of Kalai and of Matousek, Sharir and Welzl is an elegant randomized algorithm for solving linear programs and more general LP-type problems. Its expected subexponential time of $2^{\tilde{O}(\sqrt{m})}$, where $m$ is the number of inequalities, makes it the fastest known combinatorial algorithm for solving linear programs. We previously showed that Random-Facet performs…
▽ More
The Random-Facet algorithm of Kalai and of Matousek, Sharir and Welzl is an elegant randomized algorithm for solving linear programs and more general LP-type problems. Its expected subexponential time of $2^{\tilde{O}(\sqrt{m})}$, where $m$ is the number of inequalities, makes it the fastest known combinatorial algorithm for solving linear programs. We previously showed that Random-Facet performs an expected number of $2^{\tildeΩ(\sqrt[3]{m})}$ pivoting steps on some LPs with $m$ inequalities that correspond to $m$-action Markov Decision Processes (MDPs). We also showed that Random-Facet-1P, a one permutation variant of Random-Facet, performs an expected number of $2^{\tilde{O}(\sqrt{m})}$ pivoting steps on these examples. Here we show that the same results can be obtained using LPs that correspond to instances of the classical shortest paths problem. This shows that the stochasticity of the MDPs, which is essential for obtaining lower bounds for Random-Edge, is not needed in order to obtain lower bounds for Random-Facet. We also show that our new $2^{\tildeΩ(\sqrt{m})}$ lower bound applies to Random-Bland, a randomized variant of the classical anti-cycling rule suggested by Bland.
△ Less
Submitted 28 October, 2014;
originally announced October 2014.
-
Satisfiability Games for Branching-Time Logics
Authors:
Oliver Friedmann,
Martin Lange,
Markus Latte
Abstract:
The satisfiability problem for branching-time temporal logics like CTL*, CTL and CTL+ has important applications in program specification and verification. Their computational complexities are known: CTL* and CTL+ are complete for doubly exponential time, CTL is complete for single exponential time. Some decision procedures for these logics are known; they use tree automata, tableaux or axiom sys…
▽ More
The satisfiability problem for branching-time temporal logics like CTL*, CTL and CTL+ has important applications in program specification and verification. Their computational complexities are known: CTL* and CTL+ are complete for doubly exponential time, CTL is complete for single exponential time. Some decision procedures for these logics are known; they use tree automata, tableaux or axiom systems. In this paper we present a uniform game-theoretic framework for the satisfiability problem of these branching-time temporal logics. We define satisfiability games for the full branching-time temporal logic CTL* using a high-level definition of winning condition that captures the essence of well-foundedness of least fixpoint unfoldings. These winning conditions form formal languages of ω-words. We analyse which kinds of deterministic ω-automata are needed in which case in order to recognise these languages. We then obtain a reduction to the problem of solving parity or Büchi games. The worst-case complexity of the obtained algorithms matches the known lower bounds for these logics. This approach provides a uniform, yet complexity-theoretically optimal treatment of satisfiability for branching-time temporal logics. It separates the use of temporal logic machinery from the use of automata thus preserving a syntactical relationship between the input formula and the object that represents satisfiability, i.e. a winning strategy in a parity or Büchi game. The games presented here work on a Fischer-Ladner closure of the input formula only. Last but not least, the games presented here come with an attempt at providing tool support for the satisfiability problem of complex branching-time logics like CTL* and CTL+.
△ Less
Submitted 15 October, 2013; v1 submitted 23 August, 2013;
originally announced August 2013.
-
An exponential lower bound for Cunningham's rule
Authors:
David Avis,
Oliver Friedmann
Abstract:
In this paper we give an exponential lower bound for Cunningham's least recently considered (round-robin) rule as applied to parity games, Markhov decision processes and linear programs. This improves a recent subexponential bound of Friedmann for this rule on these problems. The round-robin rule fixes a cyclical order of the variables and chooses the next pivot variable starting from the previous…
▽ More
In this paper we give an exponential lower bound for Cunningham's least recently considered (round-robin) rule as applied to parity games, Markhov decision processes and linear programs. This improves a recent subexponential bound of Friedmann for this rule on these problems. The round-robin rule fixes a cyclical order of the variables and chooses the next pivot variable starting from the previously chosen variable and proceeding in the given circular order. It is perhaps the simplest example from the class of history-based pivot rules. Our results are based on a new lower bound construction for parity games. Due to the nature of the construction we are also able to obtain an exponential lower bound for the round-robin rule applied to acyclic unique sink orientations of hypercubes (AUSOs). Furthermore these AUSOs are realizable as polytopes. We believe these are the first such results for history based rules for AUSOs, realizable or not. The paper is self-contained and requires no previous knowledge of parity games.
△ Less
Submitted 16 May, 2013;
originally announced May 2013.
-
On Guarded Transformation In The Modal Mu-Calculus
Authors:
Florian Bruse,
Oliver Friedmann,
Martin Lange
Abstract:
Guarded normal form requires occurrences of fixpoint variables in a μ-calculus-formula to occur under the scope of a modal operator. The literature contains guarded transformations that effectively bring a μ-calculus-formula into guarded normal form. We show that the known guarded transformations can cause an exponential blowup in formula size, contrary to existing claims of polynomial behaviour.…
▽ More
Guarded normal form requires occurrences of fixpoint variables in a μ-calculus-formula to occur under the scope of a modal operator. The literature contains guarded transformations that effectively bring a μ-calculus-formula into guarded normal form. We show that the known guarded transformations can cause an exponential blowup in formula size, contrary to existing claims of polynomial behaviour. We also show that any polynomial guarded transformation for μ-calculus-formulas in the more relaxed vectorial form gives rise to a polynomial solution algorithm for parity games, the existence of which is an open problem. We also investigate transformations between the μ-calculus, vectorial form and hierarchical equation systems, which are an alternative syntax for alternating parity tree automata.
△ Less
Submitted 20 December, 2013; v1 submitted 3 May, 2013;
originally announced May 2013.
-
An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms
Authors:
Oliver Friedmann
Abstract:
This paper presents a new exponential lower bound for the two most popular deterministic variants of the strategy improvement algorithms for solving parity, mean payoff, discounted payoff and simple stochastic games. The first variant improves every node in each step maximizing the current valuation locally, whereas the second variant computes the globally optimal improvement in each step. We out…
▽ More
This paper presents a new exponential lower bound for the two most popular deterministic variants of the strategy improvement algorithms for solving parity, mean payoff, discounted payoff and simple stochastic games. The first variant improves every node in each step maximizing the current valuation locally, whereas the second variant computes the globally optimal improvement in each step. We outline families of games on which both variants require exponentially many strategy iterations.
△ Less
Submitted 30 September, 2011; v1 submitted 3 June, 2011;
originally announced June 2011.
-
Local Strategy Improvement for Parity Game Solving
Authors:
Oliver Friedmann,
Martin Lange
Abstract:
The problem of solving a parity game is at the core of many problems in model checking, satisfiability checking and program synthesis. Some of the best algorithms for solving parity game are strategy improvement algorithms. These are global in nature since they require the entire parity game to be present at the beginning. This is a distinct disadvantage because in many applications one only needs…
▽ More
The problem of solving a parity game is at the core of many problems in model checking, satisfiability checking and program synthesis. Some of the best algorithms for solving parity game are strategy improvement algorithms. These are global in nature since they require the entire parity game to be present at the beginning. This is a distinct disadvantage because in many applications one only needs to know which winning region a particular node belongs to, and a witnessing winning strategy may cover only a fractional part of the entire game graph.
We present a local strategy improvement algorithm which explores the game graph on-the-fly whilst performing the improvement steps. We also compare it empirically with existing global strategy improvement algorithms and the currently only other local algorithm for solving parity games. It turns out that local strategy improvement can outperform these others by several orders of magnitude.
△ Less
Submitted 7 June, 2010;
originally announced June 2010.
-
A Super-Polynomial Lower Bound for the Parity Game Strategy Improvement Algorithm as We Know it
Authors:
Oliver Friedmann
Abstract:
This paper presents a new lower bound for the discrete strategy improvement algorithm for solving parity games due to Voege and Jurdziski. First, we informally show which structures are difficult to solve for the algorithm. Second, we outline a family of games of quadratic size on which the algorithm requires exponentially many strategy iterations, answering in the negative the long-standing que…
▽ More
This paper presents a new lower bound for the discrete strategy improvement algorithm for solving parity games due to Voege and Jurdziski. First, we informally show which structures are difficult to solve for the algorithm. Second, we outline a family of games of quadratic size on which the algorithm requires exponentially many strategy iterations, answering in the negative the long-standing question whether this algorithm runs in polynomial time. Additionally we note that the same family of games can be used to prove a similar result w.r.t. the strategy improvement variant by Schewe.
△ Less
Submitted 18 January, 2009;
originally announced January 2009.
