Dense Implicant Cubes in Boolean Satisfiability Problems

Thumbnail Image

Files

master_Lipping_Joonas_2020.pdf (1.28 MB)

URL

Journal Title

Journal ISSN

Volume Title

Perustieteiden korkeakoulu | Master's thesis
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.

Authors

Date

2020-01-20

Department

Major/Subject

Computer Science

Mcode

SCI3042

Degree programme

Master’s Programme in Computer, Communication and Information Sciences

Language

en

Pages

66

Series

Abstract

The Boolean satisfiability problem (SAT) is to determine whether a formula of propositional logic evaluates to true under some assignment of truth values to its variables. It provides a natural formalism for a wide range of computational tasks, such as planning and verification tasks. SAT is NP-complete in the general case, meaning that no known solver can efficiently solve arbitrary SAT instances. However, the instances that emerge from real-world applications often have plentiful internal structure, which modern solvers can exploit using various inference techniques, making them tractable in practice. The effectiveness of such techniques has a pivotal impact on solving performance. This thesis presents a density measure for scoring certain conjunctions of literals based on the number of implied assignments they yield under unit propagation, and a solving technique that uses this score as a heuristic for the expected refutation work. An algorithm than incorporates the technique into a CDCL-type solver is described and implemented as an extension to the MiniSat 2.1 solver. The modified solver is evaluated by comparing its running times on a set of benchmark instances to those of the original solver, using both the original-form benchmarks and their permutations. The modified solver is slower on average, solving 35% of original-form and 29% of permuted-form instances faster than the baseline. The evidence, therefore, does not support using this algorithm in general. However, the modified solver appears to have the advantage on the satisfiable instances of particular benchmark families (in their non-permuted form), indicating that the algorithm may be of some use for specific kinds of instances.

Boolen toteutuvuusongelmana (SAT) on selvittää, voidaank1o propositiologiikan lauseen muuttujien totuusarvot valita siten, että lause on tosi. SAT on luonnollinen tapa ilmaista monia laskennallisia tehtäviä, muun muassa suunnittelu- ja verifiointitehtäviä. Ongelma on yleisessä muodossaan NP-täydellinen, eikä sellaista ratkaisumenetelmää tunneta, joka kykenisi ratkaisemaan mielivaltaisia SAT-instansseja tehokkaasti. Monissa käytännön sovelluksissa vastaan tulevissa instansseissa on kuitenkin runsaasti sisäistä rakennetta, jota nykyratkaisimet kykenevät hyödyntämään erinäisin tekniikoin. Tällä tavoin instanssit ovat käytännössä ratkaistavissa. Tunnettujen tekniikkojen toimivuudella on määräävä merkitys ratkaisinten suorituskyvyssä. Tässä työssä esitellään tiheysmitta, jolla pisteytetään literaalien konjunktioita sen perusteella, kuinka monta muuttujan totuusarvoa niistä seuraa yksikköpropagaatiota käyttämällä, sekä ratkaisutekniikka, joka käyttää tätä pisteytystä heuristiikkana odotetulle refutaatiotyölle. Kehitetään algoritmi, joka sisällyttää tekniikan CDCL tyyppiseen ratkaisimeen, ja toteutetaan se MiniSat 2.1-ratkaisimen laajennuksena. Muutettua ratkaisinta arvioidaan vertaamalla sen ratkaisuaikoja alkuperäisen ratkaisimen aikoihin, kun ratkaistavana on joukko teollisia vertailuinstansseja sekä niiden sekoitettuja muotoja. Muutettu ratkaisin on keskimäärin hitaampi: se ratkaisee verrokkia nopeammin 35% alkuperäisessä muodossa olevista ja 29% sekoitetuista instansseista. Tämän perusteella algoritmia ei siis voi suositella yleiseen käyttöön. Muutettu ratkaisin näyttää kuitenkin pärjäävän verrokkia paremmin joidenkin instanssiperheiden toteutuvilla instansseilla (ei-sekoitetussa muodossa), joten algoritmista saattaisi olla hyötyä joidenkin tiettyjen instanssityyppien ratkaisemisessa.

Description

Supervisor

Janhunen, Tomi

Thesis advisor

Janhunen, Tomi

Keywords

Boolean satisfiability, propositional logic, propositional satisfiability, SAT solver

Other note

Citation

Permanent link to this item

https://urn.fi/URN:NBN:fi:aalto-202001261816

Collections

[dipl] Perustieteiden korkeakoulu / SCI