Browsing Theses by Subject "SAT"
Now showing items 1-7 of 7
-
An Analysis of the Effect of Community Structure on SAT Solver Performance
(University of Waterloo, 2015-01-21)Despite enormous improvements in Boolean SATisfiability solver performance over the last decade, it is still unclear why specific input formula are slow to solve, when other similarly specified formula execute more ... -
Backdoors in Satisfiability Problems
(University of Waterloo, 2009-10-08)Although satisfiability problems (SAT) are NP-complete, state-of-the-art SAT solvers are able to solve large practical instances. The notion of backdoors has been introduced to capture structural properties of instances. ... -
Exploiting Structure in Backtracking Algorithms for Propositional and Probabilistic Reasoning
(University of Waterloo, 2010-08-03)Boolean propositional satisfiability (SAT) and probabilistic reasoning represent two core problems in AI. Backtracking based algorithms have been applied in both problems. In this thesis, I investigate structure-based ... -
Novel Value Ordering Heuristics Using Non-Linear Optimization In Boolean Satisfiability
(University of Waterloo, 2012-08-30)Boolean Satisfiability (SAT) is a fundamental NP-complete problem of determining whether there exists an assignment of variables which makes a Boolean formula evaluate to True. SAT is a convenient representation for many ... -
On the relationship between satisfiability and partially observable Markov decision processes
(University of Waterloo, 2018-09-26)Stochastic satisfiability (SSAT), Quantified Boolean Satisfiability (QBF) and decision-theoretic planning in finite horizon partially observable Markov decision processes (POMDPs) are all PSPACE-Complete problems. Since ... -
Prioritized Unit Propagation and Extended Resolution Techniques for SAT Solvers
(University of Waterloo, 2023-08-29)NP-complete problems like the Boolean Satisfiability (SAT) Problem are ubiquitous in computer science, mathematics, and engineering. Consequently, researchers have developed algorithms such as Conflict-Driven Clause-Learning ... -
Randomization and Restart Strategies
(University of Waterloo, 2006)The runtime for solving constraint satisfaction problems (CSP) and propositional satisfiability problems (SAT) using systematic backtracking search has been shown to exhibit great variability. Randomization and restarts ...