View Related Documents

Abstract

Let F = C 1 and ctdot and 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(20.18674n ). Thereby we improve a result in [2,3] stating X3SAT isin O(20.2072n ) and a bound of O(20.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 isin O(20.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).

Fulltext Preview

Image of the first page of the fulltext document