Exact 3-satisfiability is decidable in time O(20.16254n) |
| |
Authors: | Stefan Porschen Bert Randerath Ewald Speckenmeyer |
| |
Affiliation: | (1) Institut für Informatik, Universität zu Köln, 50969 Köln, Germany |
| |
Abstract: | Let F = C1 Cm be a Boolean formula in conjunctive normal form over a set V of n propositional variables, s.t. each clause Ci 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 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 O(20.16254n).An extended abstract of this paper was presented at the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002). |
| |
Keywords: | exact satisfiability autonomous clause pattern formula graph perfect matching NP-completeness |
本文献已被 SpringerLink 等数据库收录! |