Title :
Algorithms for Maximum Satisfiability using Unsatisfiable Cores
Author :
Marques-Silva, Joao ; Planes, Jordi
Author_Institution :
Electron. & Comput. Sci., Southampton Univ., Southampton
Abstract :
Many decision and optimization problems in electronic design automation (EDA) can be solved with Boolean satisfiability (SAT). Moreover, well-known extensions of SAT also find application in EDA, including pseudo-Boolean optimization, quantified Boolean formulas, multi-valued SAT and, more recently, Maximum Satisfiability (MaxSAT). Algorithms for MaxSAT are still fairly inefficient in industrial settings, in part because the most effective SAT techniques cannot be easily extended to MaxSAT. This paper proposes a novel algorithm for MaxSAT that improves existing state of the art solvers by orders of magnitude on industrial benchmarks. The new algorithm exploits modern SAT solvers, being based on the identification of unsatisfiable subformulas. Moreover, the new algorithm provides additional insights between unsatisfiable subformulas and the maximum satisfiability problem.
Keywords :
Boolean functions; circuit optimisation; electronic design automation; optimisation; Boolean satisfiability; MaxSAT; electronic design automation; maximum satisfiability algorithms; pseudo-Boolean optimization problems; Application software; Circuits; Computer science; Data structures; Debugging; Design optimization; Electronic design automation and methodology; Encoding; Industrial relations; Inference algorithms;
Conference_Titel :
Design, Automation and Test in Europe, 2008. DATE '08
Conference_Location :
Munich
Print_ISBN :
978-3-9810801-3-1
Electronic_ISBN :
978-3-9810801-4-8
DOI :
10.1109/DATE.2008.4484715