/* 
  * deterministic-cell-like-SAT.pli:
  * This P-Lingua program defines a family of recognizer P systems 
  * to solve the SAT problem, slightly adapting the design presented in:
  *  Pérez-Jiménez, M.J., Romero-Jiménez, Á., Sancho-Caparrini, F.:
  *  Complexity classes in models of cellular computing with membranes.
  *  Natural Computing 2(3), 265–285 (2003)
  *
  * 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(n,m)
{
 /* 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{1,2*n}-[]'2 --> +[r{0,2*n}];
 -[r{i,2*n} --> r{i-1,2*n}]'2 : 1<= i <= m;
 -[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{2*m+3*n+3}]'1 --> +[] no;

} /* End of Sat module */

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

 call Sat(4,7);

 /* Expansion of the input multiset */

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

 /* 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 */