AAS 390 Chapter Notes - Chapter 1: Boolean Satisfiability Problem, Lio, Rela

• School: A&M Texarkana, TAMUT
• Department: Applied Arts & Sciences
• Course: AAS 390

Document Summary

Lin xu, frank hutter, holger h. hoos and kevin leyton-brown. Empirical studies often observe that the performance of algorithms across problem domains can be quite uncorre- lated. When this occurs, it seems practical to investigate the use of algorithm portfolios that draw on the strengths of multiple algorithms. Satzilla is such an algorithm portfolio for sat problems; it was rst deployed in the. 2004 sat competition [12], and recently an updated ver- sion, satzilla2007, won a number of prizes in the 2007. Sat competition [21], including the gold medals for the. Sat+unsat categories of both the random and hand- made categories. We attribute this mainly to the lack of publicly available high-performance component solvers as well as to overheads in computing instance features for huge industrial instances; we ad- dressed this latter point in satzilla2009. Satzilla is based on empirical hardness models [10, 13], learned predictors that estimate each algorithm"s performance on a given sat instance.