From e55ae982cf7d7aba7d12585bdb32bb5580001d4e Mon Sep 17 00:00:00 2001 From: noajshu Date: Wed, 28 Feb 2024 23:02:03 +0000 Subject: [PATCH] address comments, refactor so there is a (weighted: bool and num_distinct_weights: 1) --- doc/python_api_reference_vDev.md | 50 +++++++++++++++++ doc/stim.pyi | 42 ++++++++++++++ glue/python/src/stim/__init__.pyi | 42 ++++++++++++++ src/stim/circuit/circuit.pybind.cc | 74 +++++++++++++++++-------- src/stim/circuit/circuit_pybind_test.py | 8 ++- src/stim/search/sat/wcnf.cc | 34 +++++------- src/stim/search/sat/wcnf.h | 3 +- src/stim/search/sat/wcnf.test.cc | 14 ++--- 8 files changed, 213 insertions(+), 54 deletions(-) diff --git a/doc/python_api_reference_vDev.md b/doc/python_api_reference_vDev.md index 4a197b909..08f08a76b 100644 --- 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( """ ``` + +```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)) + .... + """ +``` + ```python # stim.Circuit.shortest_graphlike_error diff --git a/doc/stim.pyi b/doc/stim.pyi index 7e476efcc..4524ad17a 100644 --- 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 index 7e476efcc..4524ad17a 100644 --- 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 index ba29d426e..a39908951 100644 --- a/src/stim/circuit/circuit.pybind.cc +++ b/src/stim/circuit/circuit.pybind.cc @@ -80,9 +80,9 @@ std::vector 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_ 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 index 2236326fa..4624fb8ca 100644 --- 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 index 88707abad..3f55fbe83 100644 --- 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 index 6c2cfcf40..e1df03161 100644 --- 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 index 6a4b86279..61f6e29eb 100644 --- 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"));