文章基本信息

标题：Measure and Conquer for Max Hamming Distance XSAT
本地全文：下载
作者：Gordon Hoi ; Frank Stephan
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：149
页码：1-19
DOI：10.4230/LIPIcs.ISAAC.2019.15
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：XSAT is defined as the following: Given a propositional formula in conjunctive normal form, can one find an assignment to variables such that there is exactly only 1 literal that is true in every clause, while the other literals are false. The decision problem XSAT is known to be NP-complete. Crescenzi and Rossi [Pierluigi Crescenzi and Gianluca Rossi, 2002] introduced the variant where one searches for a pair of two solutions of an X3SAT instance with maximal Hamming Distance among them, that is, one wants to identify the largest number k such that there are two solutions of the instance with Hamming Distance k. DahllÃ¶f [Vilhelm DahllÃ¶f, 2005; Vilhelm DahllÃ¶f, 2006] provided an algorithm using branch and bound method for Max Hamming Distance XSAT in O(1.8348^n); Fu, Zhou and Yin [Linlu Fu and Minghao Yin, 2012] worked on a more specific problem, the Max Hamming Distance X3SAT, and found for this problem an algorithm with runtime O(1.6760^n). In this paper, we propose an exact exponential algorithm to solve the Max Hamming Distance XSAT problem in O(1.4983^n) time. Like all of them, we will use the branch and bound technique alongside a newly defined measure to improve the analysis of the algorithm.
关键词：XSAT; Measure and Conquer; DPLL; Exponential Time Algorithms