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 domainof CNF formulas, while hull inclusion queries are analyzed over continuous and discrete setsdefined by rational polyhedra. Although CNF formulas can be represented by polyhedra overdiscrete sets, we analyze them separately on account of their distinct structure. In particular, weconsider the NAESAT and XSAT versions of satisfiability over HomCNF, 2CNF, and Horne2CNFformulas. These restricted families find applications in a number of practical domains. From thehull inclusion perspective, we are primarily concerned with the question of checking whether twosuccinct descriptions of a set of points are equivalent. In particular, we analyze the complexities ofinteger hull inclusion over 2SAT and Horn polyhedra. Hull inclusion problems are important fromthe perspective of deriving minimal descriptions of point sets. One of the surprising consequencesof our work is the stark difference in complexities between equivalence problems in the clausaland polyhedral domains for the same polyhedral structure.