Home  |  Papers  |  Software  |  Licensing  |  Academic Applications  |  Competitions  |  Industrial Applications  |  Speedups Achieved 

Academic Applications

ParamILS is actively being used to improve solvers in a wide variety of academic problems.

Propositional satisfiability (SAT) & SAT-based formal verification

Satisfiability Modulo Theories (SMT)

Answer set programming (ASP)

AI planning

Mixed integer programming

Time tabling

Game Theory

Game Playing

Protein folding

Travelling Salesman Problem and Quadratic Assignment Problem


ParamILS has helped several groups build competition-winning solvers.

Competition Year Result Comment Research group(s)
Configurable SAT Solver competition (CSSC) 2013 ParamILS enabled
this competition
This competition rewarded SAT algorithms that performed well after automatic configuration, and ParamILS was an integral part of the competition. See the competition website for details. Freiburg, Vancouver, Ulm
Planning competition,
learning track
2011 first PbP2 is a portfolio solver prominently relying on LPG, configured with ParamILS Profs. Gerevini & Saetti
Brescia University, Italy
Planning competition,
learning track
2011 second FD-Autotune-speed is a version of FastDownward configured with ParamILS Prof. Helmert
University of Basel, Switzerland
ASP competition 2011
(winner) Clasp has so far been configured manually for competitions (exploiting years of domain knowledge), but optimization of subcomponents by ParamILS reguarly informs the algorithm development Prof. Schaub
Potsdam University, Germany
SAT Competition,
random satisfiable track
2011 gold Sparrow2011 assesses the maximal clause length of an instance and, based on that, selects between parameter settings which were determined offline based on configuration with ParamILS for 3-SAT, 5-SAT, and 7-SAT. Prof. Hoos, UBC, Vancouver, Canada
Prof. Schoening, Ulm, Germany
SAT Competition 2009 (3 gold, 2 silver) SATZilla is a portfolio solver using various instantiations of solvers configured with ParamILS Profs. Hoos &  Leyton-Brown
UBC, Vancouver, Canada
SAT Challenge 2012 (3 first, 1 second)
Time-tabling competition 2007 third UBCTT was specifically configured for the competition with ParamILS Prof. Hoos
UBC, Vancouver, Canada
Prof. Chiarandini
University of Southern Denmark
SMT Competition,
category QF_BV
2007 winner Spear was specifically configured for the competition with ParamILS Prof.  Hu
UBC, Vancouver, Canada

Industrial Applications

ParamILS is actively being used to improve industrial solvers for a wide variety of problems.
Mixed integer programming IBM ILOG
Scheduling and Resource Allocation Actenum
UBC Exam timetabling since 2010 UBC
Software Verification Programming Research Ltd.

Speedups Achieved

Although ParamILS can in principle optimize arbitrary user-defined objective functions, so far, it has achieved its greatest successes in minimizing the runtime algorithms require to solve a given problem. For doing so effectively, ParamILS relies on the idea of ``adaptive capping'', introduced in the ParamILS JAIR article.

Problem Domain Algorithm(s) Speedups over default Citation
Propositional Satisfiability SPEAR 4.5-500 [Hutter at al., FMCAD '07]
SAPS 8.1-130 [Hutter et al., AAAI '07]
SATENSTEIN 1.6-2.8 [KhudaBukhsh et al, IJCAI '09]
Captain Jack
Mixed Integer Programming CPLEX 2.0-52 [Hutter et al., CPAIOR '10]
GUROBI 1.2-2.3 [Hutter et al., CPAIOR '10]
LPSOLVE 1.0 1.0-153 [Hutter et al., CPAIOR '10]
Timetabling UBCTT >28 [Fawcett et al., Tech Report '09]
AI Planning FASTDOWNWARD 1.0-23 [Fawcett et al., ICAPS-PAL '11]
LPG 3.0-118 [Vallati et al., ICAPS-PAL '11]
Most probable explanation GLS+ >360 [Hutter et al., AAAI '07]
Protein folding REMC 1.2-3.0 [Thachuk et al., BMC Bioinformatics '07]