Structure of random r-SAT below the pure literal threshold

TL;DR

This paper analyzes the structure of unsatisfiable random r-SAT formulas below the pure literal threshold, revealing the role of minimal unsatisfiable subformulas and providing asymptotic probabilities and algorithms.

Contribution

It introduces a detailed structural description of unsatisfiable formulas below the pure literal threshold and offers precise asymptotic probabilities and efficient algorithms.

Findings

Un satisfiable formulas below the pure literal threshold are characterized by a unique minimal unsatisfiable subformula.

The probability of unsatisfiability has a precise asymptotic expansion in this regime.

Efficient algorithms are provided for satisfiability and unsatisfiability proofs.

Abstract

It is well known that there is a sharp density threshold for a random $r$-SAT formula to be satisfiable, and a similar, smaller, threshold for it to be satisfied by the pure literal rule. Also, above the satisfiability threshold, where a random formula is with high probability (whp) unsatisfiable, the unsatisfiability is whp due to a large "minimal unsatisfiable subformula" (MUF). By contrast, we show that for the (rare) unsatisfiable formulae below the pure literal threshold, the unsatisfiability is whp due to a unique MUF with smallest possible "excess", failing this whp due to a unique MUF with the next larger excess, and so forth. In the same regime, we give a precise asymptotic expansion for the probability that a formula is unsatisfiable, and efficient algorithms for satisfying a formula or proving its unsatisfiability. It remains open what happens between the pure literal threshold and the satisfiability threshold. We prove analogous results for the $k$-core and $k$-colorability thresholds for a random graph, or more generally a random $r$-uniform hypergraph.