Name
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1145/1403375.1403474 | Proceedings of the conference on Design, automation and test in Europe |
Keywords | Field | DocType |
industrial relations,satisfiability,electronic design automation,sat solver,optimization problem,boolean functions,active power,application software,debugging,maxsat,data structures,design optimization,circuits,encoding,boolean satisfiability,computer science | Boolean function,Maximum satisfiability problem,Computer science,Satisfiability,Boolean satisfiability problem,Algorithm,AC power,Theoretical computer science,Electronic design automation,Optimization problem | Conference |
ISSN | Citations | PageRank |
1530-1591 | 65 | 2.43 |
References | Authors | |
32 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Joao Marques-Silva | 1 | 1947 | 124.04 |
| Jordi Planes | 2 | 486 | 31.38 |