Some characteristics of the simple Boolean quadric polytope extension

TL;DR

This paper extends the Boolean quadric polytope to the SATP polytope, analyzing its properties, vertices, and implications for solving various SAT-related problems through integer recognition.

Contribution

It introduces the SATP polytope extension, characterizes its vertices, explores its properties, and applies these findings to solve SAT variants and graph coloring problems.

Findings

SATP_{LP} has the Trubin-property and is quasi-integral.

Vertices of SATP have denominators with any integral value.

Polynomially solvable subproblems for integer recognition over SATP_{LP} are identified.

Abstract

Following the seminal work of Padberg on the Boolean quadric polytope $BQP$ and its LP relaxation $BQP_{LP}$, we consider a natural extension: $SATP$ and $SATP_{LP}$ polytopes, with $BQP_{LP}$ being projection of the $SATP_{LP}$ face (and $BQP$ -- projection of the $SATP$ face). We consider a problem of integer recognition: determine whether a maximum of a linear objective function is achieved at an integral vertex of a polytope. Various special instances of 3-SAT problem like NAE-3-SAT, 1-in-3-SAT, weighted MAX-3-SAT, and others can be solved by integer recognition over $SATP_{LP}$. We describe all integral vertices of $SATP_{LP}$. Like $BQP_{LP}$, polytope $SATP_{LP}$ has the Trubin-property being quasi-integral (1-skeleton of $SATP$ is a subset of 1-skeleton of $SATP_{LP}$). However, unlike $BQP$, not all vertices of $SATP$ are pairwise adjacent, the diameter of $SATP$ equals 2, and the clique number of 1-skeleton is superpolynomial in dimension. It is known that the fractional vertices of $BQP_{LP}$ are half-integer (0, 1 or 1/2 valued). We show that the denominators of $SATP_{LP}$ fractional vertices can take any integral value. Finally, we describe polynomially solvable subproblems of integer recognition over $SATP_{LP}$ with constrained objective functions. Based on that, we solve some cases of edge constrained bipartite graph coloring.