Let
F =
C
1
C
m
be a Boolean formula in conjunctive normal form over a set
V of
n propositional variables, s.t. each clause
C
i
contains at most three literals
l over
V. Solving the problem exact 3-satisfiability (X3SAT) for
F means to decide whether there is a truth assignment setting exactly one literal in each clause of
F to true (1). As is well known X3SAT is NP-complete [6]. By exploiting a perfect matching reduction we prove that X3SAT is deterministically decidable in time
O(2
0.18674n
). Thereby we improve a result in [2,3] stating X3SAT
O(2
0.2072n
) and a bound of
O(2
0.200002n
) for the corresponding enumeration problem #X3SAT stated in a preprint [1]. After that by a more involved deterministic case analysis we are able to show that X3SAT
O(2
0.16254n
).
Keywords exact satisfiability - autonomous clause pattern - formula graph - perfect matching - NP-completeness
An extended abstract of this paper was presented at the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002).