On the Complexities of Selected Satisfiability and Equivalence Queries over Boolean Formulas and Inclusion Queries over Hulls

摘要

This paper is concerned with the computational complexities of three types of queries, namely, satisfiability,equivalence, and hull inclusion. The first two queries are analyzed over the domain of CNF formulas, whilehull inclusion queries are analyzed over continuous and discrete sets defined by rational polyhedra. AlthoughCNF formulas can be represented by polyhedra over discrete sets, we analyze them separately on accountof their distinct structure. In particular, we consider the NAESAT and XSAT versions of satisfiability overHornCNF, 2CNF, and Horn⊕2CNF formulas. These restricted families find applications in a number ofpractical domains. From the hull inclusion perspective, we are primarily concerned with the question ofchecking whether two succinct descriptions of a set of points are equivalent. In particular, we analyze thecomplexities of integer hull inclusion over 2SAT and Horn polyhedra. Hull inclusion problems are importantfrom the perspective of deriving minimal descriptions of point sets. One of the surprising consequences ofour work is the stark difference in complexities between equivalence problems in the clausal and polyhedraldomains for the same polyhedral structure.