跳到正文
研踪PaperTrail
← 研踪 PaperTrail

arXiv:2611.16814 · v1

Improved Deterministic Algorithms for $k$-SAT: Generalization of Chains and Recurrence Proof

首次提交 2026-11-12 21:50
版本更新 2026-11-12 21:50
雷达观测 2026-11-13 14:15
arXiv ↗PDF ↗

摘要

We present a deterministic algorithm for 3-SAT running in $1.32736^n$ time. The algorithm is built on a branching-and-chain framework augmented with a polynomial-time expansion procedure that joins short chains through additional clauses to form bounded-size blocks, which impose stronger constraints on the assignment space. After branching, the algorithm chooses between derandomized local search guided by the block structure and enumeration of block assignments together with selected port variables, reducing the remaining formula to 2-SAT. A weighted analysis of branching, partial-assignment, and local-search costs, together with inductive bounds for chains and block interactions, establishes the running-time guarantee. The framework is self-contained and also offers guidance for practical SAT solver design by identifying useful clause-overlap structures and suggesting when to switch between local-search and reduction-based strategies.

AI 论文解读

基于摘要 · 非全文审阅

此版本尚未生成 AI 解读。解读由后台任务生成并按论文版本保存,登录后共享已有结果。

版本差异

目前只观测到一个版本,无法比较变化。之后收录新版本时,会在这里对照标题、作者、分类和摘要。

观测到的版本

相邻记录可能跳过中间版本;首次发现 v2 及以上也会标为版本更新。

v1 · 2026-11-12 21:50 · 最新观测版本

Improved Deterministic Algorithms for $k$-SAT: Generalization of Chains and Recurrence Proof

We present a deterministic algorithm for 3-SAT running in $1.32736^n$ time. The algorithm is built on a branching-and-chain framework augmented with a polynomial-time expansion procedure that joins short chains through additional clauses to form bounded-size blocks, which impose stronger constraints on the assignment space. After branching, the algorithm chooses between derandomized local search guided by the block structure and enumeration of block assignments together with selected port variables, reducing the remaining formula to 2-SAT. A weighted analysis of branching, partial-assignment, and local-search costs, together with inductive bounds for chains and block interactions, establishes the running-time guarantee. The framework is self-contained and also offers guidance for practical SAT solver design by identifying useful clause-overlap structures and suggesting when to switch between local-search and reduction-based strategies.

查看此版本解读 →查看此版本原文 ↗