Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Polynomial Decision for 3-SAT

Angela Weiss

TL;DR

The work addresses the problem of deciding satisfiability for $3$-SAT by introducing Pivoted $3$-SAT and a polynomial-time, polynomial-space decision framework. It develops a graph-theoretic pipeline: transform a $3$-SAT instance into a pivoted form, construct a cylindrical digraph representation, and use expansions to closed digraphs while tracking compatible antichains. A key innovation is the Linearized Digraph, a polynomially manageable surrogate that preserves antichain structure, allowing a tractable search for all unsatisfiable combinations without exhaustive enumeration. The approach aims to enhance complexity-theoretic understanding and provide a new, resource-bounded avenue for SAT decision procedures through pivoted formulations and graph-based reasoning.

Abstract

We propose a polynomially bounded, in time and space, method to decide whether a given 3-SAT formula is satisfiable or not. The tools we use here are, in fact, very simple. We first decide satisfiability for a particular 3-SAT formula, called pivoted 3-SAT and, after a plain transformation, still keeping the polynomial boundaries, it is shown that 3-SAT formulas can be written as pivoted formulas.

A Polynomial Decision for 3-SAT

TL;DR

The work addresses the problem of deciding satisfiability for -SAT by introducing Pivoted -SAT and a polynomial-time, polynomial-space decision framework. It develops a graph-theoretic pipeline: transform a -SAT instance into a pivoted form, construct a cylindrical digraph representation, and use expansions to closed digraphs while tracking compatible antichains. A key innovation is the Linearized Digraph, a polynomially manageable surrogate that preserves antichain structure, allowing a tractable search for all unsatisfiable combinations without exhaustive enumeration. The approach aims to enhance complexity-theoretic understanding and provide a new, resource-bounded avenue for SAT decision procedures through pivoted formulations and graph-based reasoning.

Abstract

We propose a polynomially bounded, in time and space, method to decide whether a given 3-SAT formula is satisfiable or not. The tools we use here are, in fact, very simple. We first decide satisfiability for a particular 3-SAT formula, called pivoted 3-SAT and, after a plain transformation, still keeping the polynomial boundaries, it is shown that 3-SAT formulas can be written as pivoted formulas.
Paper Structure (4 sections, 4 theorems, 33 equations)

This paper contains 4 sections, 4 theorems, 33 equations.

Table of Contents

  1. Introduction
  2. Basic Definitions
  3. The Search For Compatible Antichains
  4. A Simpler Digraph

Key Result

Lemma 2.7

Any pivoted 2-sat formula is logically equivalent to its complete version.

Theorems & Definitions (34)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3: SAT
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Lemma 2.7
  • Proposition 2.8
  • Definition 2.9
  • Definition 2.10
  • ...and 24 more