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 effi-
ciency in solving some compact formulas e.g. Pigeonhole Principle [1]
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. |