# Does Horn SAT (Horn formula in CNF) have an integral polytope?

In some ways, my question is related to this: 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:
 Chapter 25 of Alexander Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer 2004.
 Chapter 9 of Lap-Chi Lau, R. Ravi and Mohit Singh, Iterative Methods in Combinatorial Optimization, Cambridge University Press, 2011.
 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)

• 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. Sep 12 at 22:27
• 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. Sep 13 at 0:42
• Linear programming is P-complete as well, so it isn’t parallelizable any more than Horn-SAT. Sep 13 at 7:30
• 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. Sep 13 at 10:38

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:

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$$

• 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. Sep 13 at 22:13
• @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$. Sep 14 at 15:00
• 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. Sep 14 at 21:25
• Just a quick note: There is literature on the stable set (independent set) polytope or polyhedra going back more than 30 years. Oct 5 at 7:19