2026-07-24T05:42:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11511 2024-03-06T10:48:11Z ddc:004 open_access

Measure and Conquer for Max Hamming Distance XSAT Hoi, Gordon Stephan, Frank XSAT Measure and Conquer DPLL Exponential Time Algorithms 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Gordon Hoi and Frank Stephan 2019 Is Part Of LIPIcs, Volume 149, 30th International Symposium on Algorithms and Computation (ISAAC 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ISAAC.2019.15 urn:nbn:de:0030-drops-115119 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2019.15 eng https://creativecommons.org/licenses/by/3.0/legalcode