Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Study of efficient techniques for implementing a Pseudo-Boolean solver based on cutting planes
KTH, School of Computer Science and Communication (CSC).
2017 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesisAlternative title
Undersökning av effektiva tekniker för implementering av en pseudo- boolsk lösare med hjälp av skärande plan (Swedish)
Abstract [en]

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.

Place, publisher, year, edition, pages
2017.
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-209644OAI: oai:DiVA.org:kth-209644DiVA, id: diva2:1113207
Supervisors
Examiners
Available from: 2017-06-21 Created: 2017-06-21 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

fulltext(961 kB)30 downloads
File information
File name FULLTEXT01.pdfFile size 961 kBChecksum SHA-512
e237c3b4cd911de9c6aa47d11a9b1b9736eac40045192ea4d27082a27b835e974351957aaab09ac06d7b0e237c89413fa708c0d8c6be9cbae023bf20ee27a159
Type fulltextMimetype application/pdf

By organisation
School of Computer Science and Communication (CSC)
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 30 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 51 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf