Study of efficient techniques for implementing a Pseudo-Boolean solver based on cutting planes

Abstract: Most modern SAT solvers are based on resolution and CNF representation. The performance of these has improved a great deal in the past decades. But still they have some drawbacks such as the slow efficiency in solving some compact formulas e.g. Pigeonhole Principle or the large number of clauses required for representing some SAT instances. Linear Pseudo-Boolean inequalities using cutting planes as resolution step is another popular configuration for SAT solvers. These solvers have a more compact representation of a SAT formula, which makes them also able to solve some instances such as the Pigeonhole Principle easily. However, they are outperformed by clausal solvers in most cases. This thesis does a research in the CDCL scheme and how can be applied to cutting planes based PB solvers in order to understand its performance. Then some aspects of PB solving that could be improved are reviewed and an implementation for one of them (division) is proposed. Finally, some experiments are run with this new implementation. Several instances are used as benchmarks encoding problems about graph theory (dominating set, even colouring and vertex cover). In conclusion the performance of division varies among the different problems. For dominating set the performance is worse than the original, for even colouring no clear conclusions are shown and for vertex cover, the implementation of division outperforms the original version.