Measure and Conquer for Max Hamming Distance XSAT

Authors Gordon Hoi, Frank Stephan

Thumbnail PDF


  • Filesize: 471 kB
  • 19 pages

Document Identifiers

Author Details

Gordon Hoi
  • School of Computing, National University of Singapore, 13 Computing Drive, Block COM1, Singapore 117417, Republic of Singapore
Frank Stephan
  • Department of Mathematics, National University of Singapore, 10 Lower Kent Ridge Road, Block S17, Singapore 119076, Republic of Singapore
  • School of Computing, National University of Singapore, 13 Computing Drive, Block COM1, Singapore 117417, Republic of Singapore


The authors would like to thank the anonymous referees of ISAAC 2019 for useful suggestions. Furthermore, the authors would like to thank internet companies for putting services like Wolfram Alpha Equation Solver, Firefox Scratchpad and Google Scholar for free onto the internet.

Cite AsGet BibTex

Gordon Hoi and Frank Stephan. Measure and Conquer for Max Hamming Distance XSAT. In 30th International Symposium on Algorithms and Computation (ISAAC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 149, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
  • XSAT
  • Measure and Conquer
  • DPLL
  • Exponential Time Algorithms


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Andreas Blass and Yuri Gurevich. On the unique satisfiability problem. Information and Control, 55(1-3):80-88, 1982. Google Scholar
  2. David Eppstein. Small maximal independent sets and faster exact graph coloring. Proceedings of the Seventh Workshop on Algorithms and Data Structures, Springer Lecture Notes in Computer Science, 2125:462-470, 2001. Google Scholar
  3. David Eppstein. Quasiconvex analysis of multivariate recurrence equations for backtracking algorithms. ACM Transactions on Algorithms, 2(4):492-509, 2006. Google Scholar
  4. Fedor V. Fomin and Dieter Kratsch. Exact Exponential Algorithms. Texts in Theoretical Computer Science, EATCS, Springer, Berlin, Heidelberg, 2010. Google Scholar
  5. Fedor V. Fomin, Fabrizio Grandoni and Dieter Kratsch. A measure and conquer approach for the analysis of exact algorithms. Journal of the ACM, 56(5):25, 2009. Google Scholar
  6. Gordon Hoi, Sanjay Jain and Frank Stephan. A fast exponential time algorithm for Max Hamming X3SAT. Foundations of Software Technology and Theoretical Computer Science, FSTTCS, 2019. Google Scholar
  7. Jesper Makholm Byskov, Bolette Amitzbøll Madsen and Bolette Skjernaa. New algorithms for exact satisfiability. Theoretical Computer Science, 332(1-3):515-541, 2005. Google Scholar
  8. Linlu Fu, Junping Zhou and Minghao Yin. Worst case upper bound for the maximum Hamming distance X3SAT problem. Journal of Frontiers of Computer Science and Technology, 6(7):664-671, 2012. Google Scholar
  9. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960. Google Scholar
  10. Martin Davis, George Logemann and Donald W. Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394-397, 1962. Google Scholar
  11. Oliver Kullmann. New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science, 223(1-2):1-72, 1999. Google Scholar
  12. Pierluigi Crescenzi and Gianluca Rossi. On the Hamming distance of constraint satisfaction problems. Theoretical Computer Science, 288(1):85-100, 2002. Google Scholar
  13. Rodney G. Downey and Michael R. Fellows. Fundamentals of Parameterized Complexity. Springer, Berlin, Heidelberg, 2013. Google Scholar
  14. Stefan Porschen. On variable-weighted exact satisfiability problems. Annals of Mathematics and Artificial Intelligence, 51(1):27-54, 2007. Google Scholar
  15. Vilhelm Dahllöf. Algorithms for Max Hamming Exact Satisfiability. International Symposium on Algorithms and Computation, ISAAC 2005, Springer Lecture Notes in Computer Science, 3827:829-383, 2005. Google Scholar
  16. Vilhelm Dahllöf. Exact Algorithms for Exact Satisfiability Problems. PhD thesis, Department of Computer and Information Science, Linköping University, 2006. Google Scholar
  17. Vilhelm Dahllöf, Peter Jonsson and Richard Beigel. Algorithms for four variants of the exact satisfiability problem. Theoretical Computer Science, 320(2-3):373-394, 2004. Google Scholar