PV2 ⊧ SATzilladecides which solver to call per instance based on predictors

An automatic algorithm portfolio for SAT based on empirical hardness models

Application domain/field

• SAT solving
• Algorithm selection
• Solver selection

Type of tool

Solver selector for SAT problems

Expected input

SAT problem

Expected output

SATzilla runs the algorithm with the best predicated runtime until the instance is solved or the allotted time is used up.

Internals

• SAT solvers in SATzilla07: Eureka, Kcnfs06, March_dl04, MiniSat 2.0, Rsat 1.03, Vallst, Zchaff_Rand.
• Candidate SAT solvers in SATzilla09: March_dl04 (march_dl?), March_pl (march_eq?), MiniSat 2.0, Vallst, Zchaff_Rand, Kcnfs04, TTS 4.0, PicoSAT 8.46, MXC 08, MiniSat 2007, Rsat 2.0.
• Local search solvers in SATzilla09: gnovelty+, Ranov (both are variants of gNovelty), Ag2wsat0, Ag2wsat+ (both are variants of adaptG2WSAT), SATenstein.