On deciding the non-emptiness of 2SAT polytopes with respect to first order queries. (English) Zbl 1073.68081

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


68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
90C27 Combinatorial optimization
Full Text: DOI