Using Join Networks to Compute Satisfiability

Abstract

Satisfiability (SAT) of propositional logic formulas is a canonical NP-complete problem; algorithms for its solution have been studied for over forty years. The representational power of propositional logic allows a host of research and real-world problems to be solved using SAT solvers: some prominent areas of application include mathematics, circuit design and verification, and AI planning. One technique receiving increasing recent attention is the use of quantified representations for SAT problems. Quantified representations are often more intuitive to use, can require exponentially less space, and in many cases allow speedup through their elimination of isomorphism. This dissertation explores the use of networks of joins operating upon quantified representations to compute key solver functions, including unit propagation and literal choice. The complexity of computing these functions using join networks becomes dependent upon the size of the truth assignment, or potential model explored at a given search space node. Because models are relatively small for many problems of interest, we show efficiency gains in these cases. JOINSAT, the implementation of these ideas, is competitive in performance with a number of state of the art satisfiability solvers.