Name
Abstract | ||
|---|---|---|
Maximum Satisfiability (M AXSAT) is a well-known optimization pro- blem, with several practical applications. The most widely known MAXSAT algo- rithms are ineffective at solving hard problems instances f rom practical applica- tion domains. Recent work proposed using efficient Boolean S atisfiability (SAT) solvers for solving the MAXSAT problem, based on identifying and eliminating unsatisfiable subformulas. However, these algorithms do no t scale in practice. This paper analyzes existing MAXSAT algorithms based on unsatisfiable subfor- mula identification. Moreover, the paper proposes a number o f key optimizations to these MAXSAT algorithms and a new alternative algorithm. The proposed opti- mizations and the new algorithm provide significant perform ance improvements on MAXSAT instances from practical applications. Moreover, the effic iency of the new generation of unsatisfiability-based M AXSAT solvers becomes effec- tively indexed to the ability of modern SAT solvers to proving unsatisfiability and identifying unsatisfiable subformulas. |
Year | Venue | Keywords |
|---|---|---|
2007 | Clinical Orthopaedics and Related Research | satisfiability,sat solver,indexation,data structure,artificial intelligent |
Field | DocType | Volume |
Maximum satisfiability problem,Computer science,Boolean satisfiability problem,Satisfiability,Algorithm | Journal | abs/0712.1 |
Citations | PageRank | References |
25 | 1.20 | 24 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Joao Marques-Silva | 1 | 1947 | 124.04 |
| Jordi Planes | 2 | 486 | 31.38 |