On deciding the non-emptiness of 2SAT polytopes with respect to First Order Queries

Abstract

This paper is concerned with techniques for identifying simple and quantified lattice points in 2SAT polytopes. 2SAT polytopes generalize the polyhedra corresponding to Boolean 2SAT formulas, Vertex-Packing (Covering, Partitioning) and Network flow problems; they find wide application in the domains of Program verification (Software Engineering) and State-Space search (Artificial Intelligence). Our techniques are based on the symbolic elimination strategy called the Fourier-Motzkin elimination procedure and thus have the advantages of being extremely simple (from an implementational perspective) and incremental. We also provide a characterization of a 2SAT polytope in terms of its extreme points and derive some interesting hardness results for associated optimization problems. Finally, we provide a brief discussion on the maximum size of a subdeterminant of the linear system representing a 2SAT polytope; this parameter plays a vital role in deriving analytical bounds on the size of the search space for checking whether the polyhedron includes a lattice point.