Evaluation of SSAT by reduction to decision diagrams

Thumbnail Image

Files

master_Ojala_Oskari_2022.pdf (572.96 KB)

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

2022-10-17

Department

Major/Subject

Computer Science

Mcode

SCI3042

Degree programme

Master’s Programme in Computer, Communication and Information Sciences

Language

en

Pages

63

Series

Abstract

Stochastic satisfiability (SSAT) is a relatively new concept of solving search and reasoning problems in the form of quantified Boolean formulas, including a possible amount of randomness and stochasticity. SSAT is a complete problem belonging to the computational complexity class PSPACE. It is a generalization of the NP-complete SAT problem, a fundamental concept in computer science and artificial intelligence. Binary decision diagrams and their generalizations sentential decision diagrams are canonical representations of propositional knowledge bases, also referred to as Boolean formulas. It is known that the evaluation of any type of satisfiability problem either implicitly or explicitly constructs a binary decision tree-like execution path. Although subproblems of SSAT and decision diagram representations of Boolean logic are widely studied, decision diagrams have not yet been explicitly applied to SSAT solving. The aim of this thesis is to study the potential of this explicit construction and minimization of decision diagrams and propose new algorithms for SSAT solving. We have proven the correctness and rules for universal and complete SSAT evaluation algorithms for BDD and SDD and implemented corresponding minimization procedures for both data structures. Our results show that an SDD-based implementation is generally more efficient than a BDD-based one, but both are generally less efficient than the best known SSAT solvers erSSAT and ClauSSat that utilize modern pruning and learning techniques. Yet, in some test cases, our algorithms were more efficient and reliable than erSSAT and ClauSSat. Most of the computational resources were spent on the construction and minimization of the data structures. Improving the efficiency of construction and minimization procedures is a key for further computational optimization.

Stokastinen toteutuvuus (SSAT) on suhteellisen uusi tapa ratkaista kvantifioiduiksi Boolen loogisiksi lausekkeiksi muotoiltuja haku- ja päättelyongelmia, jotka voivat sisältää myös satunnaisuutta ja stokastisuutta. SSAT kuuluu laskennalliselta kompleksisuudeltaan luokkaan PSPACE, ja on PSPACE-täydellinen, eli sillä voidaan esittää kaikki kyseisen kompleksisuusluokan ongelmat. SSAT on yleistys NP-täydellisestä SAT-toteutuvuusongelmasta, joka kuuluu tietotekniikan ja tekoälytutkimuksen keskeisiin perusteisiin. Binääriset päätösdiagrammit (BDD) ja niiden yleistykset lausekkeelliset päätösdiagrammit (SDD), ovat loogisten lausekkeiden luonnollisia kuvauksia. Tiedetään, että minkä tahansa toteutuvuusongelman ratkaiseminen rakentaa suorituspolun, joka joko implisiittisesti tai eksplisiittisesti vastaa binääristä päätöspuuta. Vaikka stokastisen toteutuvuuden osaongelmia ja loogisten lausekkeiden päätösdiagrammiesityksiä on tutkittu paljon, loogisia lausekkeita päätösdiagrammimuodossa ei ole vielä suoraan sovellettu SSAT-ongelmien ratkaisemiseen. Tämän diplomityön tavoitteena on tutkia päätösdiagrammien rakentamista ja minimointia SSAT-ongelmien ratkaisemisessa. Olemme todistaneet yleisten ja täydellisten SSAT-laskenta-algoritmien oikeellisuuden ja määritelleet säännöt SSAT-ongelman ratkaisuun binäärisillä sekä lausekkeellisilla päätösdiagrammeilla, sekä toteuttaneet molemmille tietorakenteille SSAT:iin liittyvät minimointiproseduurit. Tutkimuksen tulokset kertovat, että lausekkeellisella päätösdiagrammilla toteutettu algoritmi on yleisesti tehokkaampi kuin binäärisellä päätösdiagrammilla toteutettu, mutta molemmat pääosin häviävät tehokkuudessa tämän hetken parhaille SSAT-algoritmeille erSSAT:lle ja ClauSSat:lle, joissa on hyödynnetty karsimis- ja oppimistekniikoita. Kuitenkin osassa testitapauksista uudet algoritmit olivat tehokkaampia ja luotettavampia kuin erSSAT ja ClauSSat. Suurin osa laskennallisista resursseista kului tietorakenteiden rakentamiseen ja minimointiin, joten näiden proseduurien kehittäminen on tärkeää algoritmien jatkokehityksessä.

Description

Supervisor

Rintanen, Jussi

Thesis advisor

Rintanen, Jussi

Keywords

artificial intelligence, SSAT, binary decision diagram, sentential decision diagram, automated reasoning, quantified Boolean formulas

Other note

Citation

Permanent link to this item

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

Collections

[dipl] Perustieteiden korkeakoulu / SCI