We develop a hypergraph container method for the Boolean Satisfiability Problem (SAT) via the newly developed container results [Campos and Samotij (2024)]. This provides an explicit connection between the extent of spread of clauses and the efficiency of container-based algorithms. Informally, the more evenly the clauses are distributed, the stronger the shrinking effect of the containers, which leads to faster algorithms for SAT. To quantify the extent of spread, we use a weighted point of view, in which a clause of size $s$ receives weight $p^s$ for some $0<p\le 1$.In this way, we introduce the notion of $(λ,p)_k$-structure for SAT formulas, where $λ$ is the spread parameter and $k$ is the maximum size of clauses. By the almost-independence property of containers, we prove that for formulas with $(λ,p)_k$-structures, one can distinguish between ``unsatisfiable formulas'' and ``formulas satisfying at least a $(1-δ)$-fraction of clauses'' in sub-exponential time. This shows that sufficiently spread formulas are not worst-case instances for Gap-ETH. Moreover, we show that the speedup is directly controlled by the spread parameter $λ$, yielding faster exact algorithms for SAT formulas containing a $(λ,p)_k$-structure. This result extends previous work [Zamir (STOC 2023)] to the non-uniform case.

翻译：我们基于最新发展的容器理论[Campos和Samotij (2024)]，针对布尔可满足性问题（SAT）提出了一种超图容器方法。该方法揭示了子句扩散程度与基于容器的算法效率之间的显式关联。非正式地说，子句分布越均匀，容器的收缩效应越强，从而能够实现更快的SAT算法。为量化扩散程度，我们采用加权视角：对于大小为$s$的子句赋予权重$p^s$（其中$0<p\le 1$）。由此引入SAT公式的$(λ,p)_k$结构概念，其中$λ$为扩散参数，$k$为子句最大长度。利用容器的近乎独立性性质，我们证明：对于具有$(λ,p)_k$结构的公式，可在次指数时间内区分"不可满足公式"与"至少满足$(1-δ)$比例子句的公式"。这表明充分扩散的公式并非Gap-ETH的最坏情况实例。此外，我们证明加速效果直接受扩散参数$λ$控制，从而为具有$(λ,p)_k$结构的SAT公式提供更快的精确算法。该结果将先前工作[Zamir (STOC 2023)]推广至非均匀情形。