GUO Ping, JI Jinfang, CHEN Haizhu, et al., “Solving All-SAT Problems by P Systems,” Chinese Journal of Electronics, vol. 24, no. 4, pp. 744-749, 2015, doi: 10.1049/cje.2015.10.013
Citation: GUO Ping, JI Jinfang, CHEN Haizhu, et al., “Solving All-SAT Problems by P Systems,” Chinese Journal of Electronics, vol. 24, no. 4, pp. 744-749, 2015, doi: 10.1049/cje.2015.10.013

Solving All-SAT Problems by P Systems

doi: 10.1049/cje.2015.10.013
Funds:  This work is supported by the National Science Foundation for Young Scholars of China (No.61201347), the Natural Science Foundation Project of CQ CSTC (No.2012jjA40022, No.2011jjA40027, No.2012jjA40011) and the Fundamental Research Funds for the Central Universities (No.CDJZR12180002).
  • Received Date: 2014-03-03
  • Rev Recd Date: 2014-08-11
  • Publish Date: 2015-10-10
  • The satisfiability problem (SAT) is a well known NP-complete problem. Obtaining All of the truth assignments of SAT is called All-SAT and it has numerous applications in artificial intelligence and computer theories. Many algorithms about SAT have been built, but how to solve All-SAT is still difficult. P system is a new distributed and parallel computation model. We use membrane division, which is frequently investigated to obtain an exponential working space in a linear time, to design a family of P systems to solve All-SAT in polynomial time. Our work provides a new and effective solution to All-SAT in a distributed and parallel manner.
  • loading
  • S.A. Cook, "The complexity of theorem-proving procedures", Proc. of the 3rd annual ACM symposium on Theory of computing, Shaker Heights, Ohio, USA, pp.151-158, 1971.
    M. Davis and H. Putnam, "A computing procedure for quantification theory", Journal of the ACM, Vol.7, No.3, pp.201-215, 1960.
    M. Davis, G. Logemann and D. Loveland, "A machine program for theorem-proving", Communications of the ACM, Vol.5, No.7, pp.394-397, 1962.
    D.F. Zhang, W.Q. Huang and H.X. Wang, "Personification annealing algorithm for solving SAT problem", Chinese Journal of Computers, Vol.25, No.2, pp.1-8, 2002. (in Chinses)
    S. He and B. Zhang, "Solving SAT by algorithm transform of Wu's method", Journal of Computer Science and Technology, Vol.14, No.5, pp.468-480, 1999.
    E. Koutsoupias and C.H. Papadimitriou, "On the greedy algorithm for satisfiability", Information Processing Letters, Vol.43, No.1, pp.53-55, 1992.
    G. Ciobanu, Gh. P?un and M.J. Pérez-Jiménez, Applications of Membrane Computing, Springer, Germany, pp.315-346, 2006.
    K. Ishii, A. Fujiwara and H. Tagawa, "Asynchronous P systems for SAT and Hamiltonian cycle problem", Proc. of the World Congress on Nature and Biologically Inspired Computing, Kitakyushu, Japan, pp.513-519, 2010.
    Z. Gazdag and G. Kolonits, "A new approach for solving SAT by P systems with active membranes", Proc. of the 13th International Conference on Membrane Computing, Budapest, Hungary, pp. 195-207, 2012.
    L.Q. Pan and A. Alhazov, "Solving HPP and SAT by P systems with active membranes and separation rules", Acta Informatica, Vol.43, No.2, pp.131-145, 2006.
    H. Tagawa and A.Fujiwara, "Solving SAT and Hamiltonian cycle problem using asynchronous P systems". IEICE Transactions on Information and Systems, Vol.95, No.3, pp. 746-754, 2012.
    M.A. Gutiérrez-Naranjo, M.J. Pérez-Jiménez and F.J. Romero- Campero, "A uniform solution to SAT using membrane creation", Theoretical Computer Science, Vol.371, No.1, pp.54- 61, 2007.
    K.L. McMillan, "Applying SAT methods in unbounded symbolic model checking", Proc. of the Conference on Computer Aided Verification, Copenhagen, Denmark, pp.250-264, 2002.
    H.S. Jin, H.J. Han and F. Somenzi, "Efficient conflict analysis for finding all satisfying assignments of a Boolean circuit", Proc. of International Conference on Tools and Algorithms for Construction and Analysis of Systems, Edinburgh, UK, pp. 287-300, 2005.
    O. Grumberg, A. Schuster and A. Yadgar, "Memeory eficient all-solutions SAT solver and its application for reachability anlysis". Proc. of 5th International Conference on Formal Methods in Computer-Aided Design, Austin, Texas, USA, pp. 275- 289, 2004.
    A. Alhazov, L.Q. Pan and Gh. Pun, "Trading polarizations for labels in P systems with active membranes". Acta Informatica, Vol.41, No.2-3, pp.111-144, 2004.
    L.Q. Pan and T.-O. Ishdorj, "P systems with active membranes and separation rules", Journal of Universal Computer Science, Vol.10, No.5, pp.630-649, 2004.
    A.E. Porreca, G. Mauri and C. Zandron, "Non-confluence in divisionless P systems with active membranes", Theoretical Computer Science, Vol.411, No.6, pp.878-887, 2010.
    S. Tao, L.F. Mac′?as-Ramos, L.Q. Pan, et al., "Time-free solution to SAT problem using P systems with active membranes", Theoretical Computer Science, Vol.529, pp.61-68, 2014.
    Z.Q. Bi, G.X. Chen and M.J. Shan, "A method for solving All- SAT", Computer Engineering and Applications, Vol.45, No.3, pp.35-37, 2009. (in Chinese)
  • 加载中


    通讯作者: 陈斌,
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (332) PDF downloads(756) Cited by()
    Proportional views


    DownLoad:  Full-Size Img  PowerPoint