address comments, refactor so there is a (weighted: bool and num_dist…

…inct_weights: 1)
quantumlib · Feb 28, 2024 · e55ae98 · e55ae98
1 parent da17c79
commit e55ae98
Show file tree

Hide file tree

Showing 8 changed files with 213 additions and 54 deletions.
diff --git a/doc/python_api_reference_vDev.md b/doc/python_api_reference_vDev.md
@@ -46,6 +46,7 @@ API references for stable versions are kept on the [stim github wiki](https://gi
     - [`stim.Circuit.num_ticks`](#stim.Circuit.num_ticks)
     - [`stim.Circuit.reference_sample`](#stim.Circuit.reference_sample)
     - [`stim.Circuit.search_for_undetectable_logical_errors`](#stim.Circuit.search_for_undetectable_logical_errors)
+    - [`stim.Circuit.shortest_error_problem_as_wcnf_file`](#stim.Circuit.shortest_error_problem_as_wcnf_file)
     - [`stim.Circuit.shortest_graphlike_error`](#stim.Circuit.shortest_graphlike_error)
     - [`stim.Circuit.to_file`](#stim.Circuit.to_file)
     - [`stim.Circuit.to_qasm`](#stim.Circuit.to_qasm)
@@ -2437,6 +2438,55 @@ def search_for_undetectable_logical_errors(
     """
 ```
 
+<a name="stim.Circuit.shortest_error_problem_as_wcnf_file"></a>
+```python
+# stim.Circuit.shortest_error_problem_as_wcnf_file
+
+# (in class stim.Circuit)
+def shortest_error_problem_as_wcnf_file(
+    self,
+    *,
+    weighted: bool = False,
+    num_distinct_weights: int = 1,
+) -> str:
+    """Generates a maxSAT problem instance in WDIMACS format whose optimal value is
+    the distance of the protocol, i.e. the minimum weight of any set of errors
+    that forms an undetectable logical error.
+
+    Args:
+        weighted: Defaults to False (unweighted), so that the problem is to find
+        the minimum size set of errors that leads to an undetectable logical
+        error.
+        num_distinct_weights: Defaults to 1. If weighted==False, must set
+        num_distinct_weights to 1. If weighted==True, num_distinct_weights can be
+        set to a value > 1. For a weighted problem, the errors will be quantized
+        into at most this many distinct weight values and the sum of the weights
+        will be minimized rather than the cardinality of the set of errors. For
+        a reasonably large quantization (num_distinct_weights > 100), the .wcnf
+        file solution should be the (approximately) most likely undetectable
+        logical error. Note, however, that maxSAT solvers often become slower
+        when many distinct weights are provided, so for computing the distance
+        it is better to use the default quantization num_distinct_weights = 1.
+
+    Returns:
+        A WCNF file in [WDIMACS format](http://www.maxhs.org/docs/wdimacs.html)
+
+    Examples:
+        >>> import stim
+        >>> circuit = stim.Circuit.generated(
+        ...     "surface_code:rotated_memory_x",
+        ...     rounds=5,
+        ...     distance=5,
+        ...     after_clifford_depolarization=0.001)
+        >>> print(circuit.shortest_undetectable_logical_error_wcnf(
+                        num_distinct_weights=1))
+        ....
+        >>> print(circuit.shortest_undetectable_logical_error_wcnf(
+                        num_distinct_weights=10))
+        ....
+    """
+```
+
 <a name="stim.Circuit.shortest_graphlike_error"></a>
 ```python
 # stim.Circuit.shortest_graphlike_error

diff --git a/doc/stim.pyi b/doc/stim.pyi
@@ -1774,6 +1774,48 @@ class Circuit:
             ... )))
             5
         """
+    def shortest_error_problem_as_wcnf_file(
+        self,
+        *,
+        weighted: bool = False,
+        num_distinct_weights: int = 1,
+    ) -> str:
+        """Generates a maxSAT problem instance in WDIMACS format whose optimal value is
+        the distance of the protocol, i.e. the minimum weight of any set of errors
+        that forms an undetectable logical error.
+
+        Args:
+            weighted: Defaults to False (unweighted), so that the problem is to find
+            the minimum size set of errors that leads to an undetectable logical
+            error.
+            num_distinct_weights: Defaults to 1. If weighted==False, must set
+            num_distinct_weights to 1. If weighted==True, num_distinct_weights can be
+            set to a value > 1. For a weighted problem, the errors will be quantized
+            into at most this many distinct weight values and the sum of the weights
+            will be minimized rather than the cardinality of the set of errors. For
+            a reasonably large quantization (num_distinct_weights > 100), the .wcnf
+            file solution should be the (approximately) most likely undetectable
+            logical error. Note, however, that maxSAT solvers often become slower
+            when many distinct weights are provided, so for computing the distance
+            it is better to use the default quantization num_distinct_weights = 1.
+
+        Returns:
+            A WCNF file in [WDIMACS format](http://www.maxhs.org/docs/wdimacs.html)
+
+        Examples:
+            >>> import stim
+            >>> circuit = stim.Circuit.generated(
+            ...     "surface_code:rotated_memory_x",
+            ...     rounds=5,
+            ...     distance=5,
+            ...     after_clifford_depolarization=0.001)
+            >>> print(circuit.shortest_undetectable_logical_error_wcnf(
+                            num_distinct_weights=1))
+            ....
+            >>> print(circuit.shortest_undetectable_logical_error_wcnf(
+                            num_distinct_weights=10))
+            ....
+        """
     def shortest_graphlike_error(
         self,
         *,

diff --git a/glue/python/src/stim/__init__.pyi b/glue/python/src/stim/__init__.pyi
@@ -1774,6 +1774,48 @@ class Circuit:
             ... )))
             5
         """
+    def shortest_error_problem_as_wcnf_file(
+        self,
+        *,
+        weighted: bool = False,
+        num_distinct_weights: int = 1,
+    ) -> str:
+        """Generates a maxSAT problem instance in WDIMACS format whose optimal value is
+        the distance of the protocol, i.e. the minimum weight of any set of errors
+        that forms an undetectable logical error.
+
+        Args:
+            weighted: Defaults to False (unweighted), so that the problem is to find
+            the minimum size set of errors that leads to an undetectable logical
+            error.
+            num_distinct_weights: Defaults to 1. If weighted==False, must set
+            num_distinct_weights to 1. If weighted==True, num_distinct_weights can be
+            set to a value > 1. For a weighted problem, the errors will be quantized
+            into at most this many distinct weight values and the sum of the weights
+            will be minimized rather than the cardinality of the set of errors. For
+            a reasonably large quantization (num_distinct_weights > 100), the .wcnf
+            file solution should be the (approximately) most likely undetectable
+            logical error. Note, however, that maxSAT solvers often become slower
+            when many distinct weights are provided, so for computing the distance
+            it is better to use the default quantization num_distinct_weights = 1.
+
+        Returns:
+            A WCNF file in [WDIMACS format](http://www.maxhs.org/docs/wdimacs.html)
+
+        Examples:
+            >>> import stim
+            >>> circuit = stim.Circuit.generated(
+            ...     "surface_code:rotated_memory_x",
+            ...     rounds=5,
+            ...     distance=5,
+            ...     after_clifford_depolarization=0.001)
+            >>> print(circuit.shortest_undetectable_logical_error_wcnf(
+                            num_distinct_weights=1))
+            ....
+            >>> print(circuit.shortest_undetectable_logical_error_wcnf(
+                            num_distinct_weights=10))
+            ....
+        """
     def shortest_graphlike_error(
         self,
         *,

diff --git a/src/stim/circuit/circuit.pybind.cc b/src/stim/circuit/circuit.pybind.cc
@@ -80,9 +80,9 @@ std::vector<ExplainedError> py_find_undetectable_logical_error(
     return ErrorMatcher::explain_errors_from_circuit(self, &filter, reduce_to_representative);
 }
 
-std::string py_shortest_undetectable_logical_error_wcnf(const Circuit& self, size_t num_distinct_weights) {
+std::string py_shortest_error_problem_as_wcnf_file(const Circuit& self, bool weighted, size_t num_distinct_weights) {
     DetectorErrorModel dem = ErrorAnalyzer::circuit_to_detector_error_model(self, false, true, false, 1, false, false);
-    return stim::shortest_undetectable_logical_error_wcnf(dem, num_distinct_weights);
+    return stim::shortest_error_problem_as_wcnf_file(dem, weighted, num_distinct_weights);
 }
 
 void circuit_append(
@@ -1973,41 +1973,69 @@ void stim_pybind::pybind_circuit_methods(pybind11::module &, pybind11::class_<Ci
             .data());
 
     c.def(
-        "shortest_undetectable_logical_error_wcnf",
-        &py_shortest_undetectable_logical_error_wcnf,
+        "shortest_error_problem_as_wcnf_file",
+        &py_shortest_error_problem_as_wcnf_file,
         pybind11::kw_only(),
+        pybind11::arg("weighted") = false,
         pybind11::arg("num_distinct_weights") = 1,
         clean_doc_string(R"DOC(
             Generates a maxSAT problem instance in WDIMACS format whose optimal value is
             the distance of the protocol, i.e. the minimum weight of any set of errors
             that forms an undetectable logical error.
+            FYI: here is how you could fetch a solver from the
+            [2023 maxSAT competition](https://maxsat-evaluations.github.io/2023/) and
+            run the solver on a file produced with this method:
+            ```
+            wget https://maxsat-evaluations.github.io/2023/mse23-solver-src/exact/CASHWMaxSAT-CorePlus.zip
+            unzip CASHWMaxSAT-CorePlus.zip
+            time ./CASHWMaxSAT-CorePlus/bin/cashwmaxsatcoreplus -bm -m problem.wcnf 
+            ```
 
             Args:
-                num_distinct_weights: Defaults to 1 (unweighted). If > 1, the weights of
-                the errors will be quantized accordingly and the sum of the weights will
-                be minimized. For a reasonably large quantization (num_distinct_weights >
-                100), the .wcnf file solution should be the (approximately) most likely
-                undetectable logical error. Note, however, that maxSAT solvers often
-                become slower when many distinct weights are provided, so for computing
-                the distance it is better to use the default quantization
-                num_distinct_weights = 1.
+                weighted: Defaults to False (unweighted), so that the problem is to find
+                the minimum size set of errors that leads to an undetectable logical
+                error.
+                num_distinct_weights: Defaults to 1. If weighted==False, must set
+                num_distinct_weights to 1. If weighted==True, num_distinct_weights can be
+                set to a value > 1. For a weighted problem, the errors will be quantized
+                into at most this many distinct weight values and the sum of the weights
+                will be minimized rather than the cardinality of the set of errors. For
+                a reasonably large quantization (num_distinct_weights > 100), the .wcnf
+                file solution should be the (approximately) most likely undetectable
+                logical error. Note, however, that maxSAT solvers often become slower
+                when many distinct weights are provided, so for computing the distance
+                it is better to use the default quantization num_distinct_weights = 1.
 
             Returns:
                 A WCNF file in [WDIMACS format](http://www.maxhs.org/docs/wdimacs.html)
 
             Examples:
                 >>> import stim
-                >>> circuit = stim.Circuit.generated(
-                ...     "surface_code:rotated_memory_x",
-                ...     rounds=5,
-                ...     distance=5,
-                ...     after_clifford_depolarization=0.001)
-                >>> print(circuit.shortest_undetectable_logical_error_wcnf(
-                                num_distinct_weights=1))
-                ....
-                >>> print(circuit.shortest_undetectable_logical_error_wcnf(
-                                num_distinct_weights=10))
-                ....
+                >>> circuit = stim.Circuit("""
+                ...     X_ERROR(0.1) 0
+                ...     M 0
+                ...     OBSERVABLE_INCLUDE(0) rec[-1]
+                ...     X_ERROR(0.4) 0
+                ...     M 0
+                ...     DETECTOR rec[-1] rec[-2]
+                ... """)
+                >>> print(circuit.shortest_error_problem_as_wcnf_file())
+                p wcnf 2 4 5
+                1 -1 0
+                1 -2 0
+                5 -1 0
+                5 2 0
+
+                >>> 
+                >>> print(circuit.shortest_error_problem_as_wcnf_file(
+                ...   weighted=True,
+                ...   num_distinct_weights=10
+                ... ))
+                p wcnf 2 4 41
+                2 -1 0
+                10 -2 0
+                41 -1 0
+                41 2 0
         )DOC")
             .data());
     c.def(

diff --git a/src/stim/circuit/circuit_pybind_test.py b/src/stim/circuit/circuit_pybind_test.py
@@ -827,7 +827,7 @@ def test_search_for_undetectable_logical_errors_msgs():
             dont_explore_detection_event_sets_with_size_above=4,
         )
 
-def test_shortest_undetectable_logical_error_wcnf():
+def test_shortest_error_problem_as_wcnf_file():
     c = stim.Circuit("""
         X_ERROR(0.1) 0
         M 0
@@ -836,9 +836,11 @@ def test_shortest_undetectable_logical_error_wcnf():
         M 0
         DETECTOR rec[-1] rec[-2]
     """)
-    wcnf_str = c.shortest_undetectable_logical_error_wcnf()
+    wcnf_str = c.shortest_error_problem_as_wcnf_file()
+    print(wcnf_str)
     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)
+    wcnf_str = c.shortest_error_problem_as_wcnf_file(num_distinct_weights=2)
+    print(wcnf_str)
     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():

diff --git a/src/stim/search/sat/wcnf.cc b/src/stim/search/sat/wcnf.cc
@@ -21,8 +21,11 @@ using namespace stim;
 typedef double Weight;
 constexpr Weight HARD_CLAUSE_WEIGHT = -1.0;
 
+const std::string UNSAT_WCNF_STR = "p wcnf 1 2 3\n3 -1 0\n3 1 0\n";
+
 constexpr size_t BOOL_LITERAL_FALSE = SIZE_MAX - 1;
 constexpr size_t BOOL_LITERAL_TRUE = SIZE_MAX;
+
 struct BoolRef {
   size_t variable = BOOL_LITERAL_FALSE;
   bool negated = false;
@@ -118,9 +121,11 @@ struct MaxSATInstance {
     return std::max(1ul, (size_t)std::round(weight / max_weight * (double)num_distinct_weights));
   }
 
-  std::string to_wdimacs(size_t num_distinct_weights=1) {
+  std::string to_wdimacs(bool weighted, size_t num_distinct_weights) {
     if (num_distinct_weights < 1) {
       throw std::invalid_argument("There must be at least 1 distinct weight value");
+    } else if (num_distinct_weights != 1 and !weighted) {
+      throw std::invalid_argument("Can only set num_distinct_weights > 1 when performing a weighted search.");
     }
     // 'top' is a special weight used to indicate a hard clause.
     // Should be at least the sum of the weights of all soft clauses plus 1.
@@ -152,30 +157,19 @@ struct MaxSATInstance {
   }
 };
 
-std::string stim::shortest_undetectable_logical_error_wcnf(const DetectorErrorModel &model, size_t num_distinct_weights) {
+std::string stim::shortest_error_problem_as_wcnf_file(
+  const DetectorErrorModel &model, bool weighted, size_t num_distinct_weights) {
   MaxSATInstance inst;
 
+  if (num_distinct_weights == 0) {
+    throw std::invalid_argument("num_distinct_weights must be >= 1");
+  }
+
   size_t num_observables = model.count_observables();
   size_t num_detectors = model.count_detectors();
   size_t num_errors = model.count_errors();
   if (num_observables == 0 or num_detectors == 0 or num_errors == 0) {
-    std::stringstream err_msg;
-    err_msg << "Failed to find any logical errors.";
-    if (num_observables == 0) {
-        err_msg << "\n    WARNING: NO OBSERVABLES. The circuit or detector error model didn't define any observables, "
-                   "making it vacuously impossible to find a logical error.";
-    }
-    if (num_detectors == 0) {
-        err_msg << "\n    WARNING: NO DETECTORS. The circuit or detector error model didn't define any detectors.";
-    }
-    if (num_errors == 0) {
-        err_msg << "\n    WARNING: NO ERRORS. The circuit or detector error model didn't include any errors, making it "
-                   "vacuously impossible to find a logical error.";
-    }
-    throw std::invalid_argument(err_msg.str());
-  }
-  if (num_distinct_weights == 0) {
-    throw std::invalid_argument("num_distinct_weights must be >= 1");
+    return UNSAT_WCNF_STR;
   }
 
   MaxSATInstance instance;
@@ -225,5 +219,5 @@ std::string stim::shortest_undetectable_logical_error_wcnf(const DetectorErrorMo
   }
   instance.add_clause(clause);
 
-  return instance.to_wdimacs(num_distinct_weights);
+  return instance.to_wdimacs(weighted, num_distinct_weights);
 }
diff --git a/src/stim/search/sat/wcnf.h b/src/stim/search/sat/wcnf.h
@@ -28,7 +28,8 @@ namespace stim {
 ///     users must separately manage the process of selecting and running the solver. This approach is designed to
 ///     sidestep the need for direct integration with any particular solver and allow
 ///     for experimentation with different solvers to achieve the best performance.
-std::string shortest_undetectable_logical_error_wcnf(const DetectorErrorModel &model, size_t num_distinct_weights=1);
+std::string shortest_error_problem_as_wcnf_file(
+  const DetectorErrorModel &model, bool weighted=false, size_t num_distinct_weights=1);
 
 }  // namespace stim
 

diff --git a/src/stim/search/sat/wcnf.test.cc b/src/stim/search/sat/wcnf.test.cc
@@ -3,15 +3,15 @@
 
 using namespace stim;
 
-TEST(shortest_undetectable_logical_error_wcnf, no_error) {
-    // No error.
-    ASSERT_THROW(
-        { stim::shortest_undetectable_logical_error_wcnf(DetectorErrorModel()); },
-        std::invalid_argument);
+TEST(shortest_error_problem_as_wcnf_file, no_error) {
+    // No errors. Should get an unsatisfiable formula.
+    ASSERT_EQ(
+      stim::shortest_error_problem_as_wcnf_file(DetectorErrorModel()),
+      "p wcnf 1 2 3\n3 -1 0\n3 1 0\n");
 }
 
-TEST(shortest_undetectable_logical_error_wcnf, single_detector_single_observable) {
-  std::string wcnf = stim::shortest_undetectable_logical_error_wcnf(DetectorErrorModel(R"DEM(
+TEST(shortest_error_problem_as_wcnf_file, single_detector_single_observable) {
+  std::string wcnf = stim::shortest_error_problem_as_wcnf_file(DetectorErrorModel(R"DEM(
       error(0.1) D0 L0
       error(0.1) D0
     )DEM"));