claimroutine

Fast 3-SAT at linear clause density

Claim·§1 Introduction·inside corSuperlinear circuit lower bound for E^NP

Statement (paper)

With

a(t)=\sqrt{\log_2 t}

, there exist fixed constants

A,b>0

such that testing whether the count in the constant-density part of Theorem is positive decides

3

-SAT on formulas with

V

variables and at most

5V

clauses in time

V^b2^{A V/a(V)}

, including the

V^{O(1)}

cost per bit access of the multitape simulation.

In plain English

There are fixed constants

A,b>0

such that 3-SAT on formulas with

V

variables and at most

5V

clauses can be decided in time

V^b 2^{AV/a(V)}

, where

a(t)=\sqrt{\log_2 t}

, by checking whether the model count from the constant-density case of the main theorem is positive. This time bound includes the

V^{O(1)}

overhead per bit access in the multitape simulation.

Why it's here

This specializes the constant-density bound of Theorem 1.1 (with

k=3

and

D=5

) to a concrete running time of the form

2^{AV/\sqrt{\log V}}

with explicit polynomial overhead. The later claims in the corollary's proof need this explicit time bound to compare against a time-hierarchy argument and derive the

n\sqrt{\log n}

circuit lower bound.

Classified routine:

Direct specialization of the paper's main counting theorem (thm-main) to k=3 and clause density 5, with bookkeeping of the polynomial overhead of the multitape simulation; no new idea beyond instantiating the earlier bound.

Uses

thmSubexponential deterministic k-CNF model counting

Used by

claimTest-circuit runtime contradicts time hierarchy

Sources

PaperOpen

Section: §1 Introduction
Page: —
Label: —
Line: quantitative-circuits.tex:38

Leannot aligned

Phase 2 aligns this node to a Lean declaration.