• English
    • Deutsch
  • English 
    • English
    • Deutsch
  • Login
View Item 
  •   Home
  • Universität Ulm
  • Publikationen
  • View Item
  •   Home
  • Universität Ulm
  • Publikationen
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Engineering stochastic local search for the satisfiability problem

Thumbnail
vts_8852_13227.pdf (5.406Mb)
165 S.
Veröffentlichung
2014-01-21
Authors
Balint, Adrian
Dissertation


Faculties
Fakultät für Ingenieurwissenschaften und Informatik
Abstract
This thesis describes new algorithms for the Propositional Satisfiability Problem (SAT), a fundamental problem in theoretical and practical computer science. Besides the theoretical relevance of the SAT problem, many practical applications corroborate the importance of the SAT problem. Within this thesis, we provide different improvements for SLS solvers, and also propose new SLS solving techniques for the SAT problem. By means of empirical evaluations, we compare our solving methods with available state-of-the-art methods and show the superiority of the former. The results of our solvers within different SAT competitions further confirm their state-of-the-art performance. First, we propose a new technique to analyze the search behavior of an SLS solver. We show that this approach can be used to construct hybrid solvers that are able to exceed the performance of the SLS component. We present a new type of heuristic for SLS solvers based on the concept of probability distributions, which we implement in the solver Sparrow that reaches state-of-the-art performance on a wide range of randomly generated SAT problems. To improve the applicability of SLS solvers on structured problems, we analyze different preprocessing techniques in combination with the solver Sparrow. We are able to show that the performance of SLS solvers can be significantly improved on structured problems. Within our final study, we propose and analyze a solver based solely on probability distributions. Our new solver, named probSAT, allows a detailed analysis of the role of make and break for SLS solvers. Within comprehensive evaluations, we analyze probSAT on different SAT problems, and show that it establishes new state-of-the-art standards. Finally we present an advanced framework for the empirical evaluation of algorithms, named EDACC, which provides a plethora of functionalities for the design, execution and analysis of experiments with all kind of algorithms.
Date created
2013
Subject headings
[GND]: Erfüllbarkeitsproblem
[LCSH]: Computational complexity | Satisfiability
[Free subject headings]: Algorithm engineering | SAT solving
[DDC subject group]: DDC 004 / Data processing & computer science
License
Standard
https://oparu.uni-ulm.de/xmlui/license_v3

Metadata
Show full item record

DOI & citation

Please use this identifier to cite or link to this item: http://dx.doi.org/10.18725/OPARU-2524

Balint, Adrian (2014): Engineering stochastic local search for the satisfiability problem. Open Access Repositorium der Universität Ulm und Technischen Hochschule Ulm. Dissertation. http://dx.doi.org/10.18725/OPARU-2524
Citation formatter >



Policy | kiz service OPARU | Contact Us
Impressum | Privacy statement
 

 

Advanced Search

Browse

All of OPARUCommunities & CollectionsPersonsInstitutionsPublication typesUlm SerialsDewey Decimal ClassesEU projects UlmDFG projects UlmOther projects Ulm

My Account

LoginRegister

Statistics

View Usage Statistics

Policy | kiz service OPARU | Contact Us
Impressum | Privacy statement