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

Authors: K. Subramani
Journal: Journal of Applied Mathematics and Decision Sciences
 (2009)

---

## Abstract

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 Horn⊕2CNF 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.


---

## Body

## 1. Introduction

The problem of testing the satisfiability of CNF formulas (or SAT) is ubiquitous in computer science and operations research. Applications of this problem abound from areas as diverse as econometrics and planning to graph theory and combinatorial optimization [1]. From the perspective of computational complexity, SAT was immortalized in [2] as the first natural  NP-complete problem. Advances in SAT research have been along both theoretical and practical lines. On the theoretical side, there exist a number of algorithms running in time o(2n), for instance, see [3–5]. On the practical front, greedy approaches based on random walks have been enormously successful [6, 7].One of the approaches taken by SAT theoreticians is to identify structures of SAT families that are amenable to solution through polynomial time procedures. This approach has the benefit of defining yardsticks that categorize classes of SAT problems as polynomial time solvable orNP-complete [8]. Tractable families are distinguished by a specific clausal structure; these structures either limit the number of literals per clause [9, 10] or the number of times that a variable appears across all the clauses [11]. A completely orthogonal approach to SAT research is to study the complexities of SAT variants, that is, satisfiability problems with additional requirements on the type of solutions. For instance, in the NAESAT problem, we are required to find an assignment that satisfies all the clauses but falsifies at least one literal per clause. This paper is interested in such syntactic variants of the SAT problem, inasmuch as these variants arise naturally in the domains of graph theory and scheduling.This paper also focuses on hull inclusion problems over continuous and discrete sets of points. Hull inclusion is checkable in polynomial time when the domain is continuous andNP-complete when the domain is discrete. However, there exist nontrivial cases of hull inclusion in discrete domains which are polynomial time solvable on account of the structure of the constraint matrix. These hull inclusion problems find applications in program verification [12, 13]. Although SAT problems can be cast as discrete domain polyhedral problems, we choose to treat them separately in order to exploit their structure. In this context, we will show that a particular problem is polynomial time solvable over Boolean CNF formulas, but provably hard over arbitrary polyhedra.The principal contributions of this paper are as follows.(a)
Establishing the complexities of NAESAT and XSAT queries over restricted CNF families (see Section2 for definitions of CNF restrictions).(b)
Introducing the problems of NAE-equivalence and X-equivalence and establishing their complexities over restricted CNF families.(c)
Developing a polynomial time algorithm for Linear hull inclusion.(d)
Establishing the complexities of Integer hull inclusion over various polyhedral families.The rest of this paper is organized as follows. Section2 formally describes each of the problems considered in this paper. In Section 3, we discuss the motivation for our work as well as related approaches in the literature. The complexities of satisfiability queries over various clausal families are detailed in Section 4. Boolean equivalence queries and their variants are discussed in Section 5. An algorithm for Linear hull inclusion is discussed in Section 6. Section 7 is concerned with Integer hull inclusion over various polyhedral families. We conclude in Section 8 by summarizing our work in this paper and identifying avenues for future research.


## 2. Statement of Problems

We begin with definitions of satisfiability-related problems on clausal Boolean formulas.Letϕ=C1⋀C2⋀…Cm denote a Boolean formula in conjunctive normal form (CNF), where the Cis are disjunctions on the literals {x1,x̅1,x2,x̅2,…,xn,x̅n}. For the rest of the paper, we assume that our formulas are in CNF over the n variables {x1,x2,…xn}, unless otherwise stated.Definition 2.1.
The Boolean satisfiability  (SAT) problem is: Givenϕ, is there a {true,false} assignment to the variables of ϕ, such that at least one literal in each clause is set to true.If such an assignmentx⃗ exists for a given CNF formula ϕ, then ϕ is said to be satisfiable and x⃗ is said to be a satisfying assignment. There are other variants of satisfiability of interest in the CNF case, where the number of true literals or the mix of true and false literals per clause is specified.Definition 2.2.
The Not-All-Equal satisfiability (NAESAT) problem is defined as follows: Given a Boolean formulaϕ, does ϕ have a satisfying assignment, such that at least one literal in each clause is set to false. If such an assignment exists, then it is called a NAE-satisfying assignment and ϕ is said to be NAE-satisfiable.Definition 2.3.
The Exact satisfiability (XSAT) problem is defined as follows. Given a Boolean formulaϕ, does ϕ have a satisfying assignment, such that exactly one literal in each clause is set to true. If such an assignment exists, then it is called an X-satisfying assignment and ϕ is said to be X-satisfiable.If a Boolean formulaϕ is unsatisfiable, then it is neither NAE-satisfiable nor X-satisfiable; however, satisfiability does not imply NAE-satisfiability or X-satisfiability.This paper will focus on Boolean formulas with restrictions on the structure of the formula. These restrictions are exploited in the design of polynomial time algorithms.Definition 2.4.
A Boolean formulaϕ is in k-CNF form, if every clause contains exactly k literals.Definition 2.5.
A Boolean formulaϕ is Horn, if every clause contains at most one positive literal.Definition 2.6.
A Boolean formulaϕ is said to be Horn⊕2CNF, if each clause contains at most two literals or at most one positive literal.Given an assignmenta1∈{true,false}n to the variables of a boolean formula ϕ, let T(a1) denote the set of variables that have been assigned true under a1.Definition 2.7.
A Boolean formulaϕ is said to be positively monotone, if for every pair of assignments a1,a2∈{true, false}n to the variables of ϕ, (T(a1)⊆T(a2))⇒(ϕ(a1)⇒ϕ(a2)).Definition 2.8.
A Boolean formulaϕ is said to be negatively monotone, if for every pair of assignments a1,a2∈{true,false}n to the variables of ϕ, (T(a1)⊆T(a2))⇒(ϕ(a2)⇒ϕ(a1)).A Boolean formulaϕ is monotone if it is either positively monotone or negatively monotone. It is not hard to see that if ϕ is a CNF formula, then ϕ is monotone if all variables occur positively or all variables occur negatively.It is well known that 3SAT, NAE3SAT, and X3SAT areNP-complete [11], whereas HornSAT and 2SAT are solvable in polynomial time [10]. Horn⊕2CNF formulas have also been called Mixed Horn Formulas in the literature [14] and satisfiability checking in these formulas is also  NP-complete [10]. Monotone SAT is trivial, since all variables can be set to true (or false). Other monotone problems, however, prove more interesting.From the perspective of computational complexity, the following questions are open:(i)
What are the complexities of NAESAT over Horn and Mixed Horn formulas? These problems are called NAEHornSAT and NAEMixedHornSAT, respectively.(ii)
What are complexities of XSAT over Horn and Mixed Horn formulas? These problems are called XHornSAT and XMixedHornSAT, respectively.A problem closely related to satisfiability is the boolean equivalence problem.Definition 2.9.
Two Boolean formulasϕ1 and ϕ2 are said to be equivalent (denoted ϕ1⇔ϕ2) if every assignment that satisfies ϕ1 also satisfies ϕ2 and vice versa.The problem of checking whether two Boolean formulas are equivalent is denoted by BEQ.Observe that the equivalence problem can be broken into two subproblems, namely,ϕ1⇒ϕ2 and ϕ2⇒ϕ1.Consider the subproblemϕ1⇒ϕ2. As before, we assume that ϕ1=C1⋀C2⋯⋀Cm and that ϕ2=C1′⋀C2′⋯Cm′′. Now,
(2.1)ϕ1⇒ϕ2⟺[ϕ1⇒C1′⋀C2′⋯Cm′′]⟺⋀i=1m′[ϕ1⇒Cj′].System (2.1) exploits the well-known propositional tautology, for arbitrary propositional formulas A, B, and C:
(2.2)((A⇒B)⋀(A⇒C))⟺(A⇒(B⋀C)).
Pick a particular clause Ci′∈ϕ2. Applying the tautology
(2.3)(A⇒B)⟺(A⋀B̅⟺false)
for arbitrary propositional formulas A and B, it follows that [ϕ1⇒Ci′] if and only if [ϕ1⋀Ci′̅] is unsatisfiable.Observe thatCi′ is a disjunction of literals, so that Ci′̅ is a conjunction of unit literal clauses; hence ϕ1⋀Ci′̅ is in CNF form. Thus, in order to check whether ϕ1⇒ϕ2, we merely need to confirm that all the CNF formulas in the set {ϕ1⋀Ci′̅,ϕ1⋀C2′̅,…,ϕ1⋀Cm′′̅} are unsatisfiable. In other words, the implication problem for CNF problems has been Turing reduced to the CNF unsatisfiability problem.  Then, we have the following lemma.Lemma 2.10.
BEQ is Turing reducible to the problem of checking whether a CNF formula is unsatisfiable.Proof.
Givenϕ1 and ϕ2, first check whether ϕ1⇒ϕ2 and then whether ϕ2⇒ϕ1.Observe that there exist polynomial time algorithms to decide (un)satisfiability in 2CNF and HornCNF formulas [10], and hence it follows that BEQ can be decided in polynomial time for 2CNF and HornCNF formulas.Two problems that are closely related to the boolean equivalence problem are the NAE-equivalence problem and the X-equivalence problem.Definition 2.11.
Two Boolean formulasϕ1 and ϕ2 are said to be NAE-equivalent (denoted ϕ1⇔nϕ2) if every assignment that NAE-satisfies ϕ1 also NAE-satisfies ϕ2 and vice versa.The problem of checking whether two boolean formulas are NAE-equivalent is denoted by NAEEQ.Definition 2.12.
Two Boolean formulasϕ1 and ϕ2 are said to be X-equivalent (denoted by ⇔x) if every assignment that X-satisfies ϕ1 also X-satisfies ϕ2 and vice versa.The problem of checking whether two boolean formulas are X-equivalent is denoted by XEQ.Problem 1.
Are there classes of Boolean formulas for which NAE-equivalence and X-equivalence can be determined in polynomial time?We now proceed to describe the linear and integer hull inclusion problems for particular types of polytopes. A polytope is a bounded polyhedron. A polyhedron is defined by a linear systemA·x⃗≤b⃗, where A is an m×n integer matrix, b⃗ is an integral m-vector, and x⃗=[x1,x2,…,xn]T is the variable vector. Polytopes and polyhedra are interesting because they capture a number of problems that arise in combinatorial optimization.For the following definitions, assume that we are given two polytopesP1:{A1·x⃗≤b⃗1} and P2:{A2·x⃗≤b⃗2}.Definition 2.13.
The linear hull of a polytopeP1:{A1·x⃗≤b⃗1}, denoted by LP1, is defined as the convex hull of all the points contained in it.Definition 2.14 (see [15]).
The integer hull of a polytopeP1:{A1·x⃗≤b⃗1}, denoted by SP1, is defined as the convex hull of the lattice points contained in P1.Note that for a given polytopeA1·x⃗≤b⃗, both the linear hull and the integer hull have exponentially many extreme points. However, just as we are interested in equivalence between formulas with respect to various satisfiability measures, we are interested in comparing polytopes via their convex hulls.Definition 2.15.
The linear hull inclusion (LHI) problem is defined as follows.  Given polyhedraP1and P2,is it the case that  LP1⊆LP2?Definition 2.16.
The integer hull inclusion (IHI) problem is defined as follows.  Given polyhedraP1andP2,is it the case that  SP1⊆SP2?We first observe that the IHI problem is hard in the general case.Lemma 2.17.
IHI is  coNP-complete.Proof.
Letϕ denote an arbitrary 3CNF formula. It is well known that this formula can be represented as an integer program over {0,1}, for instance, see [16]. Set P1 to be the polyhedral system representing the 3CNF formula and P2 to the empty polyhedron {x1≥1,x1≤0}. The integer hull of P1 is contained in the integer hull of P2 if and only if the 3CNF formula ϕ is unsatisfiable. Then the lemma follows.The natural question then is the following.Problem 2.
Are there classes of polytopes for which IHI can be decided in polynomial time?We now define some special classes of polytopes. The structure of these polytopes will be exploited to design polynomial time algorithms for one or both types of hull inclusion.Definition 2.18.
A polyhedral systemP1:{A·x⃗≤b⃗} is said to be a 2SAT polytope if all entries of A belong to the set {0,1,-1} and further, there are at most 2 nonzero entries per row of A.Individual constraints of a 2SAT polytope have also been referred to as UTVPI constraints in the literature [13].Definition 2.19.
A polyhedral system of the formP1:{A·x⃗≥b⃗} is said to be a Horn polytope if all entries in A belong to {1,0,-1}, and there exists at most one positive entry in each row.Observe that 2SAT polytopes and Horn polytopes generalize 2CNF clauses and HornCNF clauses, respectively.Definition 2.20.
A matrixA is said to be totally unimodular (TUM) if every square submatrix of A has determinant 0, 1, or -1.TUM matrices arise in network flow problems [17], scheduling problems [18], and a whole host of situations in which only strict difference constraints are permitted between program variables [19]. One of the more celebrated results about TUM matrices in the operations research literature is the following. Let P1:A·x⃗≤b⃗ denote a polyhedral system, with A TUM and b⃗ integral. Then, the integer hull and linear hull of P1 are identical (see [15]).Definition 2.21.
A polyhedral system of the formP1:{A·x⃗≥b⃗}, where all entries in A belong to {1,0,-1} and each row has exactly one +1 and one -1, is called a Difference polytope.Note that the class of difference polytopes is a proper subset of the class of 2SAT polytopes and also a proper subset of the class of Horn polytopes. (See Figure1.)Figure 1
Relation between polyhedral classes.Difference polytopes are a special subset of the class of TUM polytopes. Conjunctions of difference constraints are used to capture requirements in a number of application domains such as symbolic model checking [20], verification of timed systems [21, 22], and timed automata [23, 24]. Difference constraint feasibility has also been studied as the Single Source Shortest Paths problem within the operations research and algorithms communities [25]. Additionally, separation relationships in a number of scheduling problems are captured through difference constraints [18, 26, 27]. In real-time software, temporal requirements are modeled through variants of difference constraints [28, 29].


## 3. Motivation and Related Work

The two variants of SAT that we are interested in are NAESAT and XSAT. Both these problems have a long and interesting history, inasmuch as they are closely linked to graph coloring problems [30]. Mixed Horn Formulas (MHFs) have been used in the formulation of level-planarity tests in planar graphs and crossing-minimization problems [31]. In [14], it has been argued that graph colorability can also be formulated as an MHF satisfiability problem.Convex body inclusion has been well studied in the operations research literature [32, 33]. Convex body inclusion is related to the problem of estimating the volumes of convex bodies [34, 35]. In Section 6, we present an algorithm for polytope inclusion that depends on the fact that maximizing a linear function over a polytope can be accomplished in polynomial time. Integer hull inclusion is different from convex body inclusion since in general, the set of lattice points satisfying a system of linear inequalities do not form a convex set. 2SAT polytopes were introduced in [36], where it was shown that the existence of a lattice point could be determined in O(n3) time, where n is the dimension of the polytope. It is known that the problem of obtaining the integer maximum of a linear function over a 2SAT polytope is, in general,  NP-hard. (This problem generalizes the vertex cover problem.) Horn polytopes generalize Horn clausal systems [37] and find wide application in linear complementarity and econometrics research [38].A secondary motivation for the study of clausal equivalence problems is provided by classical computational complexity. One of the goals in complexity is to find the exact threshold at which problems become hard [10]. This paper shows that the NAE-equivalence and X-equivalence problems are solvable in polynomial time for 2CNF formulas but are provably hard for the other boolean families. Likewise, we show that the integer hull inclusion problem can be solved in polynomial time for 2SAT polytopes. A surprising consequence of our work is the apparent disparity between the clausal and integer programming versions of Horn equivalence. Clausal Horn equivalence can be determined in polynomial time, whereas integer hull inclusion over Horn polytopes is  coNP-complete.


## 4. Boolean Satisfiability Queries

This section focuses on the computational complexity of the satisfiability queries detailed in Section2. It has been shown that the NAE2SAT problem can be solved in polynomial time [39]. Indeed, the results in [40] establish that NAE2SAT is in the complexity class  L (Deterministic Logarithmic Space). Likewise, NAE3SAT has been proven  NP-complete in [8]. The arguments in [8] also establish that Monotone XSAT is NP-complete.We are now ready to prove the following theorem.Theorem 4.1.
XHornSAT isNP-complete.The proof is a reduction from Monotone XSAT to XHornSAT. Before we construct the reduction, we will prove a minor but useful lemma.Lemma 4.2.
Any X-satisfying assignment for the formula(z1¯∨z2¯)⋀(z1¯∨z2¯∨z3) sets z3 to false.Proof.
We note that any X-satisfying assignment for(z1¯∨z2¯) sets one of z1 and z2 to true and the other to false. Therefore, a consistent X-satisfying assignment to (z1¯∨z2¯∨z3) must set z3 to false.Note that the formula in Lemma4.2 is Horn.Proof of Theorem4.1.
Letφ=C1⋀C2⋀⋯Ck be a monotone CNF formula. Let z1, z2, and z3 be variables that do not occur in φ, and assume without loss of generality that all variables in φ appear negated.
Let(4.1)f(φ)=(z1¯∨z2¯)⋀(z1¯∨z2¯∨z3)⋀i≤k[(¬Ci)→z3].
Observe that ifCi=(x̅1,x̅2,x̅3), then [(¬Ci)→z3] has the form: [(x1⋀x2⋀x3)→z3]. As discussed in Lemma 4.2, any X-satisfying assignment to f(φ) must set z3 to false. However, any X-satisfying assignment for a Horn clause having the form [(xi⋀xj⋀xk)→false] must set exactly one literal of (xi⋀xj⋀xk) to true. It follows that f(φ) is X-satisfiable if and only if φ is. Since f(φ) can be computed in time linear in |φ|, this reduction is polynomial-time computable.
It follows that XHornSAT isNP-complete.There is a similar reduction from monotone NAESAT to NAEHornSAT. The reduction itself is completely straightforward since a monotone clauseC is equivalent to (¬C→false). (Again, without loss of generality we assume that all variables in C are negated.)Corollary 4.3.
Monotone NAESAT≤mP NAEHornSAT, where the ≤mP stands for many-to-one polynomial time.In order to show the complexity of these two satisfiability problems, we introduce a coloring problem.Definition 4.4.
The Set Splitting problem is: given a universeU={x1,…,xn} and S⊆𝒫(U) (subsets of U), is there a coloring of {x1,…,xn} by two colors, say red and blue, so that no set in S is monochrome?Sipser gives the NP completeness of Set Splitting as an exercise [41]. There is a straightforward mapping between the sets in S and clauses in a monotone formula and between the colors and the values true and false.Lemma 4.5.
The Splitting Set problem isNP-complete, and Monotone NAESAT is equivalent to it.Corollary 4.6.
NAEHornSAT is NP-complete.Note that any NAESAT assignment to a Horn clause must set at least one body variable tofalse. Otherwise, the NAE constraint would force the body to true and the head to false, and the assignment would not satisfy the clause.Observe that NAEHornSAT and XHornSAT are bothNP-complete as shown in Theorem 4.1 and Corollary 4.6, respectively. Furthermore, HornSAT is a subclass of MixedHornSAT. Finally, note that the reductions that established the  NP-completeness of NAEHornSAT and XHornSAT have the properties that they map inputs either to NAE-satisfiable (resp, X-satisfiable) Horn formulas, or to NAE-unsatisfiable (resp, X-unsatisfiable) Horn formulas. Therefore, these very reductions establish the  NP-completeness of NAEMixedHornSAT and XMixedHornSAT, respectively.Corollary 4.7.
NAEMixedHornSAT and XMixedHornSAT areNP-complete.Table1 summarizes our discussion on clausal satisfiability queries.Table 1
Complexities of various satisfiability queries over different clausal families.
Problem2CNFHornCNF3CNFHorn⊕2CNFSATPPNP-cNP-cNAESATPNP-cNP-cNP-cXSATPNP-cNP-cNP-c


## 5. Boolean Equivalence Queries

The reasoning in Section2 can be used to establish that BEQ is  coNP-complete over 3CNF and Mixed Horn Formulas.Theorem 5.1.
BEQ is  coNP-complete for 3CNF and Mixed Horn Formulas.Proof.
Letϕ1 denote an arbitrary 3CNF formula or Mixed Horn formula. We know that the problem of checking whether ϕ1 is satisfiable is  NP-complete; thus, if we set ϕ2 to false, we can determine the satisfiability of ϕ1 by checking whether ϕ1⇔ϕ2.In similar fashion, it can be shown that the NAEEQ and XEQ problems arecoNP-complete for 3CNF and Mixed Horn Formulas.We now prove a general theorem relating the NAEEQ and BEQ problems. Letϕ denote a formula in k-CNF form, and let ϕ′ denote the CNF formula obtained by negating every literal in every clause of ϕ.Lemma 5.2.
ϕ is NAE-satisfiable if and only if ϕ⋀ϕ′ is satisfiable.Proof.
Only if: Let ϕ be NAE-satisfiable and let x⃗ denote a NAE-satisfying assignment. Let C1 denote a clause of ϕ. Since x⃗ is a NAE-satisfying assignment, it sets at least one literal to true and at least one literal to false in C1. Let C1′ denote the clause in which each literal in C1 is complemented. Note that the literal that was set to false in C1 is set to true in C1′ and vice versa; since C1 was chosen arbitrarily, the same argument applies to all clauses of ϕ. In other words, x⃗ NAE-satisfies ϕ′, and therefore, x⃗ NAE-satisfies ϕ⋀ϕ′. Hence ϕ⋀ϕ′ is satisfiable.
If: Let ϕ⋀ϕ′ be satisfiable in the ordinary sense, and let x⃗ denote a satisfying assignment. Let us study the clauses C1 and C1′ under the assignment x′⃗ which is obtained by complementing every assignment in x⃗. As per the definition of ϕ′, every literal that is set to true in Ci is set to false in C1′ and vice versa. It therefore follows that x′⃗ also satisfies both C1 and C1′. Inasmuch as C1 and C1′ were chosen arbitrarily, the same argument holds for all clause pairs, that is, x′⃗ satisfies ϕ⋀ϕ′. Now, ϕ⋀ϕ′ has a complementary pair of assignments and therefore is NAE-satisfiable. But this immediately implies the NAE-satisfiability of ϕ.Lemma5.2 leads us directly to the following lemma.Lemma 5.3.
(ϕ⇔nψ) if and only if (ϕ⋀ϕ′)⇔(ψ⋀ψ′).Proof.
Suppose that(ϕ⇔nψ) but (ϕ⋀ϕ′)⇎(ψ⋀ψ′). Without loss of generality, assume that there exists an assignment x⃗ which satisfies ϕ⋀ϕ′ but falsifies ψ⋀ψ′. Since x⃗ does not satisfy ψ⋀ψ′, it cannot NAE-satisfy ψ, as per Lemma 5.2. As per the hypothesis, it cannot NAE-satisfy ϕ either. But since x⃗ satisfies ϕ⋀ϕ′, it must NAE-satisfy ϕ, as per Lemma 5.2, and thus we have a contradiction. It follows that (ϕ⇔nψ) implies that (ϕ⋀ϕ′)⇔(ψ⋀ψ′). The converse can be proved similarly.Note that in case of 2CNF formulas, the NAEEQ and XEQ problems are identical.The next theorem follows from the previous proofs.Theorem 5.4.
The NAEEQ and XEQ problems can be solved in polynomial time for 2CNF formulas.Table2 summarizes our discussion on clausal equivalence queries.Table 2
Complexities of equivalence queries over different clausal families.
Equivalence type2CNFHornCNF3CNFHorn⊕2CNFSimplePPcoNP-completecoNP-completeNAE-equivalencePcoNP-completecoNP-completecoNP-completeX-equivalencePcoNP-completecoNP-completecoNP-complete


## 6. Linear Hull Inclusion

In this section, we focus on the problem of checking whether the linear hulls of two polyhedra defined by systems of linear inequalities are equivalent.Consider two polyhedra represented by(6.1)A·x⃗≤b⃗,x⃗≥0⃗,
where(1)
A is an m×n rational matrix,(2)
b⃗ is a rational m-vector,(3)
x⃗∈ℜ+n,and(6.2)C·x⃗≤d⃗,x⃗≥0⃗,
where(1)
C, is an m′×n rational matrix,(2)
d⃗ is a rational m′-vector,(3)
x⃗∈ℜ+nThe goal is to decide the following predicate:(6.3)(∀x⃗≥0⃗)(A·x⃗≤b⃗⇒C·x⃗≤d⃗)?
Algorithm 1 represents our strategy to decide Query (6.3).Algorithm 1:Algorithm for polytope inclusion.
Function Polytope-Include  (A,b⃗,C,d⃗)(1){Lettheithconstraint ofC·x⃗≤d⃗,x⃗≥0⃗be represented as:c⃗i·x⃗≤di}.(2)for(i=1  tom′) do(3) if(maxA·x⃗≤b⃗,x⃗≥0⃗c⃗i·x⃗>di) then(4)return (false)(5)end if(6)end for(7)return (true)


### 6.1. Analysis

Letℒ(m,n) denote the polynomial running time of a linear programming algorithm on m constraints and n variables [42]. Since a total of m′ calls are made, the running time of Algorithm 1 is O(m′·ℒ), which is polynomial, since ℒ is a polynomial function of m and n.


### 6.2. Correctness

Lemma 6.1.
If Algorithm1 returns true, then for all  x⃗∈ℜ+n,A·x⃗≤b⃗⇒C·x⃗≤d⃗.Proof.
Let us assume the contrary, that is, Algorithm1 returns true, yet there exists a point x′⃗ such that A·x′⃗≤b⃗, but C·x′⃗≰d⃗. We note that the notation C·x′⃗≰d⃗ is used to indicate the fact that at least one of the m′ constraints defining the polyhedron C·x⃗≤d⃗ is violated. Let c′⃗·x⃗≤d′ denote a violated constraint, that is, c′⃗·x′⃗>d′. (See Figure 2.) Then  maxA·x⃗≤b⃗,x⃗≥0⃗c′⃗·x⃗ is greater than d′, contradicting the hypothesis that true was returned by the algorithm.Figure 2
Polytope noninclusion.Lemma 6.2.
If Algorithm1 returns false, there exists a point x′⃗∈R+n such that A·x′⃗≤b⃗ and C·x′⃗≰d⃗.Proof.
See Figure2. Let maxA·x⃗≤b⃗c'⃗·x⃗ exceed d′ at point x′⃗. Then x′⃗ is the required offending point, that is, x′⃗∈A·x⃗≤b⃗,x⃗≥0⃗, but x′⃗∉C·x⃗≤d⃗,x⃗≥0⃗.Corollary 6.3.
Algorithm1 decides if the polyhedron defined by A·x⃗≤b⃗,x⃗≥0⃗ is contained in the polyhedron represented by C·x⃗≤d⃗,x⃗≥0⃗Note that the linear hull inclusion problem is decidable in polynomial time, irrespective of the polyhedral system involved, that is, the polyhedral system could be completely arbitrary (and not necessarily one of 2SAT, Horn or TUM).


## 6.1. Analysis

Letℒ(m,n) denote the polynomial running time of a linear programming algorithm on m constraints and n variables [42]. Since a total of m′ calls are made, the running time of Algorithm 1 is O(m′·ℒ), which is polynomial, since ℒ is a polynomial function of m and n.


## 6.2. Correctness

Lemma 6.1.
If Algorithm1 returns true, then for all  x⃗∈ℜ+n,A·x⃗≤b⃗⇒C·x⃗≤d⃗.Proof.
Let us assume the contrary, that is, Algorithm1 returns true, yet there exists a point x′⃗ such that A·x′⃗≤b⃗, but C·x′⃗≰d⃗. We note that the notation C·x′⃗≰d⃗ is used to indicate the fact that at least one of the m′ constraints defining the polyhedron C·x⃗≤d⃗ is violated. Let c′⃗·x⃗≤d′ denote a violated constraint, that is, c′⃗·x′⃗>d′. (See Figure 2.) Then  maxA·x⃗≤b⃗,x⃗≥0⃗c′⃗·x⃗ is greater than d′, contradicting the hypothesis that true was returned by the algorithm.Figure 2
Polytope noninclusion.Lemma 6.2.
If Algorithm1 returns false, there exists a point x′⃗∈R+n such that A·x′⃗≤b⃗ and C·x′⃗≰d⃗.Proof.
See Figure2. Let maxA·x⃗≤b⃗c'⃗·x⃗ exceed d′ at point x′⃗. Then x′⃗ is the required offending point, that is, x′⃗∈A·x⃗≤b⃗,x⃗≥0⃗, but x′⃗∉C·x⃗≤d⃗,x⃗≥0⃗.Corollary 6.3.
Algorithm1 decides if the polyhedron defined by A·x⃗≤b⃗,x⃗≥0⃗ is contained in the polyhedron represented by C·x⃗≤d⃗,x⃗≥0⃗Note that the linear hull inclusion problem is decidable in polynomial time, irrespective of the polyhedral system involved, that is, the polyhedral system could be completely arbitrary (and not necessarily one of 2SAT, Horn or TUM).


## 7. Integer Hull Inclusion

Let us restate the Integer hull inclusion problem (IHI).Given polyhedra  P1:{A1·x⃗≤b⃗1}and  P2:{A2·x⃗≤b⃗2}, is it the case that the integer hull ofP1is contained within the integer hull ofP2, that is,  is  SP1⊆SP2?We point out some relevant information.(1)
Algorithm1 shows that the hull inclusion problem (Linear or Integer) is Turing reducible to the problem of finding the maximum (linear or integer) of a linear function over a polyhedron.(2)
It therefore follows that the  IHI problem can be solved in polynomial time whenA1,A2 are TUM. Note that when the vectors b⃗1,b⃗2 are integral, Algorithm 1 works as is, since the linear hull is identical to the integer hull. If the b⃗i vectors are not integral, we make the observation that the integer hull of Ai·x⃗≤b⃗i is identical to the linear hull of Ai·x⃗≤⌊b⃗i⌋ when the Ai are TUM, and use Algorithm 1 on the modified polyhedra. For the rest of this paper, we will assume that the vectors b⃗1,b⃗2 are integral.(3)
Optimizing a linear function over an arbitrary 2SAT polytope isNP-hard since it subsumes the vertex cover problem [15, 43], and hence we cannot directly use the technique discussed in Section 6. Likewise, maximizing an arbitrary linear function over a Horn polytope is  NP-hard, and thus the technique of Section 6 is inapplicable (see Section 7.2).


### 7.1.   2SAT  Polytopes

Assume thatA1 has dimension m×n and that A2 has dimensions m′×n. Note that P1 is constructed by taking the intersection of the m half-spaces a⃗11·x⃗≤b11,a⃗12·x⃗≤b12,…a⃗1m·x⃗≤b1m. Likewise, P2 is constructed by taking the intersection of the m′ half-spaces, a⃗21·x⃗≤b21,a⃗22·x⃗≤b22,…a⃗2m′·x⃗≤b2m′.Observe thatSP1⊆SP2 if and only if for all lattice points x⃗,(x⃗∈P1⇒x⃗∈P2). Now, for a lattice point x⃗,
(7.1)(x⃗∈P1⇒x⃗∈P2)⟺(x⃗∈P1⇒x⃗∈⋀j=1m′a⃗2j·x⃗≤b2j)⟺(⋀j=1m′[x⃗∈P1⇒a⃗2j·x⃗≤b2j]).Let us focus on proving(x⃗∈P1⇒a⃗2j·x⃗≤b2j), for a specific constraint of P2, that is, the jth half-space defining P2. As in the case of CNF equivalence, we observe that for lattice points x⃗, (x⃗∈P1⇒a⃗2j·x⃗≤b2j), if and only if the set P1⋀[a⃗2j·x⃗≰b2j] is empty with respect to lattice points. Note that the constraint a⃗2j·x⃗≰b2j can be written as: l1:a⃗2j·x⃗>b2j. But we are only interested in lattice point solutions. Consequently, a lattice point solution will satisfy the constraint l1 if and only if it satisfies the constraint a⃗2j·x⃗≥(b2j+1), which is a closed half-space. Thus, we can check that (x⃗∈P1⇒a⃗2j·x⃗≤b2j) for all lattice points x⃗, by checking whether the polyhedron P1⋀a⃗2j·x⃗≥(b2j+1) is empty with respect to lattice points. The operation of negating a constraint is referred to as constraint complementation.The discussion above implies the following theorem.Theorem 7.1.
Given polyhedraP1 and P2, the IHI problem turing reduces to the problem of checking whether a polyhedron does not have any lattice point.Corollary 7.2.
The IHI problem can be solved in polynomial time for 2SAT polytopes.Proof.
2SAT polytopes are defined by constraints that are closed under constraint complementation, insofar as lattice points are concerned. For instance, the complement of the constraintx1-x2≤4 is -x1+x2>-4, which is equivalent to -x1+x2≥-3 if only integral values of x1 and x2 are permitted. In other words, the complement of a constraint in a 2SAT polytope is also a 2SAT constraint. The presence or absence of lattice points in a 2SAT algorithm can be checked using the algorithm in [36], which runs in O(n3) time. The corollary follows.


### 7.2. Horn Polytopes

Observe that Horn constraints are not closed under constraint complementation. For instance, the negation of the Horn constraintx1-x2-x3≥5 is x1-x2-x3<5, which is equivalent to x1-x2-x3≤-4 (since the xis are integral) and hence equivalent to -x1+x2+x3≥4. Note that the last constraint is not a Horn constraint but an anti-Horn constraint!We will show that the  IHI problem for Horn polytopes is  coNP-complete. In order to establish this result, we study a related problem, namely, PK(Horn, 1).Given a Horn systemA·x⃗≥b⃗and a single non-Horn constraintc⃗·x⃗≥d,  does the polyhedral system  A·x⃗≥b⃗⋀c⃗·x⃗≥d, enclose a lattice point?We will use a reduction from the following problem.Definition 7.3.
The HittingSet (HS) problem is: Given a set S={s1,s2,…,sn} called the ground set, a collection of m subsets Ti⊆S, i=1,2,…,m, and a number K≤n, does there exist a set S′⊆S, such that |S′|≤K and Ti∩S′≠ϕ,i=1,2,…m?Theorem 7.4.
HS isNP-complete.The Hitting Set problem and a proof of itsNP-completeness are provided in [11].Corollary 7.5.
PK(Horn,1) is  NP-complete.Proof.
PK(Horn,1)  ∈  NP from the  NP-completeness of Integer Programming [19]. We reduce the Hitting Set problem to PK(Horn, 1).
Given an instance of HS, with ground setS={s1,s2,…,sn}, m sets Ti⊆S and the target K, we construct an instance of the following variation of CNF satisfiability called MCNF. Corresponding to the ground set S, we create the literal set L={x1,x2,…,xn}. Corresponding to each subset Ti={si1,si2,…,sip}, we create the clause Ci={xi1,xi2,…,xip}, where each ik indexes the set {1,2,…,n}. The query in MCNF is as follows. Does there exist an assignment that satisfies the clause set ϕ=C1⋀C2⋀⋯⋀Cm such that the number of variables set to true is at most K? Note that all literals are positive in the MCNF instance.
Assume that the instance of HS is a “yes” instance, that is, there exists a setS′⊆S such that |S′|∩Ti≠ϕ, such that |S′|≤K. Set the literals corresponding to the variables in S′ to true and all other literals to false. By construction, each clause Ci is satisfied. Since the number of literals set to true is K, the instance of MCNF is also a “yes” instance.
Now assume that the instance of MCNF is a “yes” instance, that is, there exists a{true, false} assignment to the literals of ϕ, such that all clauses are satisfied and the number of literals set to true is at most K. Construct the set S′ with those elements si∈S, such that xi=true. By construction, S′ intersects each Ti in at least one element (since each clause is satisfied), and the cardinality of S′ is at most K. It follows that the instance of HS is also a “yes” instance.
We now transform the MCNF instance into an instance of PK(Horn,1) as follows. Create n variables y1,y2,…,yn, where each yi∈{0,1}. Corresponding to the clause Ci=(xi1,xi2,xi3) (say), create the Horn constraint: (1-yi1)+(1-yi2)+(1-yi3)≥1. Finally, add the non-Horn constraint: ∑i=1nyi≥n-K. Thus, the MCNF instance is transformed into the following PK(Horn, 1) instance: A·y⃗≥b⃗⋀∑i=1nyi≥n-K, where A has the Horn structure and b⃗ is an integral vector.
Assume that the MCNF instance is a “yes” instance. For each literalxi set to true, set yi to 0 and for each literal xj set to false, set yj to 1. Since each clause is satisfied, it must be the case that each Horn constraint is satisfied, as per construction of the Horn constraint. Further, since the number of variables set to true in the MCNF instance is at most K, the number of yis set to 0 is at most K and hence the number of yis set to 1 is at least n-K, that is, we must have ∑i=1nyi≥n-K. Thus, the PK(Horn, 1) instance is a “yes”-instance.
Now assume that the PK(Horn,1) instance is a “yes” instance. Set xi to true, if yi=0 and xi to false, if yi=1. As per the construction, each clause must be satisfied, since each Horn constraint is satisfied. Further, the number of yis set to 1 is at least n-K, and hence the number of xis set to true is at most K. It follows that the MCNF instance is a “yes” instance.We get a small bonus from this result which is useful for our next theorem.Definition 7.6.
Let HMax denote the following problem. Given a Horn polytopeA·x⃗≥b⃗ and a number K, do there exist x1,x2,…,xn∈{0,1} such that A·x′⃗≥b⃗ and ∑i=1nxi≥K, where x′⃗=[x1,x2,…,xn]T?Corollary 7.7.
HMax is NP-complete.Proof.
This follows from Corollary7.2.We now use theNP-completeness of HMax to prove the following.Theorem 7.8.
The IHI problem for Horn polytopes, that is, IH-Horn, is  coNP-complete.Proof.
From the proof that integer programming is inNP, we know that the  IHI problem is in  coNP [10].
LetA1·x⃗≥b⃗1,xi∈{0,1},i=1,2,…,n, and K describe an instance of HMax. We create the following instance of the  IHI-Horn problem:P1:A1·x⃗≥b⃗1,xi∈{0,1},i=1,2,…,n, and P2:-∑i=1nxi≥(1-K).
We now argue that the instance of HMax is true if and only if the instance of  IHI-Horn is false, that is,(7.2)∃x⃗∈{0,1}nA1·x⃗≥b⃗⋀∑i=1nxi≥K⟺P1⊈P2.
Note thatP1 is a Horn system, as per the hypothesis and P2 is a Horn system by definition.
Assume that the  IHI-Horn instance is true, that is,P1⊆P2.
We then have fol allx⃗:A1·x⃗≥b⃗⇒-∑i=1nxi≥(1-K). It follows that for all x⃗:A1·x⃗≥b⃗⇒∑i=1nxi≤(K-1). Hence, the instance of  HMax is false.
Now assume that the HMax instance is true, that is,∃x'⃗∈{0,1}nA1·x⃗≥b⃗⋀∑i=1nxi′≥K. This implies that there exists x′⃗∈P1, with ∑i=1nxi′≥K, that is, -∑i=1nxi′≤-K. Thus, -∑i=1nxi′<(-K+1), and hence -∑i=1nxi′<-(K-1). It follows that x⃗′∈P1 is not contained in P2, and hence the instance of IHI-Horn is false.
The theorem follows.Table3 summarizes the discussion on Integer hull inclusion problems.Table 3
Complexities of Integer hull inclusion problems over various polyhedral families.
Polyhedral systemHull inclusionDiffP2SATPTUMPHorncoNP-complete


## 7.1.   2SAT  Polytopes

Assume thatA1 has dimension m×n and that A2 has dimensions m′×n. Note that P1 is constructed by taking the intersection of the m half-spaces a⃗11·x⃗≤b11,a⃗12·x⃗≤b12,…a⃗1m·x⃗≤b1m. Likewise, P2 is constructed by taking the intersection of the m′ half-spaces, a⃗21·x⃗≤b21,a⃗22·x⃗≤b22,…a⃗2m′·x⃗≤b2m′.Observe thatSP1⊆SP2 if and only if for all lattice points x⃗,(x⃗∈P1⇒x⃗∈P2). Now, for a lattice point x⃗,
(7.1)(x⃗∈P1⇒x⃗∈P2)⟺(x⃗∈P1⇒x⃗∈⋀j=1m′a⃗2j·x⃗≤b2j)⟺(⋀j=1m′[x⃗∈P1⇒a⃗2j·x⃗≤b2j]).Let us focus on proving(x⃗∈P1⇒a⃗2j·x⃗≤b2j), for a specific constraint of P2, that is, the jth half-space defining P2. As in the case of CNF equivalence, we observe that for lattice points x⃗, (x⃗∈P1⇒a⃗2j·x⃗≤b2j), if and only if the set P1⋀[a⃗2j·x⃗≰b2j] is empty with respect to lattice points. Note that the constraint a⃗2j·x⃗≰b2j can be written as: l1:a⃗2j·x⃗>b2j. But we are only interested in lattice point solutions. Consequently, a lattice point solution will satisfy the constraint l1 if and only if it satisfies the constraint a⃗2j·x⃗≥(b2j+1), which is a closed half-space. Thus, we can check that (x⃗∈P1⇒a⃗2j·x⃗≤b2j) for all lattice points x⃗, by checking whether the polyhedron P1⋀a⃗2j·x⃗≥(b2j+1) is empty with respect to lattice points. The operation of negating a constraint is referred to as constraint complementation.The discussion above implies the following theorem.Theorem 7.1.
Given polyhedraP1 and P2, the IHI problem turing reduces to the problem of checking whether a polyhedron does not have any lattice point.Corollary 7.2.
The IHI problem can be solved in polynomial time for 2SAT polytopes.Proof.
2SAT polytopes are defined by constraints that are closed under constraint complementation, insofar as lattice points are concerned. For instance, the complement of the constraintx1-x2≤4 is -x1+x2>-4, which is equivalent to -x1+x2≥-3 if only integral values of x1 and x2 are permitted. In other words, the complement of a constraint in a 2SAT polytope is also a 2SAT constraint. The presence or absence of lattice points in a 2SAT algorithm can be checked using the algorithm in [36], which runs in O(n3) time. The corollary follows.


## 7.2. Horn Polytopes

Observe that Horn constraints are not closed under constraint complementation. For instance, the negation of the Horn constraintx1-x2-x3≥5 is x1-x2-x3<5, which is equivalent to x1-x2-x3≤-4 (since the xis are integral) and hence equivalent to -x1+x2+x3≥4. Note that the last constraint is not a Horn constraint but an anti-Horn constraint!We will show that the  IHI problem for Horn polytopes is  coNP-complete. In order to establish this result, we study a related problem, namely, PK(Horn, 1).Given a Horn systemA·x⃗≥b⃗and a single non-Horn constraintc⃗·x⃗≥d,  does the polyhedral system  A·x⃗≥b⃗⋀c⃗·x⃗≥d, enclose a lattice point?We will use a reduction from the following problem.Definition 7.3.
The HittingSet (HS) problem is: Given a set S={s1,s2,…,sn} called the ground set, a collection of m subsets Ti⊆S, i=1,2,…,m, and a number K≤n, does there exist a set S′⊆S, such that |S′|≤K and Ti∩S′≠ϕ,i=1,2,…m?Theorem 7.4.
HS isNP-complete.The Hitting Set problem and a proof of itsNP-completeness are provided in [11].Corollary 7.5.
PK(Horn,1) is  NP-complete.Proof.
PK(Horn,1)  ∈  NP from the  NP-completeness of Integer Programming [19]. We reduce the Hitting Set problem to PK(Horn, 1).
Given an instance of HS, with ground setS={s1,s2,…,sn}, m sets Ti⊆S and the target K, we construct an instance of the following variation of CNF satisfiability called MCNF. Corresponding to the ground set S, we create the literal set L={x1,x2,…,xn}. Corresponding to each subset Ti={si1,si2,…,sip}, we create the clause Ci={xi1,xi2,…,xip}, where each ik indexes the set {1,2,…,n}. The query in MCNF is as follows. Does there exist an assignment that satisfies the clause set ϕ=C1⋀C2⋀⋯⋀Cm such that the number of variables set to true is at most K? Note that all literals are positive in the MCNF instance.
Assume that the instance of HS is a “yes” instance, that is, there exists a setS′⊆S such that |S′|∩Ti≠ϕ, such that |S′|≤K. Set the literals corresponding to the variables in S′ to true and all other literals to false. By construction, each clause Ci is satisfied. Since the number of literals set to true is K, the instance of MCNF is also a “yes” instance.
Now assume that the instance of MCNF is a “yes” instance, that is, there exists a{true, false} assignment to the literals of ϕ, such that all clauses are satisfied and the number of literals set to true is at most K. Construct the set S′ with those elements si∈S, such that xi=true. By construction, S′ intersects each Ti in at least one element (since each clause is satisfied), and the cardinality of S′ is at most K. It follows that the instance of HS is also a “yes” instance.
We now transform the MCNF instance into an instance of PK(Horn,1) as follows. Create n variables y1,y2,…,yn, where each yi∈{0,1}. Corresponding to the clause Ci=(xi1,xi2,xi3) (say), create the Horn constraint: (1-yi1)+(1-yi2)+(1-yi3)≥1. Finally, add the non-Horn constraint: ∑i=1nyi≥n-K. Thus, the MCNF instance is transformed into the following PK(Horn, 1) instance: A·y⃗≥b⃗⋀∑i=1nyi≥n-K, where A has the Horn structure and b⃗ is an integral vector.
Assume that the MCNF instance is a “yes” instance. For each literalxi set to true, set yi to 0 and for each literal xj set to false, set yj to 1. Since each clause is satisfied, it must be the case that each Horn constraint is satisfied, as per construction of the Horn constraint. Further, since the number of variables set to true in the MCNF instance is at most K, the number of yis set to 0 is at most K and hence the number of yis set to 1 is at least n-K, that is, we must have ∑i=1nyi≥n-K. Thus, the PK(Horn, 1) instance is a “yes”-instance.
Now assume that the PK(Horn,1) instance is a “yes” instance. Set xi to true, if yi=0 and xi to false, if yi=1. As per the construction, each clause must be satisfied, since each Horn constraint is satisfied. Further, the number of yis set to 1 is at least n-K, and hence the number of xis set to true is at most K. It follows that the MCNF instance is a “yes” instance.We get a small bonus from this result which is useful for our next theorem.Definition 7.6.
Let HMax denote the following problem. Given a Horn polytopeA·x⃗≥b⃗ and a number K, do there exist x1,x2,…,xn∈{0,1} such that A·x′⃗≥b⃗ and ∑i=1nxi≥K, where x′⃗=[x1,x2,…,xn]T?Corollary 7.7.
HMax is NP-complete.Proof.
This follows from Corollary7.2.We now use theNP-completeness of HMax to prove the following.Theorem 7.8.
The IHI problem for Horn polytopes, that is, IH-Horn, is  coNP-complete.Proof.
From the proof that integer programming is inNP, we know that the  IHI problem is in  coNP [10].
LetA1·x⃗≥b⃗1,xi∈{0,1},i=1,2,…,n, and K describe an instance of HMax. We create the following instance of the  IHI-Horn problem:P1:A1·x⃗≥b⃗1,xi∈{0,1},i=1,2,…,n, and P2:-∑i=1nxi≥(1-K).
We now argue that the instance of HMax is true if and only if the instance of  IHI-Horn is false, that is,(7.2)∃x⃗∈{0,1}nA1·x⃗≥b⃗⋀∑i=1nxi≥K⟺P1⊈P2.
Note thatP1 is a Horn system, as per the hypothesis and P2 is a Horn system by definition.
Assume that the  IHI-Horn instance is true, that is,P1⊆P2.
We then have fol allx⃗:A1·x⃗≥b⃗⇒-∑i=1nxi≥(1-K). It follows that for all x⃗:A1·x⃗≥b⃗⇒∑i=1nxi≤(K-1). Hence, the instance of  HMax is false.
Now assume that the HMax instance is true, that is,∃x'⃗∈{0,1}nA1·x⃗≥b⃗⋀∑i=1nxi′≥K. This implies that there exists x′⃗∈P1, with ∑i=1nxi′≥K, that is, -∑i=1nxi′≤-K. Thus, -∑i=1nxi′<(-K+1), and hence -∑i=1nxi′<-(K-1). It follows that x⃗′∈P1 is not contained in P2, and hence the instance of IHI-Horn is false.
The theorem follows.Table3 summarizes the discussion on Integer hull inclusion problems.Table 3
Complexities of Integer hull inclusion problems over various polyhedral families.
Polyhedral systemHull inclusionDiffP2SATPTUMPHorncoNP-complete


## 8. Conclusion

In this paper, we discussed clausal equivalence and hull inclusion (both linear and integer) from the perspectives of a number of specialized constraint clauses. We also detailed the complexities of some satisfiability variants. Finally, we showed that the Integer hull inclusion problem for Horn polytopes iscoNP-complete. To the best of our knowledge, our results are the first of their kind.The work in this paper is important from the orthogonal perspectives of providing efficient strategies for special cases of hard problems and exposing interesting avenues for future research. The following interesting open problems have arisen from this work.(i)
While the satisfiability of a Horn clause system can be checked by resolution inO(n2) time, to date, the only known strategy for checking the feasibility of a general Horn polytope is linear programming [37]. Finding a simpler strategy for Horn polytope feasibility is of paramount importance since Horn polytopes find wide application in engineering domains.(ii)
Although the IHI-Horn problem iscoNP-complete, the complexity of the problem, when the number of nonzero variables defining each constraint is a fixed constant, is unknown. A polynomial time algorithm for this problem is of enormous practical significance.



---

*Source: 845804-2009-07-20.xml*