Invited Session Thu.1.H 3003A

Thursday, 10:30 - 12:00 h, Room: H 3003A

Cluster 5: Constraint programming [...]

Instance-specific tuning, selection, and scheduling of solvers


Chair: Meinolf Sellmann



Thursday, 10:30 - 10:55 h, Room: H 3003A, Talk 1

Meinolf Sellmann
Solver portfolios

Coauthors: Yuri Malitsky, Ashish Sabrahwal, Horst Samulowitz, Meinolf Sellmann


We discuss the idea of selecting and scheduling solvers based on the features of a given input instance. In particular, we review the recently propose SAT Solver Selector (3S) and its parallel counterpart, p3S.



Thursday, 11:00 - 11:25 h, Room: H 3003A, Talk 2

Yuri Malitsky
Instance-specific algorithm configuration

Coauthor: Meinolf Sellmann


The presentation focuses on a method for instance-specific algorithm configuration (ISAC). ISAC is a general configurator that focuses on tuning different categories of parameterized solvers according to the instances they will be applied to. Specifically, this presentation will show that the instances of many problems can be decomposed into a representative vector of features. It will further show that instances with similar features often cause similar behavior in the applied algorithm. ISAC exploits this observation by automatically detecting the different sub-types of a problem and then training a solver for each variety. This technique is explored on a number of problem domains, including set covering, mixed integer, satisfiability, and set partitioning. ISAC is then further expanded to demonstrate its application to traditional algorithm portfolios and adaptive search methodologies. In all cases, marked improvements are shown over the existing state-of-the-art solvers.



Thursday, 11:30 - 11:55 h, Room: H 3003A, Talk 3

Lin Xu
Evaluating component solver contributions to portfolio-based algorithm selectors

Coauthors: Holger Hoos, Frank Hutter, Kevin Leyton-Brown


Portfolio-based algorithm selection can exploit complementary strengths of different solver and often represent the state of the art for solving many computationally challenging problems. In this work, we argue that a state-of-the-art method for constructing such algorithm selectors for the propositional satisfiability problem (SAT), SATzilla, also gives rise to an automated method for quantifying the importance of each of a set of available solvers. We entered the latest version of SATzilla into the analysis track of the 2011 SAT competition and draw two main conclusions from the results that we obtained. First, automatically-constructed portfolios of sequential, non-portfolio competition entries perform substantially better than the winners of all three sequential categories. Second, and more importantly, a detailed analysis of these portfolios yields valuable insights into the nature of successful solver designs in the different categories. For example, we show that the solvers contributing most to SATzilla were often not the overall best-performing solvers, but instead solvers that exploit novel solution strategies to solve instances that would remain unsolved without them.


  Do you need Missouri Payday Loans as soon as possible? Cialis Professional online is capableto release you reliably from the erection problems, its improved formula gives the new properties to the drug.