An Improved Exact Algorithm for the Exact Satisfiability Problem

TL;DR

This paper introduces a faster exact algorithm for the XSAT problem, improving the time complexity from O(1.1730^n) to O(1.1674^n) by employing a novel measure in the DPLL framework.

Contribution

It presents a new exact algorithm for XSAT with improved time complexity using a nonstandard measure for analysis.

Findings

Achieved a new fastest algorithm with O(1.1674^n) complexity.

Introduced a novel measure to tighten the algorithm's analysis.

Demonstrated improved efficiency over previous methods.

Abstract

The Exact Satisfiability problem, XSAT, is defined as the problem of finding a satisfying assignment to a formula $\varphi$ in CNF such that exactly one literal in each clause is assigned to be "1" and the other literals in the same clause are set to "0". Since it is an important variant of the satisfiability problem, XSAT has also been studied heavily and has seen numerous improvements to the development of its exact algorithms over the years. The fastest known exact algorithm to solve XSAT runs in $O(1.1730^n)$ time, where $n$ is the number of variables in the formula. In this paper, we propose a faster exact algorithm that solves the problem in $O(1.1674^n)$ time. Like many of the authors working on this problem, we give a DPLL algorithm to solve it. The novelty of this paper lies on the design of the nonstandard measure, to help us to tighten the analysis of the algorithm further.