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