Structure-based satisfiability checking : analyzing and harnessing the potential

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.authorJärvisalo, Matti
dc.contributor.departmentTietojenkäsittelytieteen laitosfi
dc.date.accessioned2012-08-21T07:45:55Z
dc.date.available2012-08-21T07:45:55Z
dc.date.issued2008
dc.description.abstractConstraint 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.extentVerkkokirja (1857 KB, 94 s.)
dc.format.mimetypeapplication/pdf
dc.identifier.isbn978-951-22-9642-2
dc.identifier.isbn978-951-22-9641-5 (printed)#8195;
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/4551
dc.identifier.urnURN:ISBN:978-951-22-9642-2
dc.language.isoenen
dc.publisherTeknillinen korkeakouluen
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.keywordpropositional satisfiabilityen
dc.subject.keywordSATen
dc.subject.keywordclause learningen
dc.subject.keywordDPLLen
dc.subject.keywordstochastic local searchen
dc.subject.keywordbranching heuristicsen
dc.subject.keywordproof complexityen
dc.subject.keywordBoolean circuitsen
dc.subject.keywordnon-clausal formulasen
dc.subject.keywordproblem structureen
dc.subject.keywordbackdoorsen
dc.subject.keywordhard instancesen
dc.subject.keywordadaptive noise strategiesen
dc.subject.keywordprobabilistically approximately completeen
dc.subject.keywordanswer set programmingen
dc.subject.otherComputer scienceen
dc.titleStructure-based satisfiability checking : analyzing and harnessing the potentialen
dc.typeG5 Artikkeliväitöskirjafi
dc.type.dcmitypetexten
dc.type.ontasotVäitöskirja (artikkeli)fi
dc.type.ontasotDoctoral dissertation (article-based)en
local.aalto.digiauthask
local.aalto.digifolderAalto_68241
Files
Original bundle
Now showing 1 - 6 of 6
No Thumbnail Available
Name:
isbn9789512296422.pdf
Size:
1.77 MB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
publication1.pdf
Size:
361.74 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
publication2.pdf
Size:
487.37 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
publication3.pdf
Size:
287.6 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
publication6.pdf
Size:
189.57 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
publication7.pdf
Size:
1.69 MB
Format:
Adobe Portable Document Format