Solving All-SAT Problems by P Systems

GUO Ping; JI Jinfang; CHEN Haizhu; LIU Ran

doi:10.1049/cje.2015.10.013

Volume 24 Issue 4

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2015 > 24(4): 744-749

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

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

PDF( 563 KB)

Solving All-SAT Problems by P Systems

doi: 10.1049/cje.2015.10.013

1.
College of Computer Science, Chongqing University, Chongqing 400030, China;
2.
Department of Software Engineering, Chongqing College of Electronic Engineering, Chongqing 401331, China;
3.
Chongqing Key Laboratory of Software Theory Technology, Chongqing 400044, China

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

Abstract

Abstract

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.
- All solutions for Satisfiability problem (All-SAT),
- Satisfiability problem (SAT problem),
- Conjunctive normal form (CNF),
- P system,
- Membrane computing

FullText(HTML)

References(20)

References

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)

Relative Articles

Supplements(0)

Cited By

Proportional views