SAT - Active membranes

Description

Well-known problem SAT, solved with P systems with active membranes.

Model in P-Lingua

The corresponding P-Lingua file is the following:

/*
  * SAT.pli:
  * This P-Lingua program defines a family of recognizer P systems
  * to solve the SAT problem.
  *
  * For more information about P-Lingua see http://www.gcn.us.es/plingua.htm
  *
  * Copyright (C) 2008  Ignacio Perez-Hurtado (perezh@us.es)
  *                     Research Group On Natural Computing
  *                     http://www.gcn.us.es
  *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
  * the Free Software Foundation, either version 3 of the License, or
  * (at your option) any later version.
  *
  * This program is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  * GNU General Public License for more details.
  *
  * You should have received a copy of the GNU General Public License
  *  along with this program.  If not, see <http://www.gnu.org/licenses/>.
  */

/* Module that defines a family of recognizer P systems
   to solve the SAT problem */
@model<membrane_division>
def Sat(m,n)
{
 /* Initial configuration */
 @mu = [[]'2]'1;

 /* Initial multisets */
 @ms(2) = d{1};

 /* Set of rules */
 [d{k}]'2 --> +[d{k}]-[d{k}] : 1 <= k <= n;

 {
  +[x{i,1} --> r{i,1}]'2;
  -[nx{i,1} --> r{i,1}]'2;
  -[x{i,1} --> #]'2;
  +[nx{i,1} --> #]'2;
 } : 1 <= i <= m;

 {
  +[x{i,j} --> x{i,j-1}]'2;
  -[x{i,j} --> x{i,j-1}]'2;
  +[nx{i,j} --> nx{i,j-1}]'2;
  -[nx{i,j} --> nx{i,j-1}]'2;
 } : 1<=i<=m, 2<=j<=n;

 {
  +[d{k}]'2 --> []d{k};
  -[d{k}]'2 --> []d{k};
 } : 1<=k<=n;

 d{k}[]'2 --> [d{k+1}] : 1<=k<=n-1;
 [r{i,k} --> r{i,k+1}]'2 : 1<=i<=m, 1<=k<=2*n-1;
 [d{k} --> d{k+1}]'1 : n <= k<= 3*n-3;
 [d{3*n-2} --> d{3*n-1},e]'1;
 e[]'2 --> +[c{1}];
 [d{3*n-1} --> d{3*n}]'1;
 [d{k} --> d{k+1}]'1 : 3*n <= k <= 3*n+2*m+2;
 +[r{1,2*n}]'2 --> -[]r{1,2*n};
 -[r{i,2*n} --> r{i-1,2*n}]'2 : 1<= i <= m;
 r{1,2*n}-[]'2 --> +[r{0,2*n}];
 -[c{k} --> c{k+1}]'2 : 1<=k<=m;
 +[c{m+1}]'2 --> +[]c{m+1};
 [c{m+1} --> c{m+2},t]'1;
 [t]'1 --> +[]t;
 +[c{m+2}]'1 --> -[]Yes;
 [d{3*n+2*m+3}]'1 --> +[]No;

} /* End of Sat module */

/* Main module */
def main()
{
 /* Call to Sat module for m=4 and n=6 */

 call Sat(4,6);

 /* Expansion of the input multiset */

 @ms(2) += x{1,1}, nx{1,2}, nx{2,2}, x{2,3},
           nx{2,4}, x{3,5}, nx{4,6};

 /* To define another P system of the family, call the Sat module with other parameters and
    expand the input multiset with other values */

} /* End of main module */

Files

Adapting a problem to MeCoSim philosophy

The previous model solves our problem, in this case SAT, by means of P systems. With P-Lingua, a general-purpose language, parsers and simulators have been provided.

However, the given P-Lingua file includes the definition of our P system as provided for the designer, but it also incorporates the specific values for m (clauses) and n (variables), thus setting a P system inside the family of SAT<m,n>. Besides, the file also includes the specific input for the system (cod(s)) codifying a formula.

Thus, there is a clear separation between the developer of parsers and simulators and the designer of solutions based on P systems, that have in P-Lingua framework the proper tools to forget about developing software tools for the modelling and simulation and can concentrate in designing solutions based on P systems. But there is no separation between designer and end-user, the instantiation of any P system of the family SAT<m,n> requires the manipulation of the same file including the specification of the family, and the same happens if that end user wants to use the solution for solving the problem for a given formula.

Among the goals of MeCoSim is the clear separation of these roles, so a custom app is provided defining the inputs for introducing the specific instance of the P system and the given formula, along with the outputs adapted to our problem, thus focusing the attention in solving the problem beyond the meta-analysis of the P system, that is interesting for the designer but probably not for a person trying to know the satisfiability of the P system.

Adapted files

Results

../../_images/SATapp.png

SAT plugin

The custom app allows the end user the introduction of the values for n and m to instantiate the P system, along with the formulas by input tables. However, a more natural way of entering the information is provided by SAT plugin:

../../_images/SATplugin1.png