On Inconsistent Clause-Subsets for Max-SAT Solving

Recent research has focused on using the power of look-ahead to speed up the resolution of the Max-SAT problem. Indeed, look-ahead techniques such as Unit Propagation (UP) allow to find conflicts and to quickly reach the upper bound in a Branch-and-Bound algorithm, reducing the search-space of the resolution. In previous works, the Max-SAT solvers maxsatz9 and maxsatz14 use unit propagation to compute, at each node of the branch and bound searchtree, disjoint inconsistent subsets of clauses in the current subformula to estimate the minimum number of clauses that cannot be satisfied by any assignment extended from the current node. The same subsets may still be present in the subtrees, that is why we present in this paper a new method to memorize them and then spare their recomputation time. Furthermore, we propose a heuristic so that the memorized subsets of clauses induce an ordering among unit clauses to detect more inconsistent subsets of clauses. We show that this new approach impr...

• Type: Conference
• Year: 2007
• Where: CP
• Authors: Sylvain Darras, Gilles Dequen, Laure Devendeville, Chu Min Li
• Keywords: Artificial Intelligence, CP 2007, Inconsistent Subsets, Max-SAT Solvers, Unit Propagation