Compact linear programs for 2SAT

TL;DR

This paper introduces a compact linear program with polynomial size that efficiently determines the satisfiability of any 2SAT formula, contrasting with the superpolynomial complexity of the natural polytope, using multicommodity flows.

Contribution

It provides an explicit polynomial-size linear program for 2SAT satisfiability, leveraging multicommodity flows, which is a significant improvement over the natural polytope's complexity.

Findings

Linear program with O(n^3) size determines 2SAT satisfiability

Contrasts with superpolynomial extension complexity of the natural polytope

Connections established to the stable matching problem

Abstract

For each integer $n$ we present an explicit formulation of a compact linear program, with $O(n^3)$ variables and constraints, which determines the satisfiability of any 2SAT formula with $n$ boolean variables by a single linear optimization. This contrasts with the fact that the natural polytope for this problem, formed from the convex hull of all satisfiable formulas and their satisfying assignments, has superpolynomial extension complexity. Our formulation is based on multicommodity flows. We also discuss connections of these results to the stable matching problem.

Equations

$$Q_n=\mathrm{CH}\{(y^{\varphi },x):\forall x,\varphi s.t.xisasatisfyingassignmentof\varphi \}$$

$$\begin{array}[]{rclr}\delta_{i,k}f^{i}_{t_{i}x_{i}}+\displaystyle\sum_{i\neq j}f^{k}_{x_{j}x_{i}}&=&\displaystyle\sum_{i\neq j}f^{k}_{x_{i}x_{j}}+\delta_{n+i,k}f^{n+i}_{t_{n+i}x_{n+i}}&i,k=1,\cdots,2n\\ P_{n}:~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}0~{}\leqslant~{}f^{i}_{t_{i}x_{i}}&\leqslant&1&i=1,\cdots,2n\\ f^{k}_{x_{i}x_{j}}&\geqslant&0&~{}i,j,k=1,\cdots,2n,\\ &&&i\neq j\end{array}$$

$$z^{\ast }=\max \sum _{i=1}^{2n}{f}_{t_i{x}_i}^i-(2n+1)\sum _{\begin{array}{c}(x_i\vee x_j)\notin \varphi \\ 1⩽k⩽2n\end{array}}(f_{x_{n+i}{x}_j}^k+f_{x_{n+j}{x}_i}^k)$$

$$f\in P_n$$

$$R_{2n}=\mathrm{CH}\{(y^{\psi },x):\forall x,\psi s.t.xisastablematchingfor\psi \}$$

Full text

11footnotetext: GERAD and School of Computer Science, McGill University, 3480 University Street, Montréal, Québec, Canada H3A 2A7.22footnotetext: Graduate School of Informatics, Kyoto University, Sakyo-ku, Yoshida Yoshida, Kyoto 606-8501, Japan.33footnotetext: Department of Applied Mathematics (KAM) and Institute of Theoretical Computer Science (ITI), Charles University, Malostranské nám. 25, 118 00 Prague 1, Czech Republic.

Keywords: 2SAT, multicommodity flows, extension complexity, stable matchings

1 Introduction

Let $n$ be a positive integer and let $x_{1},...,x_{n},\bar{x_{1}},...,\bar{x_{n}}$ be a corresponding set of $2n$ boolean valued literals. An input for the 2SAT problem is a formula $\phi$ representing the conjunctive normal form of a collection of $m$ clauses each of which contains two literals. The formula is satisfiable if an assignment of truth values to $x_{1},...,x_{n}$ makes at least one literal in each clause true. The 2SAT problem can be solved optimally in $O(n+m)$ time by an algorithm due to Aspvall et al. [1] based on path-finding. Let $w_{1},...,w_{n}$ be a set of $n$ integer weights. The problem of finding a satisfying assignment of maximum weight is known as the weighted 2SAT problem. It is NP-hard since it contains the maximum independent set problem for graphs as a special case. In the main part of this note we are concerned with polyhedra related to the unweighted 2SAT problem.

Consider solving unweighted 2SAT for a formula $\phi$ by using a linear program of the form $max~{}c^{T}y:Ay\leq b$ of small size. More formally we call such a formulation compact if: (a) the dimensions of $A$ are polynomially bounded in $n$, (b) there is an $O(log~{}n)$-space algorithm which constructs an objective function $c=c_{\phi}$ from formula $\phi$, and (c) there is an $O(log~{}n)$-space algorithm that takes the solution to $max~{}c_{\phi}^{T}y:Ay\leq b$ and decides whether or not $\phi$ is satisfiable.

In [3] the authors showed that a natural LP formulation for 2SAT has superpolynomial extension complexity. Recently this lower bound was improved by Göös to $2^{\Omega(n/\log{n})}$ where $n$ is the size of the 2SAT formula [7]. This implies that there is no polyhedron of polynomial size that projects onto this polyhedron. However, since the unweighted 2SAT problem is in $P$ and linear programming is $P$-complete, compact LPs for it must exist. In fact, in Avis et al. [2] a direct method is given to produce a compact LP from a polynomial time algorithm. Applied to the algorithm of [1] this produces an LP with $O(n^{4}log~{}n)$ constraints. The LP formulation is not explicit but is produced by a compiler111https://gitlab.com/sparktope/sparktope which transforms an implementation of the given algorithm in a simple programming language. In the next section we give an explicit compact LP for 2SAT with $O(n^{3})$ constraints and variables which is based on multicommodity flows. In Section 3 we discussion connections with the stable matching problem and give some open problems.

2 2SAT

Let $\phi$ be an instance of 2SAT with $n$ variables. We may assume that there is no clause of the form $x_{i}\vee\bar{x_{i}}$, since this is always satisfied. Therefore there are at most $2n^{2}-n$ distinct clauses which we may label, say lexicographically, $C_{1},...,C_{2n^{2}-n}$. The formula $\phi$ may be expressed by a 0/1 vector $y^{\phi}$ of length $2n^{2}-n$ by setting $y_{i}^{\phi}=1$ if and only if $C_{i}\in\phi$. Let $x$ denote a 0/1 vector of length $n$ and ${\mathbbm{1}}$ denote the vector of all ones, where the length is defined by the context. A natural polytope for 2SAT can be defined in $2n^{2}$ dimensions by

[TABLE]

which is the convex hull of all satisfiable formulae with their satisfying assignments.

Proposition 1**.**

Give a 2SAT formula $\phi$ we can solve either the unweighted or weighted satisfiability program by solving a single LP over $Q_{n}$, which has superpolynomial extension complexity.

Proof.

Let $\phi$ be a 2SAT formula and first consider the unweighted satisfiability problem. Define a vector $c$ of length $2n^{2}-n$ by setting $c_{i}=1$ if $y_{i}^{\phi}=1$ and $c_{i}=-1$ otherwise. Consider $z^{*}=\{max~{}c^{T}y:(y,x)\in Q_{n}\}$ and let $(y^{*},x^{*})$ be an optimal solution. It is easy to verify that $z^{*}={\mathbbm{1}}^{T}y^{\phi}$ if $\phi$ is satisfiable and $z^{*}\leq{\mathbbm{1}}^{T}y^{\phi}~{}-1$ otherwise.

For the weighted satisfiability problem, let $w=(w_{1},...,w_{n})$ be the vector of given integer weights and set $W=\sum_{i=1}^{n}|w_{i}|$. Consider $z^{*}=\{max~{}c^{T}y+\frac{1}{3W}w^{T}x:(y,x)\in Q_{n}\}$. If $\phi$ is unsatisfiable, then $z^{*}\leq{\mathbbm{1}}^{T}y^{\phi}-1+\frac{W}{3W}={\mathbbm{1}}^{T}y^{\phi}-\frac{2}{3}$. Otherwise $z^{*}\geq{\mathbbm{1}}^{T}y^{\phi}-\frac{W}{3W}={\mathbbm{1}}^{T}y^{\phi}-\frac{1}{3}$. So again inspecting the value of $z^{*}$ determines the satisfiability of $\phi$. Let $(y^{*},x^{*})$ be an optimum solution. When $\phi$ is satisfiable we must have $c^{T}y^{*}={\mathbbm{1}}^{T}y^{\phi}$ and $x^{*}$ must be a satisfying assignment of $\phi$. So the values of $x_{i}^{*}$ at optimality will give a maximum weight satisfying assignment.

Next we consider the extension complexity of $Q_{n}$. First observe that if we fix a 2SAT formula $\phi$ and restrict ourselves to the face where the first $2n^{2}-n$ coordinates are equal to $y^{\phi}$ we obtain a face of $Q_{n}$ that contains all satisfying assignments for $\phi$. It was shown in [3] that there is a family of 2SAT formulas $\phi_{n}$, indexed by the number of variables $n$, for which the set of satisfying assignments has superpolynomial extension complexity. Since the satisfying assignments for the formula $\phi_{n}$ correspond to a face of $Q_{n}$ this face has superpolynomial extension complexity. It follows that $Q_{n}$ does also. ∎

The proposition implies that a direct approach to solving 2SAT as a linear program over $Q_{n}$ will require exponentially many constraints. In what follows we give a completely different construction. It follows from the proposition that there will be no projection of this polytope onto $Q_{n}$.

In the sequel we define variables $x_{n+i}$ to denote the literals $\bar{x}_{i}$, for $i=1,...,n$. Subscripts should be taken $mod~{}2n$ and we usually omit this for clarity. For a given $n\geq 2$ consider the complete bidirected graph on $2n$ vertices labeled $x_{1},\ldots,x_{2n}$. We add vertices $t_{1},\ldots,t_{2n}$ and edges $(t_{i},x_{i}),(x_{i},t_{i}),(x_{n+i},t_{n+i}),$ and $(t_{n+i},x_{n+i})$ to the graph to obtain a graph with $4n$ vertices and $2n(2n-1)+4n=4n^{2}+2n$ edges. Call this graph $D_{n}$. We define a multicommodity flow problem with $2n$ commodities on $D_{n}$ as follows. For each $i=1,...,2n$, there are a pair of terminals $t_{i}$ and $t_{n+i}$ and a distinct flow, labeled flow $i$, between them. The capacity on edge $(t_{i},x_{i})$ is one and all other capacities are infinite. Therefore a unit flow from $t_{i}$ to $t_{n+i}$ saturates only the initial edge and corresponds to a path in $D_{n}$ between these two terminals. The sum of the maximum flows over all $2n$ commodities must therefore be at most $2n$ and this will be achieved if and only if there is a path between each of the $2n$ pairs of terminals. Now consider the following multicommodity flow polytope where $f_{ab}^{k}$ denotes the value of flow $k$ on edge $ab$ of $D_{n}$ and $\delta_{ij}=1$ if $i=j$ and zero otherwise.

[TABLE]

Let $f$ denote the ensemble of $2n\cdot 2n(2n-1)+4n=8n^{3}-4n^{2}+4n$ variables $\{f^{i}_{t_{i}x_{i}},f^{k}_{x_{i}x_{j}}\}$ ordered in any consistent way. The polytope $P_{n}$ has $8n^{3}-4n^{2}+6n$ inequalities and $4n^{2}$ equations. Note that the constraints consist of $2n$ disjoint copies of single commodity flow constraints and thus are totally unimodular. So in view of the upper and lower bound constraints the polytope has 0/1 vertices.

Let $\phi$ be a 2-SAT formula and suppose it contains the clause $x_{i}\lor x_{j}$ for some $i$ and $j$. This means that $\phi$ forces implications $\overline{x}_{i}\Rightarrow x_{j}$ and $\overline{x}_{j}\Rightarrow x_{i}$. In the graph $D_{n}$ these implications correspond to edges $x_{n+i},x_{j}$ and $x_{n+j},x_{i}$ respectively. For each such clause that is missing from $\phi$ these implications are missing also. We construct an implication graph $G_{n}$ from $D_{n}$ for $\phi$ by removing the corresponding edges for all missing clauses. In the flow setting, if clause $x_{i}\lor x_{j}$ is missing we set the variables $f^{k}_{x_{n+i}x_{j}}=f^{k}_{x_{n+j}x_{i}}=0$, $k=1,...,2n$. By so doing for each clause missing from $\phi$ we restrict ourselves to a face of $P_{n}$ which we denote $P^{\phi}_{n}$. A maximum commodity flow is a feasible vector in $P_{n}$ that maximizes $\sum_{i=1}^{2n}f^{i}_{t_{i}x_{i}}$.

Lemma 2**.**

Any maximum commodity flow lying on the face $P^{\phi}_{n}$ has $f^{i}_{t_{i}x_{i}}=f^{n+i}_{x_{n+i}t_{n+i}}=1$ for some $i$ if and only if the formula $\phi$ is unsatisfiable.

Proof.

If $f^{i}_{t_{i}x_{i}}=f^{n+i}_{x_{n+i}t_{n+i}}=1$, for some $i$, then these two flows imply paths from $x_{i}$ to $x_{n+i}$ and back. The first path gives a chain of implications implying that if $x_{i}$ is true then $x_{n+i}=\bar{x_{i}}$ is true, a contradiction. Similarly the second path gives implications showing that if $x_{i}$ false then it is true. Therefore the formula $\phi$ is unsatisfiable.

Conversely, if $\phi$ is unsatisfiable then there is a path from $x_{i}$ to $x_{n+i}$ and a path from $x_{n+i}$ to $x_{i}$. Thus a unit flow can be sent from $t_{i}$ to $t_{n+i}$ and from $t_{n+i}$ to $t_{i}$ and $f^{i}_{t_{i}x_{i}}=f^{n+i}_{x_{n+i}t_{n+i}}=1$. Since these two paths cannot use any edges corresponding to missing clauses in $\phi$, the corresponding flows lie on the face $P^{\phi}_{n}$. ∎

Testing the satisfiability of $\phi$ can be achieved by maximizing a suitably chosen linear objective function over $P_{n}$ designed so that all maximum solutions are found on the face $P^{\phi}_{n}$.

Theorem 3**.**

Let $\phi$ be a 2-SAT formula with $n$ variables. Consider the following LP:

[TABLE]

[TABLE]

Then, $\phi$ is unsatisfiable if and only if at optimality there is an $i$ such that $f^{i}_{t_{i}x_{i}}=f^{n+i}_{x_{n+i}t_{n+i}}=1$. A certificate for the satisfiability/unsatisfiability of $\phi$ can be obtained from the optimum solution.

Proof.

The LP is feasible, since this can be achieved by setting all variables to zero, and the objective function is upper bounded by $2n$. Therefore optimum solutions exist and $0\leq z^{*}\leq 2n$. We show that they lie on the face $P^{\phi}_{n}$. Consider any extreme point of $P_{n}$ that provides an optimum solution for the LP. As remarked above this is integral and is in fact 0/1 valued since $f^{i}_{t_{i}x_{i}}\leq 1,i=1,...,2n$. Suppose that $(x_{i}\lor x_{j})$ is a clause missing from $\phi$. For $k=1,...,2n$, if either of the variables $f^{k}_{x_{n+i}x_{j}}$ or $f^{k}_{x_{n+j}x_{i}}$ is set to one then this incurs a penalty of $-(2n+1)$ in the objective function. The rest of the objective function can only contribute $2n$ at most and so $z^{*}<0$, a contradiction. Therefore all optimum vertices, and hence all optimum solutions, occur on the face $P^{\phi}_{n}$. It now follows from Lemma 2 that the satisfiablility/unsatisfiability of $\phi$ can be determined from the optimum solution. The lemma gives a certificate of unsatisfiability. For a certificate of satisfiability we construct a satisfying assignment. For each $i$ such that $f^{i}_{t_{i}x_{i}}=1$ set $x_{n+i}=1$ and $x_{i}=0$. For each edge $x_{i},x_{j}$ with $x_{i}=1$ and $x_{j}$ unlabelled, set $x_{j}=1$ and $x_{n+j}=0$. Continuing in this way we label a set of strong components in $G_{n}$. If at termination there remain any unlabelled vertices $x_{i}$ we choose one arbitrarily, set $x_{i}=1$, $x_{n+i}=0$ and continue as before. Since no strong component can contain both $x_{i}$ and $x_{n+i}$ we have consistently labelled $G_{n}$ and have a satisfying assignment. ∎

Both the construction of the objective function and determining the (un)satisfiability of $\phi$ from the optimum solution can be done with $O(\log n)$ space. So the LP described in Theorem 3 is compact. As remarked earlier in this section this implies that it cannot be linearly projected onto $Q_{n}$ and, in particular, the satisfying assignment $x_{i}$ cannot be directly read from the optimum solution. Furthermore it apparently gives no insight into solving the weighted 2SAT problem.

3 Connections to stable matchings and open problems

From the point of view of extension complexity, 2SAT is an interesting problem since the unweighted version is in $P$ and the weighted version is NP-hard. Although the natural polyhedral formulation of 2SAT has high extension complexity we have shown that a compact explicit polyhedral formulation for the unweighted version exists. A problem of similar type is the stable matching problem, which has many variations and has received considerable attention since the seminal Gale-Shapley paper in 1962. For recent developments see Cseh and Manlove [4].

In the stable matching problem we have a group of $2n$ people each of who has a list ranking the other $2n-1$ people in order of preference. A matching is a set of $n$ pairs of people such that each person is in exactly one pair. An blocking pair is a set of 4 people $i,j,k,l$ such that $i$ is matched to $k$ but prefers $j$, and $j$ is matched to $l$ but prefers $i$. A matching is stable if it contains no blocking pair. A considerable amount of research has been done on this problem and computationally the 2SAT problem and stable matchings are closely related. Like 2SAT, there is a polynomial time algorithm for the problem (Irving [9]) and the weighted version is NP hard (Feder [5]).

From the polyhedral viewpoint we can define a polytope $R_{2n}$ for the stable matching which is analogous to $Q_{n}$ for 2SAT. Each instance $\psi$ for the stable matching problem consists of $2n$ permutations of $2n-1$ elements, each of which can be encoded as a $(2n-1)$ by $(2n-1)$ permutation matrix. Let the corresponding binary vector of length $2n(2n-1)^{2}$ be denoted $y^{\psi}$. A matching for $\psi$ can be encoded as binary vector $x$ of length $(2n-1)n$ where $x_{ij}=1$ if and only if $i$ and $j$ are matched, for $1\leq i<j\leq 2n$. We define $R_{2n}\subset{\mathbb{R}}^{n(2n-1)(4n-1)}$ by

[TABLE]

which is the convex hull of all stable matching problems with their stable matchings. Note that in the above we only consider instances $\psi$ which have stable matchings. Since the weighted stable matching problem can be solved by an LP over $R_{2n}$ we expect that it has high extension complexity, a fact we now prove.

Proposition 4**.**

$R_{2n}$* has superpolynomial extension complexity.*

Proof.

Theorem 8.2 of Feder [5] shows that a 2SAT formula with $n$ variables can be transformed to a stable matching problem with $4n$ people so that the set of solutions of the 2SAT problem correspond to the set of solutions of the stable matching problem. Proceeding as in Proposition 1 we make use of the family of 2SAT formulas $\phi_{n}$ from [3] that yield a family of faces of 2SAT polytopes that have superpolynomial extension complexity. Applying Feder’s transformation, each $\phi_{n}$ maps to an instance $\psi_{4n}$ of the stable matching problem whose stable matchings correspond to the satisfying assignments of $\phi_{n}$. If we now restrict ourselves to the face where the first $2n(2n-1)^{2}$ coordinates are $y^{\psi_{4n}}$ we obtain a face with all stable matchings of the instance $\psi_{4n}$. This is a face of $R_{4n}$ with superpolynomial extension complexity, and the proposition follows. ∎

It is natural to ask if, like the 2SAT problem, there is an explicit compact LP formulation for the unweighted problem. Indeed it is known that a stable matching problem with $2n$ people can be formulated as a 2SAT problem with $O(n^{2})$ variables and $O(n^{2})$ clauses. Algorithms for finding this formulation were given by Gusfield [8], and Feder [6] whose algorithm requires $O(n^{2})$ time and space. At first glance it may appear that we can use our compact formulation for 2SAT via this transformation of stable matching problems to 2SAT problems. Unfortunately this transformation cannot be performed using $O(log~{}n)$ space so condition (b) of a compact formulation, as defined in the Introduction, fails. So for the moment we must fall back on the method of [2] to obtain a compact formulation with $O(n^{4}~{}log~{}n)$ constraints.

A final open problem of this type concerns the perfect matching problem which Rothvoß proved also has superpolynomial extension complexity [11]. The method of [2] applied to the $O(n^{2.5})$ time and $O(n^{2})$ space implementation of Edmonds’ algorithm by Micali and Vazirani [10] yields an LP that has $O(n^{4.5}~{}log~{}n)$ constraints. It is therefore of great interest to see if this bound can be significantly improved, and if an explicit compact LP formulation for the perfect matching problem exists.

Acknowledgments

Research of the first author is supported by the JSPS under a Kakenhi grant and a Grant-in-Aid for Scientific Research on Innovative Areas, ‘Exploring the Limits of Computation (ELC)’. The second author was supported by project GA15-11559S of GA ČR.