SAT - Tissue cell separation

Description

Well-known problem SAT, solved with tissue P systems with cell separation.

Model in P-Lingua

The corresponding P-Lingua file is the following:

@model<TSCS>

def main()
{
        let m= 3;
        let n= 4;

        call init_membrane_structure();
        call init_first_alphabet(m,n);
        call init_second_alphabet(m,n);
        call init_environment(m,n);
        call init_multisets();
        call init_rules(m,n);
        call define_input();
}


def define_input()
{
/* DEFINIR AQUI LA DE ENTRADA DEL SISTEMA P */
/* ESCRIBIR DIFERENTES FUNCIONES PARA DIFERENTES ENTRADAS */
@ms(3) +=nx{1,1},x{2,1},x{3,1},x{1,2},nx{2,2},nx{3,2},x{1,3},nx{2,3},x{3,3}, x{1,4},x{2,4},x{3,4};

}


def init_membrane_structure()
{
        @mu = [ [ ]'1 [ ]'2 [ ]'3 ]'0;
}


def init_first_alphabet(m,n)
{
        @ms1 += A{i},B{i} : 1<=i<=n+1;
        @ms1 += a{i},b{i},T{i},F{i},y{i},v{i},w{i} : 1<=i<=n;
        @ms1 += c{i},t{i},f{i},s{i},z{i} : 1<= i <= n-1;
        @ms1 += E{j} : 1<= j <= m+1;
        @ms1 += alpha{i} : 0<= i <= 3*n+2*m+1;
        @ms1 += beta{i} : 0<= i <= 3*n + 2*m +2;
        @ms1 += q{i,j},r{i,j},u{i,j} : 1<=i<=n-1,1<=j<=n-1;
        @ms1 += x{i,j},nx{i,j},e{i,j},ne{i,j} : 1<=i<=n,1<=j<=m;
        @ms1 += d{i,j,k},nd{i,j,k} : 1 <=i<=n,1<=j<=m,1<=k<=n;
        @ms1 += q{0},S,yes,no;

}

def init_second_alphabet(m,n)
{
        @ms2 += Ap{i},Bp{i} : 1<=i<=n+1;
        @ms2 += ap{i},bp{i},Tp{i},Fp{i} : 1<=i<=n;
}

def init_environment(m,n)
{
        @ms(0) += S;
        @ms(0) += A{i},B{i},Ap{i},Bp{i} : 2<=i<=n+1;
        @ms(0) += T{i},F{i},Fp{i},y{i},w{i} : 1<=i<=n;
        @ms(0) += a{i},ap{i},b{i},bp{i},v{i} : 2<=i<=n;
        @ms(0) += Tp{i},c{i},t{i},f{i},s{i},z{i} : 1<=i<=n-1;
        @ms(0) += E{j} : 1<=j<=m+1;
        @ms(0) += alpha{i} : 1<= i <= 3*n+2*m+1;
        @ms(0) += beta{i} : 1<=i<=3*n+2*m+2;
        @ms(0) += q{i,j},r{i,j},u{i,j} : 1<=i<=n-1,2<=j<=n-1;
        @ms(0) += r{1,1};
        @ms(0) += u{1,1};
        @ms(0) += e{i,j},ne{i,j} : 1<=i<=n,1<=j<=m;
        @ms(0) += d{i,j,k},nd{i,j,k} : 1<=i<=n,1<=k<=n,1<=j<=m;
}

def init_multisets()
{
        @ms(1) = A{1},B{1};
        @ms(2) = a{1},ap{1},b{1},bp{1},v{1},q{1,1},alpha{0},yes,no;
        @ms(3) = beta{0};
}
def init_rules(m,n)
{
        /*1*/  [A{i}]'1    <--> [a{i},ap{i}]'2 : 1<=i<=n;
               [A{n+1}]'1  <--> [E{1}]'2;
        /*2*/  [Ap{i}]'1   <--> [a{i},ap{i}]'2 : 1<=i<=n;
               [Ap{n+1}]'1 <--> [E{1}]'2;
        /*3*/  [B{i}]'1    <--> [b{i},bp{i}]'2 : 1<=i<=n;
        /*4*/  [Bp{i}]'1   <--> [b{i},bp{i}]'2 : 1<=i<=n;
        /*5*/  [T{i}]'1    <--> [t{i}]'2       : 1<=i<=n-1;
        /*6*/  [Tp{i}]'1   <--> [t{i}]'2       : 1<=i<=n-1;
        /*7*/  [F{i}]'1    <--> [f{i}]'2       : 1<=i<=n-1;
        /*8*/  [Fp{i}]'1   <--> [f{i}]'2       : 1<=i<=n-1;
        /*9*/  [t{i}]'1    <--> [T{i},Tp{i}]'0 : 1<=i<=n-1;
        /*10*/ [f{i}]'1    <--> [F{i},Fp{i}]'0 : 1<=i<=n-1;
        /*11*/ [b{i}]'1    <--> [B{i+1},S]'0   : 1<=i<=n;
               [B{n+1}]'1  <--> [#]'0;
        /*12*/ [bp{i}]'1   <--> [Bp{i+1}]'0    : 1<=i<=n;
               [Bp{n+1}]'1 <--> [#]'0;
        /*13*/ [a{i}]'1    <--> [T{i},A{i+1}]'0 : 1<=i<=n;
        /*14*/ [ap{i}]'1   <--> [Fp{i},Ap{i+1}]'0 : 1<=i<=n;
        /*15*/ [A{i}]'2    <--> [c{i}]'0          : 1<=i<=n-1;
               [A{i}]'2    <--> [#]'0             : n<=i<=n+1;
        /*16*/ [Ap{i}]'2   <--> [c{i}]'0          : 1<=i<=n-1;
               [Ap{i}]'2   <--> [#]'0             : n<=i<=n+1;
        /*17*/ [B{i}]'2    <--> [c{i}]'0          : 1<=i<=n-1;
               [B{n}]'2    <--> [#]'0;
        /*18*/ [Bp{i}]'2   <--> [c{i}]'0          : 1<=i<=n-1;
               [Bp{n}]'2   <--> [#]'0;
        /*19*/ [c{i}]'2    <--> [b{i+1},bp{i+1}]'0 : 1<=i<=n-1;
        /*20*/ [v{i}]'2    <--> [y{i}*2]'0         : 1<=i<=n;
        /*21*/ [y{i}]'2    <--> [z{i},w{i}]'0      : 1<=i<=n-1;
               [y{n}]'2    <--> [w{n}]'0;
        /*22*/ [z{i}]'2    <--> [v{i+1}]'0         : 1<=i<=n-1;
        /*23*/ [w{i}]'2    <--> [a{i+1},ap{i+1}]'0  : 1<=i<=n-1;
               [w{n}]'2    <--> [E{1}]'0;
        /*24*/ [q{1,1}]'2  <--> [r{1,1}]'0;
        /*25*/ [q{i,j}]'2  <--> [r{i,j}*2]'0       : 1<=i<=n-1,2<=j<=n-1;
        /*26*/ [r{i,j}]'2  <--> [s{i},u{i,j}]'0    : 1<=i<=n-1,1<=j<=n-1;
        /*27*/ [s{i}]'2    <--> [t{i},f{i}]'0      : 1<=i<=n-1;
        /*28*/ [u{1,j}]'2  <--> [q{1,j+1},q{2,j+1}]'0 : 1<=j<=n-2;
        /*29*/ [u{i,j}]'2  <--> [q{i+1,j+1}]'0 : 2<=i<=n-2,2<=j<=n-2;
        /*30*/ [u{i,n-1}]'2 <--> [#]'0         : 1<=i<=n-1;
        /*31*/ [T{i}]'2     <--> [#]'0         : 1<=i<=n-1;
        /*32*/ [Tp{i}]'2    <--> [#]'0         : 1<=i<=n-1;
        /*33*/ [F{i}]'2     <--> [#]'0         : 1<=i<=n-1;
        /*34*/ [Fp{i}]'2    <--> [#]'0         : 1<=i<=n-1;
        /*35*/ [S]'1 --> [ ]'1 [ ]'1;
        /*36*/ [alpha{i}]'2 <--> [alpha{i+1}]'0 : 0<=i<=3*n+2*m;
        /*37*/ [beta{i}]'3  <--> [beta{i+1}]'0  : 0<=i<=3*n+2*m+1;
        /*38*/ [x{i,j}]'3   <--> [d{i,j,1}*2]'0 : 1<=i<=n,1<=j<=m;
               [nx{i,j}]'3  <--> [nd{i,j,1}*2]'0 : 1<=i<=n,1<=j<=m;
        /*39*/ [d{i,j,k}]'3 <--> [d{i,j,k+1}*2]'0 : 1<=i<=n,1<=j<=m,1<=k<=n-1;
               [nd{i,j,k}]'3 <--> [nd{i,j,k+1}*2]'0 : 1<=i<=n,1<=j<=m,1<=k<=n-1;
        /*40*/ [d{i,j,n}]'3 <--> [e{i,j}]'0 : 1<=i<=n,1<=j<=m;
               [nd{i,j,n}]'3 <--> [ne{i,j}]'0 : 1<=i<=n, 1<=j<=m;
        /*41*/ [T{i},E{j}]'1 <--> [e{i,j}]'3 : 1<=i<=n,1<=j<=m;
               [F{i},E{j}]'1 <--> [ne{i,j}]'3 : 1<=i<=n,1<=j<=m;
               [Tp{i},E{j}]'1 <--> [e{i,j}]'3 : 1<=i<=n,1<=j<=m;
               [Fp{i},E{j}]'1 <--> [ne{i,j}]'3 : 1<=i<=n,1<=j<=m;
        /*42*/ [e{i,j}]'1 <--> [T{i},E{j+1}]'0 : 1<=i<=n,1<=j<=m-1;
               [ne{i,j}]'1 <--> [F{i},E{j+1}]'0 : 1<=i<=n,1<=j<=m-1;
        /*43*/ [e{i,m}]'1 <--> [E{m+1}]'0 : 1<=i<=n;
               [ne{i,m}]'1 <--> [E{m+1}]'0 : 1<=i<=n;
        /*44*/ [T{i}]'3 <--> [#]'0 : 1<=i<=n;
               [F{i}]'3 <--> [#]'0 : 1<=i<=n;
               [Tp{i}]'3 <--> [#]'0 : 1<=i<=n;
               [Fp{i}]'3 <--> [#]'0 : 1<=i<=n;
        /*45*/ [E{j}]'3 <--> [#]'0 : 1<=j<=m;
        /*46*/ [E{m+1}]'1 <--> [yes,alpha{3*n+1+2*m}]'2;
        /*47*/ [yes]'1 <--> [beta{3*n+1+2*m+1}]'3;
        /*48*/ [alpha{3*n+1+2*m}]'2 <--> [beta{3*n+1+2*m+1}]'3;
        /*49*/ [no,beta{3*n+1+2*m+1}]'2 <--> [#]'0;
        /*50*/ [yes]'3 <--> [#]'0;

}

Files

Adapting a problem to MeCoSim philosophy

Now the values for m and n come from the data introduced by the user (not therefore hardcoded in the file) in the input tables, and the same happens with the formula after entering it from SAT plugin and convert into the input table format. The custom app defines the mechanism to convert those data in the params for P-Lingua (m, n, nvals, and variable{i}, clause{i}, val{i}, valn{i} for each i from 1 to nvals):

@model<TSCS>

...

def define_input()
{
    @ms(3) += nx{variable{i},clause{i}}*valn{i},x{variable{i},clause{i}}*val{i} : 1<=i<=nvals;
}