• 中国精品科技期刊
  • CCF推荐A类中文期刊
  • 计算领域高质量科技期刊T1类
Advanced Search
Zhou Junping, Yin Minghao, Zhou Chunguang, Zhai Yandong, Wang Kangping. Minimized Upper Bound for #3-SAT Problem in the Worst Case[J]. Journal of Computer Research and Development, 2011, 48(11): 2055-2063.
Citation: Zhou Junping, Yin Minghao, Zhou Chunguang, Zhai Yandong, Wang Kangping. Minimized Upper Bound for #3-SAT Problem in the Worst Case[J]. Journal of Computer Research and Development, 2011, 48(11): 2055-2063.

Minimized Upper Bound for #3-SAT Problem in the Worst Case

More Information
  • Published Date: November 14, 2011
  • Propositional model counting or #SAT is the problem of computing the number of models for a given propositional formula. The rigorous theoretical analysis of algorithms for solving #SAT have been proposed in the literature. The time complexity is calculated based on the size of the #SAT instances, depending on not only the number of variables, but also the number of clauses. Researches on the worst case upper bound for #SAT with the number of clauses as the parameter can not only measure the efficiency of the algorithms, but also correctly reflect their performance. Therefore, it is significant to exploit the minimized upper bound of #SAT problem in the worst case using the number of clauses as the parameter. In this paper, we firstly analyze the CER algorithm which we have proposed for solving #SAT and prove an upper bound O(2\+m) regarding the number of clauses as the parameter. In order to increase the efficiency, an algorithm MCDP based on Davis-Putnam-Logemann-Loveland (DPLL) for solving #3-SAT is presented. By analyzing the algorithm, we obtain the worst-case upper bound O(1.8393\+m) for #3-SAT, where m is the number of clauses in a formula.
  • Related Articles

    [1]Wang Jingjing, Wang Yanhao, Jiang Wenjun, Zeng Yifu, Zhu Tuanfei. Fast Algorithm for Approximate Motif Counting in Temporal Graph Streams[J]. Journal of Computer Research and Development. DOI: 10.7544/issn1000-1239.202330788
    [2]Yu Ying, Zhu Huilin, Qian Jin, Pan Cheng, Miao Duoqian. Survey on Deep Learning Based Crowd Counting[J]. Journal of Computer Research and Development, 2021, 58(12): 2724-2747. DOI: 10.7544/issn1000-1239.2021.20200699
    [3]Ouyang Dantong, Jia Fengyu, Liu Siguang, Zhang Liming. An Algorithm Based on Extension Rule For Solving #SAT Using Complementary Degree[J]. Journal of Computer Research and Development, 2016, 53(7): 1596-1604. DOI: 10.7544/issn1000-1239.2016.20150032
    [4]Fu Ning, Du Chenglie, Li Jianliang, Liu Zhiqiang, Peng Han. Analysis and Verification of AADL Hierarchical Schedulers[J]. Journal of Computer Research and Development, 2015, 52(1): 167-176. DOI: 10.7544/issn1000-1239.2015.20130722
    [5]Zhou Junping, Jiang Yunhui, and Yin Minghao. New Worst-Case Upper Bounds for X2SAT[J]. Journal of Computer Research and Development, 2014, 51(3): 598-605.
    [6]Li Zhen, Yang Yahui, Xie Gaogang, Qin Guangcheng. An Identification Method Combining Data Streaming Counting with Probabilistic Fading for Heavy-Hitter Flows[J]. Journal of Computer Research and Development, 2011, 48(6): 1010-1017.
    [7]Lai Yong, Ouyang Dantong, Cai Dunbo, and Lü Shuai. Model Counting and Planning Using Extension Rule[J]. Journal of Computer Research and Development, 2009, 46(3): 459-469.
    [8]Ren Jinping and Lü Shuwang. Enumerations and Counting of Orthomorphic Permutations[J]. Journal of Computer Research and Development, 2006, 43(6): 1071-1075.
    [9]Yang Zhiying, Zhu Hong, Lei Xiangxin. Achievements and Prospects of Smoothed Analysis of Algorithms[J]. Journal of Computer Research and Development, 2005, 42(2): 286-293.
    [10]Ma Liang, Chen Qunxiu, and Cai Lianhong. An Improved Model for Adaptive Text Information Filtering[J]. Journal of Computer Research and Development, 2005, 42(1): 79-84.

Catalog

    Article views (835) PDF downloads (382) Cited by()

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return