Show simple item record

dc.contributor.authorSacrest Gascón, Aleix
dc.coverage.spatialeast=18.068580800000063; north=59.32932349999999; name=Norrmalm, Stockholm, Suècia
dc.description.abstractMost 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.
dc.publisherUniversitat Politècnica de Catalunya
dc.subjectÀrees temàtiques de la UPC::Informàtica
dc.subject.lcshElectronic circuits
dc.subject.lcshConstrained optimization
dc.subject.otherCutting Planes
dc.subject.otherConflict Driven Clause Learning
dc.titleStudy of efficient techniques for implementing a Pseudo-Boolean solver based on cutting planes
dc.typeBachelor thesis
dc.subject.lemacCircuits electrònics
dc.subject.lemacOptimització amb restriccions
dc.rights.accessOpen Access
dc.audience.degreeGRAU EN ENGINYERIA INFORMÀTICA (Pla 2010)
dc.contributor.covenanteeKungliga Tekniska högskolan

Files in this item


This item appears in the following Collection(s)

Show simple item record

All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder