forgot to push this

sat.pl

@@ -4,6 +4,7 @@
     run_sat/2,
     run_sat/3,
     run_sat_iteratively/2,
+    call_maxsat/2,
     write_sat_header/1,
     sat_vars/1,
     sat_comment/1,

sepi_bounds.pl

@@ -2,14 +2,14 @@
   sepi_bounds,
   [
     % Commands
-    sepi_glb_bounds/3
+    sepi_glb_bounds/2
   ]
 ).
 
 
 :- use_module(biocham).
+:- use_module(sat).
 :- use_module(sepi_infos).
-:- use_module(sepi_util).
 
 
 :- initial(option(merge_restriction: yes)).
@@ -28,7 +28,7 @@ sepi_glb_bounds(FileName1, FileName2) :-
   string_concat(FileRoot, ".wcnf", FileIn),
   debug(sepi, "Will be writing clauses to: ~w", [FileIn]),
   write_clauses(G1, G2, FileIn, Merge),
-  solve_sat(FileIn),
+  solve_sat(FileIn, _Sepis),
   delete_file(FileIn).
 
 
@@ -49,11 +49,31 @@ sepi_glb_bounds(FileName1, FileName2) :-
 write_clauses(G1, G2, FileIn, Merge):-
   open(FileIn, write, Stream),
   write_header(G1, G2, Stream, Merge),
-  left_totality_clauses(G1, G2, Stream),
-  functionality_clauses(G1, G2, Stream),
-  existing_clauses(G1, G2, Stream),
+  G1 = [Nb_vertices_G1, Nb_species_G1, _, _],
+  G2 = [Nb_vertices_G2, Nb_species_G2, _, _],
+  Nb_reactions_G1 = Nb_vertices_G1 - Nb_species_G1,
+  Nb_reactions_G2 = Nb_vertices_G2 - Nb_species_G2,
+  Max_size = min(Nb_vertices_G1, Nb_vertices_G2),
+  (
+    Max_size = Nb_vertices_G1
+  ->
+    Max_species = Nb_species_G1,
+    Max_reactions = Nb_reactions_G1
+  ;
+    Max_species = Nb_species_G2,
+    Max_reactions = Nb_reactions_G2
+  ),
+  format(Stream, 'c left totality\n', []),
+  left_totality_clauses(G1, G2, Max_species, Max_reactions, Stream),
+  format(Stream, 'c functionality\n', []),
+  functionality_clauses(G1, G2, Max_species, Max_reactions, Stream),
+  format(Stream, 'c existing\n', []),
+  existing_clauses(G1, G2, Max_species, Max_reactions, Stream),
+  format(Stream, 'c set normalisation\n', []),
   set_normalisation_clauses(G1, G2, Stream),
+  format(Stream, 'c graph morphism\n', []),
   graph_morphism_clauses(G1, G2, Stream),
+  format(Stream, 'c label epimorhpism\n', []),
   label_epimorphism_clauses(G1, G2, Stream),
   (
     Merge = yes
@@ -65,36 +85,46 @@ write_clauses(G1, G2, FileIn, Merge):-
   close(Stream).
 
 
-write_header(G1, G2, Stream, Merge):-
-  .
+write_header(_G1, _G2, _Stream, _Merge).
 
 
-left_totality_clauses(G1, G2, Stream):-
+left_totality_clauses(G1, G2, Max_species, Max_reactions, Stream):-
   G1 = [Nb_vertices_G1, Nb_species_G1, _, _],
   G2 = [Nb_vertices_G2, Nb_species_G2, _, _],
   Nb_reactions_G1 = Nb_vertices_G1 - Nb_species_G1,
-  Nb_reactions_G2 = Nb_vertices_G2 - Nb_species_G2,
-  Max_size = min(Nb_vertices_G1, Nb_vertices_G2),
-  Max_species = min(Nb_species_G1, Nb_species_G2),
-  Max_reactions = min(Nb_reactions_G1, Nb_reactions_G2),
+  Max_size = Max_species + Max_reactions,
   Weight_hard_clauses = Max_size + 1,
-  Nb_species_G1_1 is Nb_species_G1 - 1,
-  numlist(0,Nb_species_G1_1,Species_G1),
-  numlist(0,Max_species,Species_G),
+  numlist(0,Nb_vertices_G1-1,Vertices_G1),
+  numlist(0,Max_size,Vertices_G),
+  format(Stream, 'c G1\n', []),
   forall(
-    member(A, Species_G1),
+    member(A, Vertices_G1),
     (
       format(Stream, "~d ", [Weight_hard_clauses]),
       forall(
-        member(J, Species_G),
+        member(J, Vertices_G),
         (
-          m_i_aj_species(0, A, J, Nb_vertices_G1, Nb_vertices_G2, Max_size, X),
-          format(Stream, "~d ", [X])
+          (
+            A < Nb_species_G1,
+            J < Max_species
+          ->
+            m_i_aj_species(0, A, J, Nb_vertices_G1, Max_species, X),
+            format(Stream, "~d ", [X])
+          ;
+            A >= Nb_species_G1,
+            J >= Max_species
+          ->
+            m_i_aj_reactions(0, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Max_species, Max_reactions, X),
+            format(Stream, "~d ", [X])
+          ;
+            true
+          )
         )
       ),
       format(Stream, "0\n", [])
     )
   ),
+  format(Stream, 'c G2\n', []),
   numlist(0,Nb_vertices_G2,Vertices_G2),
   forall(
     member(A, Vertices_G2),
@@ -103,8 +133,21 @@ left_totality_clauses(G1, G2, Stream):-
       forall(
         member(J, Vertices_G),
         (
-          m_i_aj(1, A, J, Nb_vertices_G1, Nb_vertices_G2, Max_size, X),
-          format(Stream, "~d ", [X])
+          (
+            A < Nb_species_G2,
+            J < Max_species
+          ->
+            m_i_aj_species(1, A, J, Nb_vertices_G1, Max_species, X),
+            format(Stream, "~d ", [X])
+          ;
+            A >= Nb_species_G2,
+            J >= Max_species
+          ->
+            m_i_aj_reactions(1, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Max_species, Max_reactions, X),
+            format(Stream, "~d ", [X])
+          ;
+            true
+          )
         )
       ),
       format(Stream, "0\n", [])
@@ -112,31 +155,218 @@ left_totality_clauses(G1, G2, Stream):-
   ).
 
 
-functionality_clauses(G1, G2, Stream):-
-  .
+functionality_clauses(G1, G2, Max_species, Max_reactions, Stream):-
+  G1 = [Nb_vertices_G1, Nb_species_G1, _, _],
+  G2 = [Nb_vertices_G2, Nb_species_G2, _, _],
+  Nb_reactions_G1 = Nb_vertices_G1 - Nb_species_G1,
+  Nb_reactions_G2 = Nb_vertices_G2 - Nb_species_G2,
+  Max_size = Max_species + Max_reactions,
+  Weight_hard_clauses = Max_size + 1,
+  numlist(0,Nb_vertices_G1-1,Vertices_G1),
+  numlist(0,Max_size,Vertices_G),
+  format(Stream, 'c G1\n', []),
+  forall(
+    member(A, Vertices_G1),
+    (
+      forall(
+        member(J, Vertices_G),
+        (
+          (
+            A < Nb_species_G1,
+            J < Max_species
+          ->
+            equ_impl_inf(0, 0, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream),
+            inf_impl_inf(0, 0, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream),
+            inf_imp_not_equ(0, 0, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream)
+          ;
+            A >= Nb_species_G1,
+            J >= Max_species
+          ->
+            equ_impl_inf(1, 0, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream),
+            inf_impl_inf(1, 0, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream),
+            inf_imp_not_equ(1, 0, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream)
+          ;
+            true
+          )
+        )
+      )
+    )
+  ),
+  numlist(0,Nb_vertices_G2-1,Vertices_G2),
+  format(Stream, 'c G2\n', []),
+  forall(
+    member(A, Vertices_G2),
+    (
+      forall(
+        member(J, Vertices_G),
+        (
+          (
+            A < Nb_species_G2,
+            J < Max_species
+          ->
+            equ_impl_inf(0, 1, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream),
+            inf_impl_inf(0, 1, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream),
+            inf_imp_not_equ(0, 1, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream)
+          ;
+            A >= Nb_species_G2,
+            J >= Max_species
+          ->
+            equ_impl_inf(1, 1, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream),
+            inf_impl_inf(1, 1, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream),
+            inf_imp_not_equ(1, 1, A, J, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Nb_reactions_G2, Max_species, Max_reactions, Weight_hard_clauses, Stream)
+          ;
+            true
+          )
+        )
+      )
+    )
+  ).
 
 
-existing_clauses(G1, G2, Stream):-
-  .
+existing_clauses(G1, G2, Max_species, Max_reactions, Stream):-
+  G1 = [Nb_vertices_G1, Nb_species_G1, _, _],
+  G2 = [Nb_vertices_G2, Nb_species_G2, _, _],
+  Nb_reactions_G1 = Nb_vertices_G1 - Nb_species_G1,
+  Nb_reactions_G2 = Nb_vertices_G2 - Nb_species_G2,
+  Max_size = Max_species + Max_reactions,
+  Weight_hard_clauses = Max_size + 1,
+  numlist(0,Nb_vertices_G1-1,Vertices_G1),
+  numlist(0,Nb_vertices_G2-1,Vertices_G2),
+  numlist(1,Max_size,Vertices_G),
+  forall(
+    member(A, Vertices_G),
+    (
+      (
+        A <= Max_species
+      ->
+        S = 0
+      ;
+        S = 1
+      ),
+      exists(S, A, Nb_species_G1, Nb_species_G2, Nb_reactions_G1, Nb_reactions_G2, Max_species, Max_reactions, X1),
+      format(Stream, "~d -~d ", [Weight_hard_clauses, X1]),
+      forall(
+        member(B, Vertices_G1),
+        (
+          (
+            B <= Nb_species_G1,
+            A < Max_species
+          ->
+            m_i_aj_species(0, B, A, Nb_vertices_G1, Max_species, X2),
+            format(Stream, "~d ", [X2])
+          ;
+            B > Nb_species_G1,
+            A >= Max_species
+          ->
+            m_i_aj_reactions(0, B, A, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Max_species, Max_reactions, X2),
+            format(Stream, "~d ", [X2])
+          ;
+            true
+          )
+        )
+      ),
+      format(Stream, "0\n", []),
+      format(Stream, "~d -~d ", [Weight_hard_clauses, X1]),
+      forall(
+        member(B, Vertices_G2),
+        (
+          (
+            B <= Nb_species_G2,
+            A < Max_species
+          ->
+            m_i_aj_species(1, B, A, Nb_vertices_G1, Max_species, X3),
+            format(Stream, "~d ", [X3])
+          ;
+            B > Nb_species_G2,
+            A >= Max_species
+          ->
+            m_i_aj_reactions(1, B, A, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Max_species, Max_reactions, X3),
+            format(Stream, "~d ", [X3])
+          ;
+            true
+          )
+        )
+      ),
+      format(Stream, "0\n", []),
+      forall(
+        member(B, Vertices_G1),
+        (
+          (
+            B <= Nb_species_G1,
+            A < Max_species
+          ->
+            m_i_aj_species(0, B, A, Nb_vertices_G1, Max_species, X4),
+            format(Stream, "~d -~d ~d 0\n", [Weight_hard_clauses, X4, X1])
+          ;
+            B > Nb_species_G1,
+            A >= Max_species
+          ->
+            m_i_aj_reactions(0, B, A, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Max_species, Max_reactions, X4),
+            format(Stream, "~d -~d ~d 0\n", [Weight_hard_clauses, X4, X1])
+          ;
+            true
+          )
+        )
+      ),
+      forall(
+        member(B, Vertices_G2),
+        (
+          (
+            B <= Nb_species_G2,
+            A < Max_species
+          ->
+            m_i_aj_species(1, B, A, Nb_vertices_G1, Max_species, X4),
+            format(Stream, "~d -~d ~d 0\n", [Weight_hard_clauses, X4, X1])
+          ;
+            B > Nb_species_G2,
+            A >= Max_species
+          ->
+            m_i_aj_reactions(1, B, A, Nb_species_G1, Nb_reactions_G1, Nb_species_G2, Max_species, Max_reactions, X4),
+            format(Stream, "~d -~d ~d 0\n", [Weight_hard_clauses, X4, X1])
+          ;
+            true
+          )
+        )
+      )
+    )
+  ).
+
 
+graph_morphism_clauses(_G1, _G2, _Stream).
 
-set_normalisation_clauses(G1, G2, Stream):-
-  .
 
+label_epimorphism_clauses(_G1, _G2, _Stream).
 
-graph_morphism_clauses(G1, G2, Stream):-
-  .
 
+set_normalisation_clauses(_G1, _G2, _Stream).
 
-label_epimorphism_clauses(G1, G2, Stream):-
-  .
 
+symmetry_breaking_clauses(_G1, _G2, _Stream).
 
-solve_sat(FileIn):-
-  .
+
+bound_maximisation_clauses(_G1, _G2, _Stream).
+
+
+solve_sat(FileIn, Sepis):-
+  call_maxsat(FileIn, Sepis).
+
+
+%! m_i_aj_species(+I, +A, +J, +Ns1, +Max_species, -X)
+%
+% mu_i is a morphism from an initial graph Gi to an image graph G
+% X is the SAT variable for mu_i(a) = j with an image graph of Max_size vertices
+%
+% @arg I            Interger 0/1: 0 for G1, 1 for G2
+% @arg A            Interger representing a in the initial graph
+% @arg J            Interger representing j in the image graph
+% @arg Ns1          Number of vertices in the G1
+% @arg Max_species  Number of species in the image graph
+% @arg X            SAT variable representing mu_i(a) = j
+m_i_aj_species(I, A, J, Ns1, Max_species, X):-
+  X is (1 + J + A * (Max_species + 1) + I * (Max_species * Ns1 + 1)).
 
 
-%! m_i_aj_species(+I, +A, +J, +N1, +N2, +Max_size, -X)
+%! m_i_aj_reactions(+I, +A, +J, +N1, +N2, +Max_size, -X)
 %
 % mu_i is a morphism from an initial graph Gi to an image graph G
 % X is the SAT variable for mu_i(a) = j with an image graph of Max_size vertices
@@ -144,13 +374,126 @@ solve_sat(FileIn):-
 % @arg I        Interger 0/1: 0 for G1, 1 for G2
 % @arg A        Interger representing a in the initial graph
 % @arg J        Interger representing j in the image graph
-% @arg Ns1       Number of vertices in the G1
+% @arg Ns1      Number of vertices in the G1
 % @arg Max_size Number of vertices in the image graph
 % @arg X        SAT variable representing mu_i(a) = j
-m_i_aj_species(I, A, J, Ns1, Max_species, X):-
-  X is (1 + A + J * (Ns1 + 1) + I * (Max_species + 1)).
+m_i_aj_reactions(I, A, J, Ns1, Nr1, Ns2, Max_species, Max_reactions, X):-
+  m_i_aj_species(1, Ns2, Max_species, Ns1, Max_species, X_Max_species),
+  X is X_Max_species + (1 + J + A * (Max_reactions + 1) + I * (Max_reactions * Nr1 + 1)).
+
+
+%! m_inf_ij(+S, +G, +I, +J, +N1, +N2, -X)
+%
+% mu is a morphism from an initial graph G1 to an image graph G2
+% X is the SAT variable for mu(i) < j
+%
+% @arg S    Integer 0/1: 0 for species, 1 for reaction
+% @arg G    Interger 0/1: 0 for G1, 1 for G2
+% @arg I    Integer representing i in the initial graph
+% @arg J    Integer representing j in the image graph
+% @arg N1   Number of vertices in the initial graph
+% @arg N2   Number of vertices in the image graph
+% @arg X    SAT variable representing mu(i) < j
+m_inf_ij(S, G, I, J, Ns1, Nr1, Ns2, Nr2, Max_species, Max_reactions, X) :-
+  (
+    S = 0
+  ->
+    m_i_aj_species(G, I, J, Ns1, Max_species, X1)
+  ;
+    m_i_aj_reactions(G, I, J, Ns1, Nr1, Ns2, Max_species, Max_reactions, X1)
+  ),
+  X is (X1 + Max_species * (Ns1 + Ns2) + Max_reactions * (Nr1 + Nr2) ).
 
-m_i_aj_reactions(I, A, J, Nr1, Max_reactions, X):-
-  m_i_aj_species(1, Ns2, Max_species, Ns1, Max_species, Max_species),
-  X is Max_species + (1 + A + J * (Ns1 + 1) + I * (Max_species + 1)).
 
+%! implies(+A, +B, +Stream, +Top)
+%
+% translate 'A=>B' to '-A or B'
+%
+% @arg A              First SAT variable
+% @arg B              Second SAT variable
+% @arg Stream         Stream for the CNF file
+% @arg Weight_hard_clauses Clause's weight in the CNF file
+implies(A, B, Stream, Weight_hard_clauses) :-
+  A1 is -A,
+  format(Stream, '~d ~d ~d 0~n', [Weight_hard_clauses, A1, B]).
+
+
+%! equ_impl_inf(+I, +J, +N1, +N2, +Stream, +Extremal_sepi)
+%
+% mu is a morphism from an initial graph G1 to an image graph G2
+% 'mu(i) = j' implies 'mu(i) < j + 1'
+%
+% @arg I              Interger representing the vertex i in the initial graph
+% @arg J              Interger representing the vertex j in the image graph
+% @arg N1             Number of vertices in the initial graph
+% @arg N2             Number of vertices in the image graph
+% @arg Stream         Stream for the CNF file
+% @arg Extremal_sepi  no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
+equ_impl_inf(S, G, I, J, Ns1, Nr1, Ns2, Nr2, Max_species, Max_reactions, Weight_hard_clauses, Stream) :-
+  J1 is J + 1,
+  (
+    S = 0
+  ->
+    m_i_aj_species(G, I, J, Ns1, Max_species, X1)
+  ;
+    m_i_aj_reactions(G, I, J, Ns1, Nr1, Ns2, Max_species, Max_reactions, X1)
+  ),
+  m_inf_ij(S, G, I, J1, Ns1, Nr1, Ns2, Nr2, Max_species, Max_reactions, X2),
+  implies(X1, X2, Stream, Weight_hard_clauses).
+
+
+%! inf_impl_inf(+I, +J, +N1, +N2, +Stream, +Extremal_sepi)
+%
+% mu is a morphism from an initial graph G1 to an image graph G2
+% 'mu(i) < j' implies 'mu(i) < j + 1'
+%
+% @arg I              Interger representing the vertex i in the initial graph
+% @arg J              Interger representing the vertex j in the image graph
+% @arg N1             Number of vertices in the initial graph
+% @arg N2             Number of vertices in the image graph
+% @arg Stream         Stream for the CNF file
+% @arg Extremal_sepi  no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
+inf_impl_inf(S, G, I, J, Ns1, Nr1, Ns2, Nr2, Max_species, Max_reactions, Weight_hard_clauses, Stream) :-
+  J1 is J + 1,
+  m_inf_ij(S, G, I, J, Ns1, Nr1, Ns2, Nr2, Max_species, Max_reactions, X1),
+  m_inf_ij(S, G, I, J1, Ns1, Nr1, Ns2, Nr2, Max_species, Max_reactions, X2),
+  implies(X1, X2, Stream, Weight_hard_clauses).
+
+
+%! inf_imp_not_equ(+I, +J, +N1, +N2, +Stream, +Extremal_sepi)
+%
+% mu is a morphism from an initial graph G1 to an image graph G2
+% 'mu(i) < j' implies 'mu(i) != j'
+%
+% @arg I              Interger representing the vertex i in the initial graph
+% @arg J              Interger representing the vertex j in the image graph
+% @arg N1             Number of vertices in the initial graph
+% @arg N2             Number of vertices in the image graph
+% @arg Stream         Stream for the CNF file
+% @arg Extremal_sepi  no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
+inf_imp_not_equ(S, G, I, J, Ns1, Nr1, Ns2, Nr2, Max_species, Max_reactions, Weight_hard_clauses, Stream) :-
+  m_inf_ij(S, G, I, J, Ns1, Nr1, Ns2, Nr2, Max_species, Max_reactions, X1),
+  J1 is J + 1,
+  (
+    S = 0
+  ->
+    m_i_aj_species(G, I, J1, Ns1, Max_species, X2)
+  ;
+    m_i_aj_reactions(G, I, J1, Ns1, Nr1, Ns2, Max_species, Max_reactions, X2)
+  ),
+  X3 is -X2,
+  implies(X1, X3, Stream, Weight_hard_clauses).
+
+
+%! inf_imp_not_equ(+I, +J, +N1, +N2, +Stream, +Extremal_sepi)
+%
+% Vertex I of the targeted graph exists
+%
+% @arg I              Interger representing the vertex i in the initial graph
+% @arg J              Interger representing the vertex j in the image graph
+% @arg N1             Number of vertices in the initial graph
+% @arg N2             Number of vertices in the image graph
+% @arg Stream         Stream for the CNF file
+% @arg Extremal_sepi  no/minimal_deletion/maximal_deletion cf. sepi:extremal_sepi/1
+exists(S, I, Ns1, Ns2, Nr1, Nr2, Max_species, Max_reactions, X):-
+  X is (I + 2 * (Max_species * (Ns1 + Ns2) + Max_reactions * (Nr1 + Nr2)) + S * Max_species ).

toc.org

@@ -74,6 +74,7 @@
 - sepi_neigh_merge.pl
 - sepi_old_merge.pl
 - sepi_mapping.pl
+- sepi_bounds.pl
 - sat.pl
 ** Pattern reduction
 - pattern_reduction.pl