Easy/Hard Transition in k-SAT

TL;DR

This paper models the phase transition in k-SAT problems, showing how the satisfiability shifts from easy to hard regions based on clause-variable interactions, using nonlinear recursion relations.

Contribution

It introduces a heuristic recursive model to analyze the easy/hard transition in k-SAT, revealing the underlying competition causing the phase change.

Findings

Identifies a sharp transition from bounded to runaway behavior in the model

Shows the transition is due to competition between branching and clause growth

Provides a framework to understand computational hardness in k-SAT

Abstract

A heuristic model procedure for determining satisfiability of CNF-formulae is set up and described by nonlinear recursion relations for m (number of clauses), n (number of variables) and clause filling k. The system mimicked by the recursion undergoes a sharp transition from bounded running times (easy) to uncontrolled runaway behaviour (hard). Thus the parameter space turns out to be separated into regions with qualitatively different efficiency of the model procedure. The transition results from a competition of exponential blow up by branching versus growing number of orthogonal clauses.