Name
Abstract | ||
|---|---|---|
Many lower bound computation methods for branch and bound Max-SAT solvers can be explained as procedures that search for disjoint inconsistent subformulas in the Max-SAT instance under consideration. The difference among them is the technique used to detect inconsistencies. In this paper, we define five new lower bound computation methods: two of them are based on detecting inconsistencies via a unit propagation procedure that propagates unit clauses using an original ordering; the other three add an additional level of forward look-ahead based on detecting failed literals. Finally, we provide empirical evidence that the new lower bounds are of better quality than the existing lower bounds, as well as that a solver with our new lower bounds greatly outperforms some of the best performing state-of-the-art Max-SAT solvers on Max-2SAT, Max-3SAT, and Max-Cut instances. |
Year | Venue | Keywords |
|---|---|---|
2006 | AAAI | max-cut instance,new lower bound computation,propagates unit clause,max-sat instance,new lower bound,disjoint inconsistent subformulas,max-sat solvers,lower bound computation method,lower bound,unit propagation procedure,state-of-the-art max-sat solvers,look ahead,branch and bound,sat solver,empirical evidence |
Field | DocType | Citations |
Maximum satisfiability problem,Mathematical optimization,Branch and bound,Disjoint sets,Upper and lower bounds,Computer science,Algorithm,Solver,Unit propagation,Computation | Conference | 42 |
PageRank | References | Authors |
1.99 | 13 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chu Min Li | 1 | 1194 | 85.65 |
| Felip Manyà | 2 | 787 | 59.52 |
| Jordi Planes | 3 | 486 | 31.38 |