corollaryroutine

Randomized approximate Max-k-SAT in subexponential time

Corollary·cor:max-sat-approximation·§1 Introduction

Statement (paper)

For every fixed k⩾2k\ge2 and ε>0\varepsilon>0, there exists a randomized algorithm that, given a kk-CNF FF on n⩾20n\ge20 variables with mm clauses, finds an assignment satisfying at least OPT⁡(F)−εm\operatorname{OPT}(F)-\varepsilon m clauses with probability 1−2−Ω(n)1-2^{-\Omega(n)}, in (n+m)Ok,ε(1)2Ok,ε(ρ(n)) (n+m)^{O_{k,\varepsilon}(1)}2^{O_{k,\varepsilon}(\rho(n))} time and (n+m)Ok,ε(1)(n+m)^{O_{k,\varepsilon}(1)} space.

In plain English

For fixed k⩾2k\ge2 and ε>0\varepsilon>0, a randomized algorithm finds, with probability 1−2−Ω(n)1-2^{-\Omega(n)}, an assignment satisfying at least OPT⁡(F)−εm\operatorname{OPT}(F)-\varepsilon m clauses of a kk-CNF FF, in time (n+m)Ok,ε(1)2Ok,ε(ρ(n))(n+m)^{O_{k,\varepsilon}(1)}2^{O_{k,\varepsilon}(\rho(n))} and polynomial space.

Why it's here

This applies the main subexponential counting algorithm to Max-kk-SAT, showing that additive εm\varepsilon m approximation is also possible in subexponential time. The counting theorem supplies the engine, and the randomized approximation inherits its time and polynomial space bounds.
Classified routine:
Direct consequence of the paper's main counting theorem (thm-main): additive εm approximation for Max-k-SAT follows by a standard reduction, e.g. random clause sampling plus self-reducibility, that turns an exact counting or decision engine into an approximate optimizer while keeping its time and space bounds.

Uses

thmSubexponential deterministic k-CNF model counting

Used by

Nothing in the paper

Sources

PaperOpen
Section
§1 Introduction
Page
—
Label
cor:max-sat-approximation
Line
main_full_version.tex:111
Leannot aligned

Phase 2 aligns this node to a Lean declaration.