Jan Elffers: Towards faster pseudo-Boolean SAT solving

PRACTICALITIES

Lunch is served at 12:00 noon (register at tinyurl.com/TCS181105  at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for 1½-2 hours of more technical discussions.

ABSTRACT

The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean satisfiability---so-called SAT solvers---and today conflict-driven clause learning (CDCL) solvers are routinely used in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak.

Pseudo-Boolean SAT solvers are a type of SAT solvers that deal with this weakness. These solvers work with linear inequalities instead of clauses. While there is potential for stronger reasoning than with CDCL solvers, past pseudo-Boolean SAT solvers that do stronger reasoning are often prohibitively slow, so that pseudo-Boolean solvers translating to clauses are often more competitive. We make progress on this issue by proposing a new pseudo-Boolean SAT solver, RoundingSat, which is able to do such stronger reasoning at a higher speed than earlier solvers. The solver follows the framework of [Chai and Kuehlmann '05], but differs in the conflict analysis, where it uses the division rule instead of the saturation rule that was used before.

In this talk, I will explain CDCL solvers, the extension of CDCL to pseudo-Boolean solving of [Chai and Kuehlmann '05], and the new conflict analysis used in RoundingSat.

This seminar is the 50%-level seminar for Jan Elffers.