From da17c79be4e8ec1ccc6e76eee27b383c42ee5312 Mon Sep 17 00:00:00 2001
From: noajshu <shutty@google.com>
Date: Wed, 28 Feb 2024 00:08:18 +0000
Subject: [PATCH] Fix a bug in CNF -- was missing the constraints for detectors
 to be inactive

---
 src/stim/circuit/circuit_pybind_test.py |  4 ++--
 src/stim/search/sat/wcnf.cc             |  9 +++++++++
 src/stim/search/sat/wcnf.test.cc        | 26 +++++++++++++++----------
 3 files changed, 27 insertions(+), 12 deletions(-)

diff --git a/src/stim/circuit/circuit_pybind_test.py b/src/stim/circuit/circuit_pybind_test.py
index f71150338..2236326fa 100644
--- a/src/stim/circuit/circuit_pybind_test.py
+++ b/src/stim/circuit/circuit_pybind_test.py
@@ -837,9 +837,9 @@ def test_shortest_undetectable_logical_error_wcnf():
         DETECTOR rec[-1] rec[-2]
     """)
     wcnf_str = c.shortest_undetectable_logical_error_wcnf()
-    assert wcnf_str == 'p wcnf 2 3 4\n1 -1 0\n1 -2 0\n4 2 0\n'
+    assert wcnf_str == 'p wcnf 2 4 5\n1 -1 0\n1 -2 0\n5 -1 0\n5 2 0\n'
     wcnf_str = c.shortest_undetectable_logical_error_wcnf(num_distinct_weights=2)
-    assert wcnf_str == 'p wcnf 2 3 7\n1 -1 0\n2 -2 0\n7 2 0\n'
+    assert wcnf_str == 'p wcnf 2 4 9\n1 -1 0\n2 -2 0\n9 -1 0\n9 2 0\n'
 
 def test_shortest_graphlike_error_ignore():
     c = stim.Circuit("""
diff --git a/src/stim/search/sat/wcnf.cc b/src/stim/search/sat/wcnf.cc
index c4a3078ca..88707abad 100644
--- a/src/stim/search/sat/wcnf.cc
+++ b/src/stim/search/sat/wcnf.cc
@@ -208,6 +208,15 @@ std::string stim::shortest_undetectable_logical_error_wcnf(const DetectorErrorMo
       }
       ++error_index;
   });
+  assert(error_index == num_errors);
+
+  // Add a hard clause for each detector to be inactive
+  for (size_t d=0; d<num_detectors; ++d) {
+      Clause clause;
+      if (detectors_activated[d].variable == BOOL_LITERAL_FALSE) continue;
+      clause.add_var(~detectors_activated[d]);
+      instance.add_clause(clause);
+  }
 
   // Add a hard clause for any observable to be flipped
   Clause clause;
diff --git a/src/stim/search/sat/wcnf.test.cc b/src/stim/search/sat/wcnf.test.cc
index ccac79892..6a4b86279 100644
--- a/src/stim/search/sat/wcnf.test.cc
+++ b/src/stim/search/sat/wcnf.test.cc
@@ -27,23 +27,29 @@ TEST(shortest_undetectable_logical_error_wcnf, single_detector_single_observable
   // hard clause x != (0, 1, 0)
   // hard clause x != (1, 0, 0)
   // hard clause x != (1, 1, 1)
+  // Plus 1 hard clause to ensure detector is not flipped
+  // hard clause -x_2
   // Plus 1 hard clause to ensure an observable is flipped:
   // hard clause x_0
-  // This gives a total of 7 clauses
-  // The top value should be at least 1 + 1 + 1 = 3. In our implementation ends up being 8.
+  // This gives a total of 8 clauses
+  // The top value should be at least 1 + 1 + 1 = 3. In our implementation ends up being 9.
   std::stringstream expected;
   // WDIMACS header format: p wcnf nbvar nbclauses top
-  expected << "p wcnf 3 7 8\n";
+  expected << "p wcnf 3 8 9\n";
   // Soft clause
-  expected << "1 -0\n";
+  expected << "1 -1 0\n";
   // Hard clauses
-  expected << "8 0 1 -2\n";
-  expected << "8 0 -1 2\n";
-  expected << "8 -0 1 2\n";
-  expected << "8 -0 -1 -2\n";
+  expected << "9 1 2 -3 0\n";
+  expected << "9 1 -2 3 0\n";
+  expected << "9 -1 2 3 0\n";
+  expected << "9 -1 -2 -3 0\n";
   // Soft clause
-  expected << "1 -1\n";
+  expected << "1 -2 0\n";
+  // Hard clause for the detector not to be flipped
+  expected << "9 -3 0\n";
   // Hard clause for the observable flipped
-  expected << "8 0\n";
+  expected << "9 1 0\n";
   ASSERT_EQ(wcnf, expected.str());
+  // The optimal value of this wcnf file should be 2, but we don't have
+  // a maxSAT solver to be able to test it here.
 }