首页 | 本学科首页   官方微博 | 高级检索  
     


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=C1andsdotsdotsdotandCm 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 X3SATisinO(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 X3SATisinO(20.16254n).
Keywords:exact satisfiability  autonomous clause pattern  formula graph  perfect matching  NP-completeness
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号