关键词: 海明距离, 可满足性（SAT）, X3SAT, DPLL, 最坏情况, 复杂性分析, 上界

Abstract: The maximum Hamming distance X-3-satisfiability (X3SAT) problem looks for the maximum Hamming distance between any two x-models of the formula F in 3-conjunctive normal form (3-CNF). This paper presents an exact algorithm HMX based on Davis-Putnam-Logemann-Loveland (DPLL) for the maximum Hamming distance X3SAT problem. The algorithm branches on some variable according to its different values in two truth assignments of the formula. Before the branching some reduction rules are used to simplify the formula. The reduction rules increase the efficiency of the algorithm. The worst case upper bound for the problem is O(1.676 0n), which improves the previous result O(1.710 7n), where n is the number of the variables in the formula.

Key words: Hamming distance, satisfiability(SAT), X3SAT, DPLL, worst case, complexity analysis, upper bound