<p><em>EDIT: Strengthened Theorem 2.</em></p>
<p>The answer to the problem as posed is no, unless P=NP:</p>
<p><strong>Theorem 1.</strong> <em>Unless P=NP, there is no LP polytope for Horn-SAT that has only integer extreme points and is optimizable in polynomial time.</em></p>
<p>On the other hand, the natural polytope <span class="math-container">$P$</span> given in the post still suffices to solve Horn-SAT via linear programming, as the solution to the LP <span class="math-container">$\min\{\sum_v x_v : x\in P\}$</span> will correspond to a (minimal) satisfying assignment for the given formula <span class="math-container">$\phi$</span>, as long as <span class="math-container">$\phi$</span> is satisfiable.</p>
<p><strong>Theorem 2.</strong> <em>For any Horn formula <span class="math-container">$\phi$</span>, the corresponding polytope <span class="math-container">$P$</span> (as defined by the constraints in the post) is feasible iff <span class="math-container">$\phi$</span> is satisfiable, and the solution to <span class="math-container">$\arg\min\{ \sum_v x'_v : x\in P\}$</span> (if it exists) is a satisfying assignment to <span class="math-container">$\phi$</span>.</em></p>
<p>[Caveats: by an &quot;<em>LP polytope for Horn-SAT</em>&quot;, I mean a polytope with at least the following properties: given a Horn formula <span class="math-container">$\phi$</span>, a representation of the corresponding polytope can be constructed in polynomial time, and it has a 0/1 variable <span class="math-container">$x'_i$</span> for each Boolean variable <span class="math-container">$x_i$</span> in <span class="math-container">$\phi$</span>, and the feasible integer solutions <span class="math-container">$x'$</span> to the LP correspond to the satisfying assignments to <span class="math-container">$x$</span> (setting each <span class="math-container">$x_i$</span> True if <span class="math-container">$x'_i=1$</span> and False otherwise).  By &quot;<em>optimizable in polynomial time</em>&quot;, I mean that, if we extend this polytope to a full LP by adding any linear objective function, the resulting LP is solvable in polynomial time.]</p>
<p><em>Proof of Theorem 1.</em> Suppose that there is such a linear program.  Then Max Independent Set can be solved in polynomial time as follows.  Given an instance <span class="math-container">$G=(V,E)$</span> of Max Independent Set:</p>
<ol>
<li><p>construct a Horn formula <span class="math-container">$\phi$</span> with a variable <span class="math-container">$x_v$</span> for every vertex <span class="math-container">$v\in V$</span>, and a clause <span class="math-container">$(\neg x_v \vee \neg x_u)$</span> for each edge <span class="math-container">$(u, v)\in E$</span></p>
</li>
<li><p>construct the LP polytope for <span class="math-container">$\phi$</span>, then obtain a full LP by adding objective function <em>maximize</em> <span class="math-container">$\sum_v x'_v$</span></p>
</li>
<li><p>solve the LP using standard techniques to obtain an optimal extreme point <span class="math-container">$x^*$</span></p>
</li>
<li><p>return the corresponding vertex set <span class="math-container">$I=\{v\in V : x^*_v = 1\}$</span></p>
</li>
</ol>
<p><span class="math-container">$I$</span> is an independent set by our assumption that extreme points of the polytope correspond to satisfying assignments to <span class="math-container">$\phi$</span> (and by construction of <span class="math-container">$\phi$</span> satisfying assignments for <span class="math-container">$\phi$</span> correspond to independent sets).</p>
<p>Given any independent set <span class="math-container">$I'$</span>, there exists (by definition of <span class="math-container">$\phi$</span>) a corresponding solution to <span class="math-container">$\phi$</span>, and therefore a corresponding solution <span class="math-container">$x'$</span> to the LP (with <span class="math-container">$x'_v = 1$</span> iff <span class="math-container">$v\in I'$</span>), with objective function <span class="math-container">$\sum_v x'_v = |I'|$</span>.  Hence the size of <span class="math-container">$I$</span> is <span class="math-container">$\sum_v x^*_v \ge \sum_v x'_v = |I'|$</span>.  So <span class="math-container">$I$</span> has maximum size. <span class="math-container">$~~~\Box$</span></p>
<p><em>Proof of Theorem 2.</em> Recall <a href="https://en.wikipedia.org/wiki/Horn-satisfiability" rel="nofollow noreferrer">the standard linear-time algorithm for solving Horn-SAT</a>:</p>
<ol>
<li><p>while the formula <span class="math-container">$\phi$</span> contains any clause consisting of a single positive literal <span class="math-container">$x_i$</span>:</p>
</li>
<li><p><span class="math-container">$~~~~$</span>set <span class="math-container">$x_i$</span> true (remove all clauses containing <span class="math-container">$x_i$</span>, and remove <span class="math-container">$\neg x_i$</span> from all clauses that contain <span class="math-container">$\neg x_i$</span>)</p>
</li>
<li><p>if the resulting formula contains any empty clause, return &quot;not satisfiable&quot;</p>
</li>
<li><p>otherwise, set all remaining variables to false</p>
</li>
</ol>
<p>In the first step, any satisfying assignment must have <span class="math-container">$x_i$</span> true, so forcing <span class="math-container">$x_i$</span> true does not change the set of satisfying assignments.
If Step 3 executes, the set of satisfying assignments must be empty, so the (original) formula is not satisfiable.
If Step 4 executes, it satisfies all remaining clauses (as each must contain a negated variable), so generates a satisfying assignment.</p>
<p>To prove the theorem, note that the algorithm and the proof of correctness extend directly to the problem of finding a solution to the polytope <span class="math-container">$P$</span> defined by the constraints described in the post.  Namely, if there is a &quot;clause&quot; constraint <span class="math-container">$x_i \ge 1$</span>, then every point <span class="math-container">$x\in P$</span> must have <span class="math-container">$x_i=1$</span>, so forcing <span class="math-container">$x_i=1$</span> (and adjusting the remaining constraints accordingly) does not reduce the feasible set.  And if there is (in Step 3) an &quot;empty clause&quot;, the corresponding constraint will be <span class="math-container">$0 \ge 1$</span>, so the (original) polytope must be infeasible.  And otherwise (in Step 4) setting <span class="math-container">$x_i=0$</span> for all remaining variables will satisfy all remaining clause constraints.</p>
<p>(We are using here that when we force <span class="math-container">$x_i=1$</span> and simplify, the resulting set of constraints is exactly the set of constraints that corresponds to the Horn formula obtained by setting <span class="math-container">$x_i$</span> true in formula <span class="math-container">$\phi$</span>, and then simplifying as described.)</p>
<p>Finally, by the above reasoning, if the given formula <span class="math-container">$\phi$</span> is satisfiable, then the algorithm returns the 0/1 point <span class="math-container">$x^*$</span> such that, if <span class="math-container">$x^*_v = 1$</span>, then <span class="math-container">$x'_v = 1$</span> in every feasible point <span class="math-container">$x'\in P$</span>. Consequently, <span class="math-container">$x^*$</span> is the  feasible point that (uniquely) minimizes <span class="math-container">$\sum_v x'_v$</span>.  It follows that the solution to the LP <span class="math-container">$\min\{ \sum_v x'_v : x' \in P\}$</span> will be <span class="math-container">$x^*$</span>.  <span class="math-container">$~~~\Box$</span></p>

CC BY-SA 4.0
2021-09-13T22:13:38.950Z
Neal, Thank you.. May I add that $~\land_{(i,j) \in E} (\neg x_i \lor \neg x_j)~$ falls in 3 subclasses of SAT -- HornSAT, 2-SAT and Neg-SAT (where all literals are negative).. These 3 subclasses are among the well-known "Schaefer 6" from 1978.. Thomas Schaefer (a student of Richard Karp then) showed that unless P=NP, **only** 6 subclasses of SAT are polynomially solvable.. 2SAT, of course, is complete for the class NL.. Will update the references.
Shuxue Jiaoshou
CC BY-SA 4.0
2021-09-14T15:00:31.283Z
@ShuxueJiaoshou, FYI I strengthened Theorem 2 to point out that one can solve Horn SAT by solving the LP $\min\{\sum_v x'_v : x'\in P\}$ for your polytope $P$.
Neal Young
CC BY-SA 4.0
2021-09-14T21:25:14.933Z
Neal, Exactly.. The uniqueness follows from the intersection property of Horn solution sets.. Example -- If $\{ x_1, ~x_2, ~x_3, ~x_4 \}$ and $\{ x_3, ~x_4, x_5 \}$ are two sets of feasible solutions to an instance of HornSAT, then their intersection $\{x_3, ~x_4\}$ is also a feasible solution for that instance.. So we can keep doing intersections which will lead us to a *unique* minimum-size solution set.
Shuxue Jiaoshou
CC BY-SA 4.0
2021-10-05T07:19:31.207Z
Just a quick note: There is literature on the stable set (independent set) polytope or polyhedra going back more than 30 years.
Shuxue Jiaoshou
CC BY-SA 4.0
2021-09-13T16:10:32.843Z
2021-09-14T19:44:00.470Z
2021-09-14T19:44:00.470Z
Neal Young
<p>In some ways, my question is related to this: <a href="https://cstheory.stackexchange.com/questions/47252/is-the-matching-polytope-integral">Is the matching polytope integral?</a></p>
<p>Matching and Horn-SAT are both polynomial time solvable.. So I wonder if there is a Horn polytope, similar to the Matching Polytope?</p>
<p>The &quot;generic&quot; set of constraints for Horn-SAT results in a solution space (polyhedron), where some of the extreme points may <strong>not</strong> be integral.. For example, consider the Horn formula:</p>
<p><span class="math-container">$(x_1 \lor \neg x_2 \lor \neg x_3)  \land  (x_2)  \land  (\neg x_1 \lor  \neg x_3)$</span>.</p>
<p>The <strong>LP relaxation</strong> of the corresponding Integer Program is as follows:</p>
<p><span class="math-container">$-x_1 + x_2 + x_3 \leq 1, ~~
x_2 \geq 1, ~~ 
x_1 + x_3 \le 1~$</span> and
<span class="math-container">$~0 \le x_1,~ x_2,~ x_3 \leq 1$</span>.</p>
<p>The polyderon (solution space) of the above LP has one <strong>non</strong>-integer extreme
point, which is (0.5,  1,  0.5).</p>
<p>I would like to know -- is it possible to add inequalities to Linear
Programs such as the above (for Horn formulas), so that the modified
LP's have <strong>all</strong> Integer extreme points?  And thus obtain a Horn
polytope?</p>
<p>Matching and Horn-SAT are both polynomial time solvable.. So I imagine
that similar to Matching, we should be able to obtain a Horn polytope
by adding inequalities.. Are there any results along these lines?</p>
<p>I realise that Horn-SAT can be solved in polynomial time using algorithms
such as Unit Propagation.. But it will be nice to know whether we can
obtain a Horn polytope where all extreme points have integer
components (and hence can be solved using LP algorithms such as the Interior Point method).</p>
<p>References: <br />
[1] Chapter 25 of <em>Alexander Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer 2004</em>. <br />
[2] Chapter 9 of <em>Lap-Chi Lau, R. Ravi and Mohit Singh, Iterative Methods in Combinatorial Optimization, Cambridge University Press, 2011</em>. <br />
[3] Thomas J. Schaefer, <em>The Complexity of Satisﬁability Problems</em>, Proceedings of
the Tenth Annual ACM Symposium on the Theory of Computing (STOC), San Diego, Calif.,
pp. 216–226. ACM (1978)</p>

CC BY-SA 4.0
2021-09-12T22:27:14.763Z
Are these inter point methods etc. highly parallelizable? If yes, then it would suggest that Horn-Sat does not have integral polytope , since it is P-complete i.e. it is believed that it is not efficiently solavable with paraller computing (in other words the problem is not believed to be in the complexity class NC). Note that finding maximal matchings is in NC.
Reijo Jaakkola
CC BY-SA 4.0
2021-09-13T00:42:29.397Z
That's right, HornSAT is P-complete.. And from what I know, NC = P is unlikely.. Not sure about the parallelisation of LP algorithms; have to check.
Shuxue Jiaoshou
CC BY-SA 4.0
2021-09-13T07:30:01.627Z
Linear programming is P-complete as well, so it isn’t parallelizable any more than Horn-SAT.
Emil Jeřábek
CC BY-SA 4.0
2021-09-13T10:38:49.717Z
For Matching, Edmonds developed a set of inequalities, which if added to the relaxed LP, provides an integral polytope.. If the original LP (like the one posted above) returns an integer optimal solution, then we are done.. Otherwise, we should find one of those Edmonds' inequalities, add them to the LP and solve it again.. A polynomial time "separation algorithm" to determine such an inequality for Matching was developed by Padberg and Rao.. We need to find out if something similar has been (or can be) developed for Horn-SAT.
Shuxue Jiaoshou
<cc.complexity-theory><co.combinatorics><sat><matching><polytope>
Does Horn SAT (Horn formula in CNF) have an integral polytope?
Shuxue Jiaoshou
# Does Horn SAT (Horn formula in CNF) have an integral polytope?

(Asked by: username_0 on 2021-09-12)

In some ways, my question is related to this: [Is the matching polytope integral?](https://cstheory.stackexchange.com/questions/47252/is-the-matching-polytope-integral)

Matching and Horn-SAT are both polynomial time solvable.. So I wonder if there is a Horn polytope, similar to the Matching Polytope?

The "generic" set of constraints for Horn-SAT results in a solution space (polyhedron), where some of the extreme points may **not** be integral.. For example, consider the Horn formula:

$(x\_1 \lor \neg x\_2 \lor \neg x\_3) \land (x\_2) \land (\neg x\_1 \lor \neg x\_3)$.

The **LP relaxation** of the corresponding Integer Program is as follows:

$-x\_1 + x\_2 + x\_3 \leq 1, ~~
x\_2 \geq 1, ~~
x\_1 + x\_3 \le 1~$ and
$~0 \le x\_1,~ x\_2,~ x\_3 \leq 1$.

The polyderon (solution space) of the above LP has one **non**-integer extreme
point, which is (0.5, 1, 0.5).

I would like to know -- is it possible to add inequalities to Linear
Programs such as the above (for Horn formulas), so that the modified
LP's have **all** Integer extreme points? And thus obtain a Horn
polytope?

Matching and Horn-SAT are both polynomial time solvable.. So I imagine
that similar to Matching, we should be able to obtain a Horn polytope
by adding inequalities.. Are there any results along these lines?

I realise that Horn-SAT can be solved in polynomial time using algorithms
such as Unit Propagation.. But it will be nice to know whether we can
obtain a Horn polytope where all extreme points have integer
components (and hence can be solved using LP algorithms such as the Interior Point method).

References:   
[1] Chapter 25 of *Alexander Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer 2004*.   
[2] Chapter 9 of *Lap-Chi Lau, R. Ravi and Mohit Singh, Iterative Methods in Combinatorial Optimization, Cambridge University Press, 2011*.   
[3] Thomas J. Schaefer, *The Complexity of Satisﬁability Problems*, Proceedings of
the Tenth Annual ACM Symposium on the Theory of Computing (STOC), San Diego, Calif.,
pp. 216–226. ACM (1978)

**Tags:** cc.complexity-theory, co.combinatorics, sat, matching, polytope

> **Comments:**
> **username_1**: Are these inter point methods etc. highly parallelizable? If yes, then it would suggest that Horn-Sat does not have integral polytope , since it is P-complete i.e. it is believed that it is not efficiently solavable with paraller computing (in other words the problem is not believed to be in the complexity class NC). Note that finding maximal matchings is in NC.  
> **username_0**: That's right, HornSAT is P-complete.. And from what I know, NC = P is unlikely.. Not sure about the parallelisation of LP algorithms; have to check.  
> **username_2**: Linear programming is P-complete as well, so it isn’t parallelizable any more than Horn-SAT.  
> **username_0**: For Matching, Edmonds developed a set of inequalities, which if added to the relaxed LP, provides an integral polytope.. If the original LP (like the one posted above) returns an integer optimal solution, then we are done.. Otherwise, we should find one of those Edmonds' inequalities, add them to the LP and solve it again.. A polynomial time "separation algorithm" to determine such an inequality for Matching was developed by Padberg and Rao.. We need to find out if something similar has been (or can be) developed for Horn-SAT.  

---

## 1 answers

### Answer by username_3 on 2021-09-13. Score: 7 | Accepted answer

*EDIT: Strengthened Theorem 2.*

The answer to the problem as posed is no, unless P=NP:

**Theorem 1.** *Unless P=NP, there is no LP polytope for Horn-SAT that has only integer extreme points and is optimizable in polynomial time.*

On the other hand, the natural polytope $P$ given in the post still suffices to solve Horn-SAT via linear programming, as the solution to the LP $\min\{\sum\_v x\_v : x\in P\}$ will correspond to a (minimal) satisfying assignment for the given formula $\phi$, as long as $\phi$ is satisfiable.

**Theorem 2.** *For any Horn formula $\phi$, the corresponding polytope $P$ (as defined by the constraints in the post) is feasible iff $\phi$ is satisfiable, and the solution to $\arg\min\{ \sum\_v x'\_v : x\in P\}$ (if it exists) is a satisfying assignment to $\phi$.*

[Caveats: by an "*LP polytope for Horn-SAT*", I mean a polytope with at least the following properties: given a Horn formula $\phi$, a representation of the corresponding polytope can be constructed in polynomial time, and it has a 0/1 variable $x'\_i$ for each Boolean variable $x\_i$ in $\phi$, and the feasible integer solutions $x'$ to the LP correspond to the satisfying assignments to $x$ (setting each $x\_i$ True if $x'\_i=1$ and False otherwise). By "*optimizable in polynomial time*", I mean that, if we extend this polytope to a full LP by adding any linear objective function, the resulting LP is solvable in polynomial time.]

*Proof of Theorem 1.* Suppose that there is such a linear program. Then Max Independent Set can be solved in polynomial time as follows. Given an instance $G=(V,E)$ of Max Independent Set:

1. construct a Horn formula $\phi$ with a variable $x\_v$ for every vertex $v\in V$, and a clause $(\neg x\_v \vee \neg x\_u)$ for each edge $(u, v)\in E$
2. construct the LP polytope for $\phi$, then obtain a full LP by adding objective function *maximize* $\sum\_v x'\_v$
3. solve the LP using standard techniques to obtain an optimal extreme point $x^\*$
4. return the corresponding vertex set $I=\{v\in V : x^\*\_v = 1\}$

$I$ is an independent set by our assumption that extreme points of the polytope correspond to satisfying assignments to $\phi$ (and by construction of $\phi$ satisfying assignments for $\phi$ correspond to independent sets).

Given any independent set $I'$, there exists (by definition of $\phi$) a corresponding solution to $\phi$, and therefore a corresponding solution $x'$ to the LP (with $x'\_v = 1$ iff $v\in I'$), with objective function $\sum\_v x'\_v = |I'|$. Hence the size of $I$ is $\sum\_v x^\*\_v \ge \sum\_v x'\_v = |I'|$. So $I$ has maximum size. $~~~\Box$

*Proof of Theorem 2.* Recall [the standard linear-time algorithm for solving Horn-SAT](https://en.wikipedia.org/wiki/Horn-satisfiability):

1. while the formula $\phi$ contains any clause consisting of a single positive literal $x\_i$:
2. $~~~~$set $x\_i$ true (remove all clauses containing $x\_i$, and remove $\neg x\_i$ from all clauses that contain $\neg x\_i$)
3. if the resulting formula contains any empty clause, return "not satisfiable"
4. otherwise, set all remaining variables to false

In the first step, any satisfying assignment must have $x\_i$ true, so forcing $x\_i$ true does not change the set of satisfying assignments.
If Step 3 executes, the set of satisfying assignments must be empty, so the (original) formula is not satisfiable.
If Step 4 executes, it satisfies all remaining clauses (as each must contain a negated variable), so generates a satisfying assignment.

To prove the theorem, note that the algorithm and the proof of correctness extend directly to the problem of finding a solution to the polytope $P$ defined by the constraints described in the post. Namely, if there is a "clause" constraint $x\_i \ge 1$, then every point $x\in P$ must have $x\_i=1$, so forcing $x\_i=1$ (and adjusting the remaining constraints accordingly) does not reduce the feasible set. And if there is (in Step 3) an "empty clause", the corresponding constraint will be $0 \ge 1$, so the (original) polytope must be infeasible. And otherwise (in Step 4) setting $x\_i=0$ for all remaining variables will satisfy all remaining clause constraints.

(We are using here that when we force $x\_i=1$ and simplify, the resulting set of constraints is exactly the set of constraints that corresponds to the Horn formula obtained by setting $x\_i$ true in formula $\phi$, and then simplifying as described.)

Finally, by the above reasoning, if the given formula $\phi$ is satisfiable, then the algorithm returns the 0/1 point $x^\*$ such that, if $x^\*\_v = 1$, then $x'\_v = 1$ in every feasible point $x'\in P$. Consequently, $x^\*$ is the feasible point that (uniquely) minimizes $\sum\_v x'\_v$. It follows that the solution to the LP $\min\{ \sum\_v x'\_v : x' \in P\}$ will be $x^\*$. $~~~\Box$

> **Comments:**
> **username_0**: Neal, Thank you.. May I add that $~\land_{(i,j) \in E} (\neg x_i \lor \neg x_j)~$ falls in 3 subclasses of SAT -- HornSAT, 2-SAT and Neg-SAT (where all literals are negative).. These 3 subclasses are among the well-known "Schaefer 6" from 1978.. Thomas Schaefer (a student of Richard Karp then) showed that unless P=NP, **only** 6 subclasses of SAT are polynomially solvable.. 2SAT, of course, is complete for the class NL.. Will update the references.  
> **username_3**: @ShuxueJiaoshou, FYI I strengthened Theorem 2 to point out that one can solve Horn SAT by solving the LP $\min\{\sum_v x'_v : x'\in P\}$ for your polytope $P$.  
> **username_0**: Neal, Exactly.. The uniqueness follows from the intersection property of Horn solution sets.. Example -- If $\{ x_1, ~x_2, ~x_3, ~x_4 \}$ and $\{ x_3, ~x_4, x_5 \}$ are two sets of feasible solutions to an instance of HornSAT, then their intersection $\{x_3, ~x_4\}$ is also a feasible solution for that instance.. So we can keep doing intersections which will lead us to a *unique* minimum-size solution set.  
> **username_0**: Just a quick note: There is literature on the stable set (independent set) polytope or polyhedra going back more than 30 years.  

---

