The complexity of satisfaction problems in reverse mathematics

TL;DR

This paper classifies the complexity of satisfaction problems within reverse mathematics, showing they are either provable over RCA or equivalent to WKL, and explores a Ramseyan variant with an open question on class distinctions.

Contribution

It extends Schaefer's classification to the reverse mathematics framework and introduces a Ramseyan version with a new dichotomy theorem.

Findings

Satisfaction problems are either provable over RCA or equivalent to WKL.

A Ramseyan version of the problems exhibits a different dichotomy.

The classes from the Ramseyan classification are not yet proven to be distinct.

Abstract

Satisfiability problems play a central role in computer science and engineering as a general framework for studying the complexity of various problems. Schaefer proved in 1978 that truth satisfaction of propositional formulas given a language of relations is either NP-complete or tractable. We classify the corresponding satisfying assignment construction problems in the framework of reverse mathematics and show that the principles are either provable over RCA or equivalent to WKL. We formulate also a Ramseyan version of the problems and state a different dichotomy theorem. However, the different classes arising from this classification are not known to be distinct.