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 - Jan. 2017, 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) binary 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

Currently, the solver has its main strengths on quantified integer optimization with one to two dozens of universal variables - which span thousands up to millions of scenarios. 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

527efb333