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

Subramani, K.

Math. Log. Q. 50, No. 3, 281-292 (2004).

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.

MSC:

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

Keywords:

2SAT polytope; first-order query; lattice point problem; quantified lattice point problem; NP-complete; PSPACE-complete