O(1.890n) Exact Algorithm for a Class of Separable SAT Problems
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61271264, 11471110)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    The Boolean satisfiability problem (SAT) refers to whether there is a truth assignment that satisfies a given Boolean formula, which is the first confirmed NP complete problem that generally does not exist a polynomial time algorithm unless P=NP. However many practical applications of such problems often take place and are in need of an effective algorithm to reduce their time complexity. At present, many scholars have studied the problem of SAT with clause length not exceeding k (k-SAT). From global search to local search, a large number of effective algorithms, including random algorithm and determination algorithm are developed, and the best result, including probabilistic algorithm and deterministic algorithm for solving k-SAT problems, is that the time complexity is less than O((2-2/k)n), and when k=3 the time complexity of the best algorithm is O(1.308n). However, there is little literature about SAT problems that are more general than clause length k. This paper discusses a class of separable satisfiability problems (SSAT), in particular, the problem of 3-regular separable satisfiability (3-RSSAT) where the formula can be separated into several subformulas according to certain rules. The paper proves that 3-RSSAT problem is NP complete problem because any SAT problem can be polynomially reduced to it. To determine 3-regular separability of the general SAT problem, an algorithm is given with time complexity is no more than O(1.890n). Then by using the result in the matrix multiplication algorithm optimal research field, an O(1.890n) exact algorithm is constructed for solving the 3-RSSAT problem, which is the WELL algorithm independent of clause length.

    Reference
    Related
    Cited by
Get Citation

黄金贵,王胜春.一类可分离SAT问题的O(1.890n)精确算法.软件学报,2018,29(12):3595-3603

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:March 17,2017
  • Revised:July 07,2017
  • Adopted:
  • Online: June 08,2018
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063