Study of efficient techniques for implementing a Pseudo-Boolean solver based on cutting planes
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/109283
Realitzat a/ambKungliga Tekniska högskolan
Tipus de documentTreball Final de Grau
Data2017-06
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
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.
MatèriesElectronic circuits, Constrained optimization, Circuits electrònics, Optimització amb restriccions
TitulacióGRAU EN ENGINYERIA INFORMÀTICA (Pla 2010)
Localització
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
126452.pdf | 961,0Kb | Visualitza/Obre |