Learning Centre

Approaches to grid-based SAT solving

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Hyvärinen, Antti E. J.
dc.date.accessioned 2011-11-28T13:23:11Z
dc.date.available 2011-11-28T13:23:11Z
dc.date.issued 2009
dc.identifier.isbn 978-951-22-9943-0
dc.identifier.issn 1797-5042
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/896
dc.description.abstract In this work we develop techniques for using distributed computing resources to efficiently solve instances of the propositional satisfiability problem (SAT). The computing resources considered in this work are assumed to be geographically distributed and connected by a non-dedicated network. Such systems are typically referred to as computational grid environments. The time a modern SAT solver consumes while solving an instance varies according to a random distribution. Unlike many other methods for distributed SAT solving, this work identifies the random distribution as a valuable resource for solving-time reduction. The methods which use randomness in the run times of a search algorithm, such as the ones discussed in this work, are examples of multi-search. The main contribution of this work is in developing and analyzing the multi-search approach in SAT solving and showing its efficiency with several experiments. For the purpose of the analysis, the work introduces a grid simulation model which captures several of the properties of a grid environment which are not observed in more traditional parallel computing systems. The work develops two algorithmic frameworks for multi-search in SAT. The first, SDSAT, is based on using properties of the distribution of the solving time so that the expected time required to solve an instance is reduced. Based on the analysis of SDSAT, the work proposes an algorithm for efficiently using large number of computing resources simultaneously to solve collections of SAT instances. The analysis of SDSAT also motivates the second algorithmic framework, CL-SDSAT. The framework is used to efficiently solve many industrial SAT instances by carefully combining information learned in the distributed SAT solvers. All methods described in the work are directly applicable in a wide range of grid environments and can be used together with virtually unmodified state-of-the-art SAT solvers. The methods are experimentally verified using standard benchmark SAT instances in a production-level grid environment. The experiments show that using the relatively simple methods developed in the work, SAT instances which cannot be solved efficiently in sequential settings can be now solved in a grid environment. en
dc.format.extent 85
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher Helsinki University of Technology en
dc.publisher Teknillinen korkeakoulu fi
dc.relation.ispartofseries TKK reports in information and computer science en
dc.relation.ispartofseries 16 en
dc.subject.other Computer science en
dc.title Approaches to grid-based SAT solving en
dc.type D4 Julkaistu kehittämis- tai tutkimusraportti taikka -selvitys fi
dc.contributor.school Faculty of Information and Natural Sciences en
dc.contributor.school Informaatio- ja luonnontieteiden tiedekunta fi
dc.contributor.department Department of Information and Computer Science en
dc.contributor.department Tietojenkäsittelytieteen laitos fi
dc.subject.keyword propositional satisfiability en
dc.subject.keyword SAT solving en
dc.subject.keyword computational grids en
dc.subject.keyword distributed search en
dc.subject.keyword multi-search en
dc.identifier.urn urn:nbn:fi:tkk-013015
dc.type.dcmitype text en

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive

Advanced Search

article-iconSubmit a publication