# 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.

## Key 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.