Structure-based satisfiability checking : analyzing and harnessing the potential

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Järvisalo, Matti
dc.date.accessioned 2012-08-21T07:45:55Z
dc.date.available 2012-08-21T07:45:55Z
dc.date.issued 2008
dc.identifier.isbn 978-951-22-9642-2
dc.identifier.isbn 978-951-22-9641-5 (printed) #8195;
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/4551
dc.description.abstract Constraint satisfaction deals with developing automated techniques for solving computationally hard problems in a declarative fashion. The main emphasis of this thesis is on constraint satisfaction techniques for the propositional satisfiability problem (SAT). As solving techniques for propositional satisfiability have rapidly progressed during the last 15 years, implementations of decision procedures for SAT, so called SAT solvers, have been found to be extremely efficient as back-end search engines in solving large industrial-scale combinatorial problems. Since SAT solvers have become a standard tool for solving various real-world problem instances of increasing size and difficulty, there is a demand for more and more robust and efficient solvers. For understanding the success (and failures) of SAT solving in specific problem domains, it is important to investigate how different types of structural properties of SAT instances are related to the efficiency of solving the instances with different SAT-based constraint satisfaction techniques. This is the underlying motivation for this thesis. The emphasis of the thesis is on search-based SAT solving techniques for solving structured real-world problems. The work focuses on selected topics related to the analysis and development of both complete and stochastic local search methods for SAT. Both experimental and proof complexity theoretic approaches are applied. The main contributions are three-fold. The work contributes to the analysis of structure-based branching heuristics. A proof complexity theoretic power hierarchy is established for DPLL and clause learning SAT solvers with various structure-based branching restrictions. The proof complexity theoretic results are complemented by a detailed experimental evaluation of the effects of structure-based branching on state-of-the-art SAT solvers. In connection with structure-based branching in SAT, the work introduces the Extended ASP Tableaux proof system in the context of answer set programming, which is a field closely related to SAT solving. The work also contributes to the development of stochastic local search methods for structured real-world SAT instances. A novel non-clausal local search method for SAT is developed by incorporating the concept of justification frontiers previously applied in the context of complete non-clausal solvers. Variants of the method are analyzed with respect approximate completeness, and adaptive noise mechanisms aimed specifically for the method are developed. As a third point of view to structure in SAT, the work addresses the problem of generating hard satisfiable SAT instances for both DPLL-based and local search solvers by introducing the regular XORSAT model. Additionally, techniques for applying XORSAT instances specifically for benchmarking equivalence reasoning techniques in SAT solvers are developed. en
dc.format.extent Verkkokirja (1857 KB, 94 s.)
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher Teknillinen korkeakoulu en
dc.relation.haspart [Publication 1]: Harri Haanpää, Matti Järvisalo, Petteri Kaski, and Ilkka Niemelä. 2006. Hard satisfiable clause sets for benchmarking equivalence reasoning techniques. Journal on Satisfiability, Boolean Modeling and Computation, volume 2, numbers 1-4, pages 27-46. © 2006 Delft University of Technology. By permission. en
dc.relation.haspart [Publication 2]: Matti Järvisalo and Ilkka Niemelä. 2008. The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study. Journal of Algorithms: Algorithms in Cognition, Informatics and Logic, volume 63, numbers 1-3, pages 90-113. © 2008 Elsevier Science. By permission. en
dc.relation.haspart [Publication 3]: Matti Järvisalo and Tommi Junttila. 2008. Limitations of restricted branching in clause learning. Constraints, to appear, 29 pages. © 2008 by authors and © 2008 Springer Science+Business Media. By permission. en
dc.relation.haspart [Publication 4]: Matti Järvisalo and Tommi Junttila. 2008. On the power of top-down branching heuristics. In: Dieter Fox and Carla P. Gomes (editors). Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI 2008). Chicago, Illinois, USA. 13-17 July 2008. AAAI Press, pages 304-309. en
dc.relation.haspart [Publication 5]: Matti Järvisalo and Emilia Oikarinen. 2008. Extended ASP tableaux and rule redundancy in normal logic programs. Theory and Practice of Logic Programming, volume 8, numbers 5-6, pages 691-716. en
dc.relation.haspart [Publication 6]: Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. 2008. Justification-based non-clausal local search for SAT. In: Malik Ghallab, Constantine D. Spyropoulos, Nikos Fakotakis, and Nikos Avouris (editors). Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008). Patras, Greece. 21-25 July 2008. IOS Press. Frontier in Artificial Intelligence and Applications, volume 178, pages 535-539. © 2008 IOS Press. By permission. en
dc.relation.haspart [Publication 7]: Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. 2008. Justification-based local search with adaptive noise strategies. In: Iliano Cervesato, Helmut Veith, and Andrei Voronkov (editors). Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008). Doha, Qatar. 22-27 November 2008. Springer. Lecture Notes in Computer Science, volume 5330, pages 31-46. © 2008 Springer Science+Business Media. By permission. en
dc.subject.other Computer science en
dc.title Structure-based satisfiability checking : analyzing and harnessing the potential en
dc.type G5 Artikkeliväitöskirja fi
dc.contributor.department Tietojenkäsittelytieteen laitos fi
dc.subject.keyword propositional satisfiability en
dc.subject.keyword SAT en
dc.subject.keyword clause learning en
dc.subject.keyword DPLL en
dc.subject.keyword stochastic local search en
dc.subject.keyword branching heuristics en
dc.subject.keyword proof complexity en
dc.subject.keyword Boolean circuits en
dc.subject.keyword non-clausal formulas en
dc.subject.keyword problem structure en
dc.subject.keyword backdoors en
dc.subject.keyword hard instances en
dc.subject.keyword adaptive noise strategies en
dc.subject.keyword probabilistically approximately complete en
dc.subject.keyword answer set programming en
dc.identifier.urn URN:ISBN:978-951-22-9642-2
dc.type.dcmitype text en
dc.type.ontasot Väitöskirja (artikkeli) fi
dc.type.ontasot Doctoral dissertation (article-based) 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

Browse

My Account