文章基本信息

标题：Algorithms for SAT based on search in Hamming balls
本地全文：下载
作者：Evgeny Dantsin ; Edward Hirsch ; Alexander Wolpert 等
期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2003
卷号：2003
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：We present a simple randomized algorithm for SAT and prove an upper bound on its running time. Given a Boolean formula F in conjunctive normal form, the algorithm finds a satisfying assignment for F (if any) by repeating the following: Choose an assignment A at random and search for a satisfying assignment inside a Hamming ball around A (the radius of the ball depends on F). We show that this algorithm solves SAT with a small probability of error in at most 2^{n - 0.712\sqrt{n}} steps, where n is the number of variables in F. We also derandomize this algorithm using covering codes instead of random assignments. The deterministic algorithm solves SAT in at most 2^{n - 2\sqrt{n/\log_2 n}} steps. To the best of our knowledge, this is the first non-trivial bound for a deterministic SAT algorithm.
关键词：Boolean satisfiability