Formal Description Of The DPLL Algorithm With Clause Learning Based On Membrane Calculus

Although the propositional logic can meet the problem is NP-complete problem, but there isstill a SAT Solver to determine SAT on many rules the world of computer-related problems. Forstructured problems, fast SAT Solver is called DPLL algorithm based on backtracking procedure,extending the additional technologies, such as the clause. The DPLL with clause learning isimportant for fast complete Boolean satisfiability Solver. DPLL is the most classic completemethod for solving SAT problems, ideas based on depth-first search on binary trees, throughtruth assignment of atoms to quickly reduce the size clause set. DPLL solving SAT problemsuntil recent years has been effectively applied in reality. Improvement of the algorithm is themain reason, its most important improvement of DPLL SAT Solver technology is clause learning.DPLL clause learning is an extension method, can be simply interpreted as a truth assignmentconflicts, analyzes the causes of the conflict, find the conflicting clauses and record in order toachieve the non-sequential back and prevent the same conflict in the search process.Typically, services that a transaction with one or more nested can be nested to express thestructure of the cell membrane. Reaction rules can be used to describe the General activities,similar to this and in General Petri nets. Membranes evolved a new method of transaction formal,syntax, semantics, presentation skills, and override the logical semantic description mobiletransaction and transaction processing of dynamic change of process. Cell membranes of thesyntax and semantics of a biological membrane model membranes can be nested, linked below,the concept of, which itself can also move in, move out, dissolve, and build. On operationalsemantics by the chemical abstract model so calculus is Turing equivalent to the power ofexpression of cell membrane. Membrane calculus is an extension of cell membrane computing,membrane computing emphasize process, calculation of cell membrane main highlight is skills.Calculation compared with the cell membrane, membrane calculation increases the reaction rules,formal method is a new transaction.Clause pruning uses search technology, contains strong conflict analysis of process andspeed up the efficiency of learning. But so far, the formal description clause learning is still notperfect. For example, during the process of assigning one layer, not intuitive performance thecurrent layer status; the current layer, after the first clash, variable reverse the mandatory negated, then is what kind of status (conflicts or meet). Such problems, described by membrane calculuscan be more intuitive, more layered reflecting the DPLL procedure.Tableau abstract in this paper, by membrane calculus, formal description of the DPLLalgorithm with clause learning. The DPLL procedure and clause learning process is describedabstractly, provided a formal verification for clause-learning process. Two aspects of this paperwill be based on calculations from the cell membrane Description: cell membrane describe thegeneral process of DPLL, and analysis of conflict (clause) in the process. And verified with apractical example. In order to prove that the cell membrane calculus can be used to formallydescribe the DPLL, clause the purpose of learning the whole process. More intuitive and conciseexpression of the whole learning process. As the DPLL algorithm provides a formal descriptionof the new, but also promotes the development of membrane calculus in the computer field.