Resumen de A new framework for max-sat solving

Federico Heras Viaga

• The propositional satisfiability problem (SAT) is the problem of determining whether a truth assignment exists that satisfies a CNF formula, The SAT problem is a well known NP-Complete problem that appears in many contexts. Algorithms for SAT solving include, among others, local search, systematic search and formula manipulation based on the resolution rule.

  The optimization version of the SAT problem is known as the Weighted Maximum Satisfiability Problem but we will refer to it as simply Maximum Satisfiability Problem (Max-SAT). Given a set of clauses with an associated weight, the Max-SAT problem consists in finding an assignment for the variables such that the sum of weights of the satisfied clauses is maximized. The Max-SAT problem is NP-Hard. SAT algorithms based on local search can be applied directly to Max-SAT, while algorithms based on systematic search and formula manipulation have to be adapted to Max-SAT.

  In this dissertation we contribute to better understanding the relationship between SAT and Max-SAT. As a result, we find nice connections between both problems that allow us to propose a new framework for efficient Max-SAT solving. First, we extend a classical algorithm based on systematic search from SAT to Max-SAT and we extend the resolution rule from SAT to Max-SAT. Then, we show how the new resolution rule can be applied during the search process to simplify the formula and as a consequence boost the search process. Finally, we present an algorithm that integrates all these techniques and other improvements coming from the SAT and Max-SAT literature.