License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ISAAC.2019.15
URN: urn:nbn:de:0030-drops-115119
Go to the corresponding LIPIcs Volume Portal

Hoi, Gordon ; Stephan, Frank

Measure and Conquer for Max Hamming Distance XSAT

LIPIcs-ISAAC-2019-15.pdf (0.5 MB)


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.

BibTeX - Entry

  author =	{Gordon Hoi and Frank Stephan},
  title =	{{Measure and Conquer for Max Hamming Distance XSAT}},
  booktitle =	{30th International Symposium on Algorithms and Computation (ISAAC 2019)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-130-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{149},
  editor =	{Pinyan Lu and Guochuan Zhang},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-115119},
  doi =		{10.4230/LIPIcs.ISAAC.2019.15},
  annote =	{Keywords: XSAT, Measure and Conquer, DPLL, Exponential Time Algorithms}

Keywords: XSAT, Measure and Conquer, DPLL, Exponential Time Algorithms
Collection: 30th International Symposium on Algorithms and Computation (ISAAC 2019)
Issue Date: 2019
Date of publication: 28.11.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI