ParamILS

Academic Applications

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

Propositional satisfiability (SAT) & SAT-based formal verification

• Boosting verification by automatic tuning of decision procedures
  Frank Hutter, Domagoj Babić, Holger H. Hoos, and Alan J. Hu - Formal Methods in Computer Aided Design, 2007. FMCAD '07, pp. 27-34, November 2012.
  [The first major application of ParamILS for a configuration space too big for humans to search manually. ParamILS achieved an average 500-fold speedup of SPEAR for solving SAT-encoded software verification instances, and a 4.5-fold speedup for SAT-encoded hardware verification. Based on this optimization, SPEAR won the QF_BV category of the 2007 international SMT competition]
  [pdf] [bibtex]


• SATenstein: Automatically building local search SAT solvers from components
  Ashiqur R. KhudaBukhsh, Lin Xu, Holger H. Hoos, and Kevin Leyton-Brown - Proceedings of the 21st international jont conference on Artifical intelligence, pp. 517-524, July, 2009.
  [pdf] [bibtex]


• Captain Jack: New variable selection heuristics in local search for SAT
  Dave A.D. Tompkins, Adrian Balint, and Holger H. Hoos - Theory and Applications of Satisfiability Testing - SAT 2011, LNCS 6695, pp. 302-316, Springer, June, 2011.
  [pdf] [bibtex]


• Dynamic scoring functions with variable expressions: New SLS methods for solving SAT
  Dave A.D. Tompkins, and Holger H. Hoos - Theory and Applications of Satisfiability Test - SAT 2010, LNCS 6175, pp. 278-292, Springer, July, 2010.
  [pdf] [bibtex]


• clasp, claspfolio, aspeed: Three Solvers from the Answer Set Solving Collection Potassco
  Martin Gebser, Benjamin Kaufmann, and Torsen Schaub - Proceedings of SAT Challenge 2012; Solver and, pp. 17, 2012.
  [pdf] [bibtex]

Satisfiability Modulo Theories (SMT)

• Automated Parameter Configuration for an SMT Solver
  Duy Tin Truong - Degree thesis DISI-10-057, University of Trento, Department of Information Engineering and Computer Science, November 2010.
  [pdf] [bibtex]

Answer set programming (ASP)

• A Portfolio Solver for Answer Set Programming: Preliminary Report
  Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Torsin Schaub, Marius Thomas Schneider, and Stefan Ziller - Logic Programming and Nonmonotonic Reasoning, LNCS 6645, pp. 352-357, Springer, May, 2011.
  [pdf] [bibtex]


• Parsing combinatory categorial grammar via planning in answer set programming
  Yuliya Lierler, Peter Schüller - Correct Reasoning, LNCS 7265, pp. 436-453, Springer, 2012.
  [pdf] [bibtex]

AI planning

• FD-Autotune: Domain-specific configuration using fast downward
  Chris Fawcett, Malte Helmert, Holger H. Hoos, Erez Karpas, Gabriele Röger, Jendrik Seipp - PAL 2011 3rd Workshop on Planning and Learning, 2011.
  [pdf]


• Automatic generation of efficient domain-optimized planners from generic parametrized planners
  Mauro Vallati, Chris Fawcett, Alfonso E. Gerevini, Holger H. Hoos, and Alessandro Saetti - Proceedings of the Eighth RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion. (RCRA 2011), 2010.
  [pdf] [bibtex]


• Generating fast domain-specific planners by automatically configuring a generic parameterised planner
  Mauro Vallati, Chris Fawcett, Alfonso Gerevini, Holger H. Hoos, Alessandro Saetti - Workshop on Planning and Learning: ICAPS 2011, 13th June 2011.
  [An application of ParamILS to domain-specific planning, showing that the state-of-the-art solver LPG can be sped up in a fully automated fashion by up to a factor of 118 times. The resulting solver helped the PbP2 portfolio win the gold medal in the international planning competition 2011]
  [pdf] [bibtex]


• Learning to Choose Instance-Specific Macro Operators
  Maher Alhossaini - ICAPS 2010 Doctoral Consortium (DC), 2010
  [pdf] [bibtex]


• Macro Learning in Planning as Parameter Configuration
  Maher Alhossaini, and J. Christopher Beck - Advances in Artificial Intelligence, LNCS 7310, pp. 13-24, Springer, 2012.
  [Uses ParamILS to find the optimal subset of macros to use for a subset of instances, and then learns a mapping from instance features to the subset of macros to use.]
  [pdf] [bibtex]


• PbP2: Automatic Configuration of a Portfolio-based Multi-Planner
  Alfonso Gerevini, Alessandro Saetti, and Mauro Vallati - 7th International Planning Competition, June 2011.
  [Presents an automated system for generating domain-specific multi-planners from domain-specific techniques, as an important step including parameter optimization using ParamILS. The resulting configured algorithm won the learning track of the international planning competition 2011]
  [pdf] [bibtex]

Mixed integer programming

• Automated configuration of mixed integer programming solvers
  Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown - Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, LNCS 6140, pp. 186-202, 2010.
  [An application of ParamILS to demonstrate that large speedups can be achieved automatically for state-of-the-art mixed integer programming solvers, without the algorithm developers in the loop. Specifically, without any domain-specific knowledge about MIP or MIP solvers, ParamILS achieved up to 50-fold speedups of CPLEX for benchmark distributions for while the built-in CPLEX tuning tool did not improve over the default. The paper also used ParamILS to optimize other solvers (Gurobi and lpsolve) and objective functions (in particular, the optimality gap that could be achieved in a fixed time)]
  [pdf] [bibtex]

Time tabling

• An automatically configured modular algorithm for post enrollment course timetabling
  Chris Fawcett, Holger H. Hoos, and Marco Chiarandini - Technical Report TR-2009-15, University of British Columbia, Department of Computer Science, 2009.
  [pdf]


• A modular multiphase heuristic solver for post enrollment course timetabling
  Marco Chiarandini, Chris Fawcett, and Holger H. Hoos - Proc. PATAT, 2008.
  [An early application of ParamILS to the time-tabling domain. Based on optimization with ParamILS, the solver described here won a bronze medal in the international time-tabling competition 2008. With later improvements and ongoing optimization with ParamILS, this solver is now the state-of-the-art for time-tabling. It has also been used to schedule the exams for UBC's 50.000 students since 2010, improving exam schedules substantially compared to previous manual solutions]
  [pdf] [bibtex]

Game Theory

• Dynamic Matching via Weighted Myopia with Application to Kidney Exchange
  John P. Dickerson, Ariel D. Procaccia, and Tuomas Sandholm - Proceedings of the 26th AAAI Conference on Artificial Intelligence, 2012.
  [An application of ParamILS to optimize the 20 vertex potentials of a dynamic matching algorithm with applications to kidney exchanges. ParamILS found substantially improved potentials, thereby allowing the algorithm to match more kidney exchange patients than the current practice of clearing myopically]
  [pdf] [bibtex]

Game Playing

• Automatically Configuring Algorithms for Scaling Performance
  James Styles, Holger H. Hoos, and Martin Müller - LION 2012, pages 205-219.
  [An application of ParamILS to optimize various algorithms for scaling performance. The application domains were Computer GO (configuring the MCTS solver Fuego), the travelling salesman problem, and mixed integer programming]
  [pdf] [bibtex]

Protein folding

• A replica exchange Monte Carlo algorithm for protein folding in the HP model
  Chris Thachuk, Alena Shmygelska, and Holger H. Hoos - BMC Bioinformatics 8.1, 2007.
  [An early application of ParamILS, showing consistent speedups over the default of a new state-of-the-art algorithm for protein folds. Even though this algorithm only had 4 parameters, ParamILS achieved up to a speedup factor of 3, making the difference between being a good solver and the new state of the art]
  [pdf] [bibtex]

Travelling Salesman Problem and Quadratic Assignment Problem

• Consultant-Guided Search: A New Metaheuristic for Combinatorial Optimization Problems
  Serban Iordache - Proceedings of the 12th annual conference on Genetic and evolutionary computation, pp. 225-232, 2010.
  [pdf] [bibtex]


• A hybrid heuristic approach for solving the generalized traveling salesman problem
  Petrică C. Pop, and Serban Iordache - Proceedings of the 13th annual conference on Genetic and evolutionary computation, pp. 481-488, 2011.
  [pdf] [bibtex]


• Consultant-guided search algorithms with local search for the traveling salesman problem
  Serban Iordache - Parallel Problem Solving from Nature, PPSN XI, LNCS 6239, pp. 81-90, 2010.
  [pdf] [bibtex]


• Consultant-guided search algorithms for the quadratic assignment problem
  Serban Iordache - Hybrid Metaheuristics, LNCS 6373, pp. 148-159, 2010.
  [pdf] [bibtex]


• Emergent Phenomena in Agent-Based Systems
  Serban Iordache - PhD Dissertation, UNIVERSITATEA „POLITEHNICA“ din BUCUREȘTI, Facultatea de Automatică şi Calculatoare, 2011.
  [Applications of ParamILS to configure a new metaheuristic algorithm (Consultant-guided search, CGS) with over a dozen parameters, to achieve state-of-the-art performance for TSP solving and the quadratic assignment problem]
  [pdf]

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 2012	(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
Clasp
Lingeling
PicoSAT
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]