MaxSAT Resolution and Subcube Sums

TL;DR

This paper introduces the SubCubeSums proof system, demonstrating its power and limitations in certifying unsatisfiability, and compares it to existing proof systems like MaxResW and resolution.

Contribution

It defines the SubCubeSums proof system, shows its relation to MaxResW and Sherali-Adams, and establishes new lower bounds for refuting certain formulas.

Findings

SubCubeSums p-simulates MaxResW.

Tseitin contradictions on expanders are hard in SubCubeSums.

Lifting techniques show large XOR-ification requires large SubCubeSums proofs.

Abstract

We study the MaxRes rule in the context of certifying unsatisfiability. We show that it can be exponentially more powerful than tree-like resolution, and when augmented with weakening (the system MaxResW), p-simulates tree-like resolution. In devising a lower bound technique specific to MaxRes (and not merely inheriting lower bounds from Res), we define a new proof system called the SubCubeSums proof system. This system, which p-simulates MaxResW, can be viewed as a special case of the semialgebraic Sherali-Adams proof system. In expressivity, it is the integral restriction of conical juntas studied in the contexts of communication complexity and extension complexity. We show that it is not simulated by Res. Using a proof technique qualitatively different from the lower bounds that MaxResW inherits from Res, we show that Tseitin contradictions on expander graphs are hard to refute in SubCubeSums. We also establish a lower bound technique via lifting: for formulas requiring large degree in SubCubeSums, their XOR-ification requires large size in SubCubeSums.