Dense Implicant Cubes in Boolean Satisfiability Problems

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.