dc.contributor.author Li, Chunxiao dc.date.accessioned 2019-09-09 12:48:50 (GMT) dc.date.available 2019-09-09 12:48:50 (GMT) dc.date.issued 2019-09-09 dc.date.submitted 2019-09-02 dc.identifier.uri http://hdl.handle.net/10012/15024 dc.description.abstract Restart policy is a widely used class of techniques integral to the efficiency of conflict-driven clause-learning (CDCL) SAT solvers. While the utility of such policies has been well-established, to-date we still lack a deep theoretical understanding of why restart policies are crucial to the power of CDCL SAT solvers. en In this paper, we provide a series of results that theoretically establish the power of restarts for various models of Boolean SAT solvers. More precisely, we make the following contributions. First, we show that certain model of CDCL solvers with restarts are no more powerful from a proof-complexity theoretic point of view than the same configurations without restarts. Second, we define \textit{decision depth} for DPLL proofs of an unsatisfiable formula $\varphi$, and then we relate decision depth of $\varphi$ and size of DPLL proofs (or the running time of a DPLL based solver) for $\varphi$. Third, we introduce a new class of satisfiable instances called $Ladder_n$, then we use decision depth as a tool to proved that a drunk style DPLL solver with restarts can solve $Ladder_n$ in polynomial time with high probability while the solvers with the same configuration without restarts have exponential run time with high probability. Finally, the crucial insight that drives this line of research is the fact that restarts add proof-theoretic or algorithmic power to solver configurations by compensating for the weaknesses of some other important heuristics like branching or value selection or clause learning. dc.language.iso en en dc.publisher University of Waterloo en dc.subject proof complexity en dc.subject power of restarts en dc.subject branching heuristics en dc.title Towards a Theoretical Understanding of the Power of Restart in SAT solvers en dc.type Master Thesis en dc.pending false uws-etd.degree.department Electrical and Computer Engineering en uws-etd.degree.discipline Electrical and Computer Engineering en uws-etd.degree.grantor University of Waterloo en uws-etd.degree Master of Applied Science en uws.contributor.advisor Ganesh, Vijay uws.contributor.affiliation1 Faculty of Engineering en uws.published.city Waterloo en uws.published.country Canada en uws.published.province Ontario en uws.typeOfResource Text en uws.peerReviewStatus Unreviewed en uws.scholarLevel Graduate en
﻿

### This item appears in the following Collection(s)

UWSpace

University of Waterloo Library
200 University Avenue West