Solving SAT by P Systems with Active Membranes in Linear Time in the Number of Variables

摘要

In this paper we solve the SAT problem (the satisfiability problem of propositional formulas in conjunctive normal form) by two polynomially uniform families of P systems with active membranes. The novelty of these solutions is that these P systems can solve the SAT problem in linear time in the number of propositional variables occurring in the input. This means that the number of computation steps is independent form the number of clauses of the input. To achieve this efficiency our systems employ only the standard rules of P systems with active membranes plus membrane creation rules. Moreover, in the first solution the P systems do not use the polarizations of the membranes but use such membrane division rules which can change the labels of the involved membranes. In the second solution the P systems do not employ membrane label changing but use the polarizations of the membranes instead.