Results on Extensions of the Satisfability Problem

Bennett, Huxley David

Graduate Thesis Or Dissertation

Results on Extensions of the Satisfability Problem Public Deposited

Analytics

Citations

Citeable URL: https://scholar.colorado.edu/concern/graduate_thesis_or_dissertations/vm40xr958

Abstract

The satisfiability problem (SAT) and its extensions have become indispensible tools in artificial intelligence, verification, and many other domains. Extensions of the problem such as model counting, quantified Boolean formulae (QBF), and MAX-SAT have similarly seen increased study and applications. This thesis provides a survey on SAT, and then presents novel results related to model counting and random QBF. Chapter 3 gives a general technique for computing inclusion-exclusion sums more efficiently for the purpose of model counting. The main contribution is a subsumption technique which reduces computational overhead. Treating an inclusion-exclusion sum's computation as tree exploration, subsumption allows us to prune large subtrees. We also give a better worst-case upper bound on the algorithm's running time, improving it from exponential in the number of clauses to the number of variables in a CNF formula. Chapter 5 describes a new phase transition in random QBF, along with related results on random QBF models. The clause-to-variable ratio phase transition identified in random $k$-SAT has been the subject of intense study on what makes a SAT instance intractable, and recent work has studied a similar transition in random QBF. Here we show that a satisfiability threshold exists around phase transitions arising from altering the fraction of existentially versus universally quantified variables in a formula. In chapter 6 we revisit work on generating trivially false formulas in several related random QBF models, giving precise bounds for how likely they are to occur.

Creator