About Yasol

Yasol is a search based solver for so called 'Quantified mixed integer linear programs with minimax objective‘ (Q-MIP). The aim is to support optimization under uncertainty in a new way, based upon rigorous formal models of quantification and linear constraints.

Our mission is research. The reason why we open the sources of this solver is in order to intensify the discussion whether multi-stage optimization is possible and maybe even practical. 

While the solver is new in the sense that there are no other Q-MIP solver at this time (June 2021), most basic ingredients of Yasol are not new at all. The heart of the search algorithm is an arithmetic linear constraint database together with the Alphabeta-algorithm which has been successfully used in gaming programs like in chess programs since many years. In order to realize fast back-jumps as typically performed in SAT- and QBF- solvers, we have extended the Alphabeta-algorithm as roughly described in [1]. Yasol deals with constraint learning on the so called primal side as known from SAT- and QBF- solving, as well as with constraint learning on the so called dual side, as is known from Mathematical Programming. Yasol solves multistage quantified programs with the following properties:

  • all constraints are linear
  • quantifiers are either existential or universal
  • the objective is minmax (more exactly: min max min … max min max) and is linear for any single game
  • integer variables are allowed on all exist-stages and must be greater or equal to zero
  • only integer variables are allowed on universal stages
  • continuous variables are allowed only on the last stage, assuming it is an existential stage
  • all variables must be bounded from below and above, and the range between upper and lower bounds of integer variables must not exceed 40 bits

In a recent computational study we showed that solving robust discrete problems with multiple stages is well within the reach of our solver [2]. It makes intensive use of a linear program solver like clp or the lp-solver of cplex. These tools are black-box used, but it is our intention not to use the integer solving abilities of these foreign solvers.

For some historical notes on Quantified Programming, Linear Programming and personal credits, we refer to our history page

For details of how to use the solver and about details of input formats etc. we refer to our download page.

[1] Thorsten Ederer, Michael Hartisch, Ulf Lorenz, Thomas Opfer, Jan Wolf. Yasol: An Open Source Solver for Quantified Mixed Integer Programs. ACG 2017: 224-233

[2] Marc Goerigk, Michael Hartisch. Multistage Robust Discrete Optimization via Quantified Integer Programming. Submitted to COR