Thresholds and Symmetries in Propositional Formulas

60 p.Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 2002.Two problems with application to the analysis and design of algorithms concerning the satisfiability of propositional formulas are investigated. With respect to the first problem, there is great experimental evidence for a phenomenon known as the 'phase transition' of satisfiability, that is there is a sharp threshold, in the limit, between satisfiable and unsatisfiable formulas as the ratio of clauses to variables increases. To analyze this threshold, we count the number of satisfiable boolean formulas given in conjunctive normal form. The intention is to provide information about the relative frequency of boolean functions with respect to statements of a given size. This in turn will provide information about algorithms attempting to decide problems such as satisfiability and validity. First, we describe a correspondence between the syntax of propositions and the semantics of functions using a system of equations. Then we show how to solve such a system. This gives a general solution for any set of functions represented by atomic symbols acting as literals; we simplify the specific solution for the variables and their negations as literals. And finally we extract some asymptotics and threshold bounds from this solution. The second problem is the generation of distinct models of propositional formulas, when the variables can be permuted to form the same boolean function. A model is a complete assignment to the variables, but the permutations can render some of these assignments equivalent. Generation methods are developed for specific permutation groups.U of I OnlyRestricted to the U of I community idenfinitely during batch ingest of legacy ETD