Yasol software

(Ulf Lorenz, Jan. 2017)

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.
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 [7]. 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. The most inspiring sources from our point of view are: 

[1] T. Achterberg: Constraint Integer Programming. Doctoral Thesis
[2] T. Achterberg, T. Koch, A. Martin: Branching on History Information. ZIB-Report 02-32, Berlin, 2002
[3] H. Crowder, E.L. Johnson, M. Padberg: Solving Large-Scale Zero-One Linear Programming Problems. Operations Research, 31:5, pp. 803-834, 1983
[4] G. Gamrath, T. Koch, A. Martin, M. Miltenberger, D. Weninger: Progress in Presolving for Mixed Integer Programming. ZIB-Report 13-48, Berlin, 2013
[5] N. Sörensson, N. Een: MiniSat v1.13 – A SAT Solver with Conflict-Clause Minimization. minisat.se/downloads/MiniSat_v1.13_short.pdf
[6] F. Lonsing, A. Biere. DepQBF: A Dependency-Aware QBF Solver. JSAT 7(2-3), 71–76 (2010)
[7] T. Ederer, M. Hartisch, U. Lorenz, T. Opfer, J. Wolf. Yasol: An Open Source Solver for Quantified Mixed Integer Programs. ACG 2017: 224-233
[8] J. Wolf: Quantified Linear Programming. Doctoral Thesis. 
[9] L. Zhang: Searching for truth: Techniques for Satisfiability of Boolean Formulas. Doctoral Thesis

Special thanks go to Alexander Martin for many fruitful discussions and bringing the field of integer programming to my interest.