Copyright © 2009 K. Subramani. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
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, while
hull inclusion queries are analyzed over continuous and discrete sets defined by rational polyhedra. Although
CNF formulas can be represented by polyhedra over discrete sets, we analyze them separately on account
of their distinct structure. In particular, we consider the NAESAT and XSAT versions of satisfiability over
HornCNF, 2CNF, and Horn2CNF formulas. These restricted families find applications in a number of
practical domains. From the hull inclusion perspective, we are primarily concerned with the question of
checking whether two succinct descriptions of a set of points are equivalent. In particular, we analyze the
complexities of integer hull inclusion over 2SAT and Horn polyhedra. Hull inclusion problems are important
from the perspective of deriving minimal descriptions of point sets. One of the surprising consequences of
our work is the stark difference in complexities between equivalence problems in the clausal and polyhedral
domains for the same polyhedral structure.