Por Maria Luisa Bonet (Universidad Politecnica de Catalunya).

Abstract: The problem of Satisfiability (SAT) is NP-complete, and therefore hard to solve. On the other and, it is very important to find the best algorithms to solve as many instances of SAT as possible, since many important real life problems can be encoded into SAT. Conflict-driven clause learning (CDCL) is at the core of the success of modern SAT solvers. In terms of propositional proof complexity, CDCL has been shown as strong as the propositional proof system of general resolution.

Improvements to SAT solvers can be realized either by improving existing algorithms, or by exploiting proof systems stronger than CDCL.It is open whether a proof system stronger than CDCL/RES could yield more efficient SAT solvers, as attempts at exploiting extended resolution or cutting planes in SAT solvers have been so far largely unsuccessful.

Furthermore, a key issue from a practical perspective is whether proof systems are automatizable. A proof system is automatizable, if there is an algorithm that finds proofs in that system, in time polynomial in the smallest proofs of the tautology. Unfortunately, most results regarding automatizability are negative (Bonet-Pitassi-Raz, Razborov).

Recent work (Ignatiev-Morgado-Marques-Silva) proposed an approach for solving SAT by an encoding to Horn MaxSAT. The proposed reduction coupled with MaxSAT resolution represents a new proof system, DRMaxSAT, which was shown to enable polynomial time refutations of pigeonhole formulas, in contrast with  either CDCL or general resolution.

The work of Bonet-Buss-Ignatiev-Marques-Silva-Morgado) investigates the DRMaxSAT proof system, and shows that DRMaxSAT p-simulates general resolution, that AC_0-Frege+PHP p-simulates DRMaxSAT, and that DRMaxSAT can not p-simulate neither AC^0-Frege+PHP nor the cutting planes proof system.

Short Bio: Maria Luisa Bonet obtained a Ph.D. in Mathematics at the University of California, Berkeley, under the joint direction of Leo Harrington and Sam Buss. She held the Warshowsky assistant professorship at University of California, San Diego, and a two year postdoc at the University of Pennsylvania. Currently she is a full professor in Computer Science, at the Universidad Politecnica de Catalunya.