From e9f60df85734e79cc1959523cd424bbed147f9aa Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 29 Aug 2013 17:10:07 +0200
Subject: [PATCH] sat: implement partial symmetry breaking
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Thanks to Rüdiger Ehlers for his helpful email.

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Here.
---
 src/tgbaalgos/dtbasat.cc  | 53 +++++++++++++++++++++++----------------
 src/tgbaalgos/dtgbasat.cc | 44 +++++++++++++++++++++++++++-----
 2 files changed, 70 insertions(+), 27 deletions(-)

diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index ba0f2d720..4e0de777d 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/src/tgbaalgos/dtbasat.cc
@@ -300,6 +300,18 @@ namespace spot
       sm.build_map();
       bdd ap = sm.aprec_set_of(sm.initial());
 
+      // Count the number of atomic propositions
+      int nap = 0;
+      {
+	bdd cur = ap;
+	while (cur != bddtrue)
+	  {
+	    ++nap;
+	    cur = bdd_high(cur);
+	  }
+	nap = 1 << nap;
+      }
+
       // Number all the SAT variable we may need.
       {
 	filler_dfs f(ref, d, ap, state_based);
@@ -323,27 +335,26 @@ namespace spot
       dout << "cand_size: " << d.cand_size << "\n";
 #endif
 
-      // dout << "symmetry-breaking clauses\n";
-      // int k = 1;
-      // bdd all = bddtrue;
-      // while (all != bddfalse)
-      // 	{
-      // 	  bdd s = bdd_satoneset(all, ap, bddfalse);
-      // 	  all -= s;
-      // 	  for (int q1 = 1; q1 < d.cand_size; ++q1)
-      // 	    for (int q2 = q1 + 2; q2 <= d.cand_size; ++q2)
-      // 	      if ((q1 - 1) * d.cand_size + q2 + 2 <= k)
-      // 		{
-      // 		  transition t(q1, s, q2);
-      // 		  int ti = d.transid[t];
-      // 		  dout << "¬" << t << "\n";
-      // 		  out << -ti << " 0\n";
-      // 		  ++nclauses;
-      // 		}
-      // 	  ++k;
-      // 	}
-      // if (!nclauses)
-      // 	dout << "(none)\n";
+      dout << "symmetry-breaking clauses\n";
+      int j = 0;
+      bdd all = bddtrue;
+      while (all != bddfalse)
+ 	{
+ 	  bdd s = bdd_satoneset(all, ap, bddfalse);
+ 	  all -= s;
+ 	  for (int i = 1; i < d.cand_size; ++i)
+ 	    for (int k = (i - 1) * nap + j + 3; k <= d.cand_size; ++k)
+	      {
+		transition t(i, s, k);
+		int ti = d.transid[t];
+		dout << "¬" << t << "\n";
+		out << -ti << " 0\n";
+		++nclauses;
+	      }
+ 	  ++j;
+ 	}
+      if (!nclauses)
+ 	dout << "(none)\n";
 
       dout << "(1) the candidate automaton is complete\n";
       for (int q1 = 1; q1 <= d.cand_size; ++q1)
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index 2187aba27..728931670 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -477,6 +477,17 @@ namespace spot
       sm.build_map();
       bdd ap = sm.aprec_set_of(sm.initial());
 
+      // Count the number of atomic propositions
+      int nap = 0;
+      {
+	bdd cur = ap;
+	while (cur != bddtrue)
+	  {
+	    ++nap;
+	    cur = bdd_high(cur);
+	  }
+	nap = 1 << nap;
+      }
 
       // Number all the SAT variable we may need.
       {
@@ -485,12 +496,6 @@ namespace spot
 	ref_size = f.size();
       }
 
-#if DEBUG
-      debug_dict = ref->get_dict();
-      dout << "ref_size: " << ref_size << "\n";
-      dout << "cand_size: " << d.cand_size << "\n";
-#endif
-
       // empty automaton is impossible
       if (d.cand_size == 0)
 	{
@@ -501,6 +506,33 @@ namespace spot
       // An empty line for the header
       out << "                                                 \n";
 
+#if DEBUG
+      debug_dict = ref->get_dict();
+      dout << "ref_size: " << ref_size << "\n";
+      dout << "cand_size: " << d.cand_size << "\n";
+#endif
+
+      dout << "symmetry-breaking clauses\n";
+      int j = 0;
+      bdd all = bddtrue;
+      while (all != bddfalse)
+ 	{
+ 	  bdd s = bdd_satoneset(all, ap, bddfalse);
+ 	  all -= s;
+ 	  for (int i = 1; i < d.cand_size; ++i)
+ 	    for (int k = (i - 1) * nap + j + 3; k <= d.cand_size; ++k)
+	      {
+		transition t(i, s, k);
+		int ti = d.transid[t];
+		dout << "¬" << t << "\n";
+		out << -ti << " 0\n";
+		++nclauses;
+	      }
+ 	  ++j;
+ 	}
+      if (!nclauses)
+ 	dout << "(none)\n";
+
       dout << "(8) the candidate automaton is complete\n";
       for (int q1 = 1; q1 <= d.cand_size; ++q1)
 	{