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

Fund Project:

National Natural Science Foundation of China (61271264, 11471110)

  • Article
  • | |
  • Metrics
  • |
  • Reference [17]
  • |
  • Related [20]
  • | | |
  • 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
    [1] Cook SA. The complexity of theorem-proving procedures. In:Proc. of the 3rd Annual ACM Symp. on Theory of Computing. 1971. 151-158.[doi:10.1145/800157.805047]
    [2] Levin L. Universal search problems. Problems of Information Transmission, 1973,9(3):265-266.
    [3] Even S, Itai A, Shamir A. On the complexity of timetable and multi-commodity flow problems. In:Proc. of the Symp. on Foundations of Computer Science. IEEE Xplore, 1975. 184-193.[doi:10.1109/SFCS.1975.21]
    [4] Monien B, Speckenmeyer E. Solving satisfiabilty in less than 2n steps. Discrete Applied Mathematics, 1985,10(3):287-295.
    [5] Paturi R, Pudlak P, Zane F. Satisfiability coding lemma. In:Proc. of the 38th IEEE Symp. on Foundations of Computing. 1997. 566-574.
    [6] Paturi R, Pudlak P, Saks ME, Zane F. An improved exponential-time algorithm for k-SAT. In:Proc. of the 39th IEEE Symp. on Foundations of Computing. 1998. 628-637.
    [7] Schöning U. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In:Proc. of the 40th IEEE Symp. on Foundations of Computing. IEEE, 1999. 410-414.
    [8] Hertli T. 3-SAT faster and simpler-Unique-SAT bounds for PPSZ hold in general. In:Proc. of the Foundations of Computer Science. IEEE, 2011. 277-284.
    [9] Dantsin E, Goerdt A, Hirsch EA, et al. A deterministic (2-2/(k+1))n algorithm for k-SAT based on local search. Theoretical Computer Science, 2002,289:69-83.
    [10] Moser RA, Scheder D. A full derandomization of Schöening's k-SAT algorithm. In:Proc. of the Annual ACM Symp. on Theory of Computing. 2010. 245-252.
    [11] Makino K, Tamaki S, Yamamoto M. Derandomizing HSSW algorithm for 3-SAT. In:Proc. of the Int'l Conf. on Computing and Combinatorics. Springer-Verlag, 2011. 1-12.
    [12] Strassen V. Gaussian elimination is not optimal. Numerische Mathematik, 1969,13:354-356.
    [13] Coppersmith D, Winograd S. Matrix multiplication via arithmetic progressions. Journal of Symbolic Computation, 1990,9(3):251-280.
    [14] Alon N, Galil Z, Margalit O. On the exponent of the all-pairs shortest path problem. Journal of Computer and System Sciences, 1997,54:255-262.
    [15] Williams R. Maximum two-satisfiability. In:Proc. of the Encyclopedia of Algorithms. 2008. 1-99.
    [16] Karp RM. Reducibility among combinatorial problems. Journal of Symbolic Logic, 1972,1(4):85-103.
    [17] Bellman R. Notes on the theory of dynamic programming iv-maximization over discrete sets. Naval Research Logistics Quarterly, 1956,3(1):67-70.[doi:10.1002/nav.3800030107]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:3768
  • PDF: 4401
  • HTML: 1758
  • Cited by: 0
History
  • Received:March 17,2017
  • Revised:July 07,2017
  • Online: June 08,2018
You are the first2044861Visitors
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