From b6fc31301ca3e88b89ebb08ff5d03fb9d5f13972 Mon Sep 17 00:00:00 2001 From: noajshu Date: Wed, 28 Feb 2024 23:11:13 +0000 Subject: [PATCH] add test for weighted search with p > 0.5 --- doc/python_api_reference_vDev.md | 45 +++++++++++++++++++------ doc/stim.pyi | 45 +++++++++++++++++++------ glue/python/src/stim/__init__.pyi | 45 +++++++++++++++++++------ src/stim/circuit/circuit.pybind.cc | 3 +- src/stim/circuit/circuit_pybind_test.py | 14 ++++++-- src/stim/search/sat/wcnf.cc | 17 ++++++++-- 6 files changed, 129 insertions(+), 40 deletions(-) diff --git a/doc/python_api_reference_vDev.md b/doc/python_api_reference_vDev.md index 08f08a76b..5d49c647b 100644 --- a/doc/python_api_reference_vDev.md +++ b/doc/python_api_reference_vDev.md @@ -2452,6 +2452,15 @@ def shortest_error_problem_as_wcnf_file( """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: + ``` + # first download nzip CASHWMaxSAT-CorePlus.zip from + # https://maxsat-evaluations.github.io/2023 + unzip CASHWMaxSAT-CorePlus.zip + time ./CASHWMaxSAT-CorePlus/bin/cashwmaxsatcoreplus -bm -m problem.wcnf + ``` Args: weighted: Defaults to False (unweighted), so that the problem is to find @@ -2473,17 +2482,31 @@ def shortest_error_problem_as_wcnf_file( 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 """ ``` diff --git a/doc/stim.pyi b/doc/stim.pyi index 4524ad17a..b2dc52e19 100644 --- a/doc/stim.pyi +++ b/doc/stim.pyi @@ -1783,6 +1783,15 @@ class Circuit: """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: + ``` + # first download nzip CASHWMaxSAT-CorePlus.zip from + # https://maxsat-evaluations.github.io/2023 + unzip CASHWMaxSAT-CorePlus.zip + time ./CASHWMaxSAT-CorePlus/bin/cashwmaxsatcoreplus -bm -m problem.wcnf + ``` Args: weighted: Defaults to False (unweighted), so that the problem is to find @@ -1804,17 +1813,31 @@ class Circuit: 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 """ def shortest_graphlike_error( self, diff --git a/glue/python/src/stim/__init__.pyi b/glue/python/src/stim/__init__.pyi index 4524ad17a..b2dc52e19 100644 --- a/glue/python/src/stim/__init__.pyi +++ b/glue/python/src/stim/__init__.pyi @@ -1783,6 +1783,15 @@ class Circuit: """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: + ``` + # first download nzip CASHWMaxSAT-CorePlus.zip from + # https://maxsat-evaluations.github.io/2023 + unzip CASHWMaxSAT-CorePlus.zip + time ./CASHWMaxSAT-CorePlus/bin/cashwmaxsatcoreplus -bm -m problem.wcnf + ``` Args: weighted: Defaults to False (unweighted), so that the problem is to find @@ -1804,17 +1813,31 @@ class Circuit: 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 """ def shortest_graphlike_error( self, diff --git a/src/stim/circuit/circuit.pybind.cc b/src/stim/circuit/circuit.pybind.cc index a39908951..6f73a3c76 100644 --- a/src/stim/circuit/circuit.pybind.cc +++ b/src/stim/circuit/circuit.pybind.cc @@ -1986,7 +1986,8 @@ void stim_pybind::pybind_circuit_methods(pybind11::module &, pybind11::class_ 0.5 and invert + // the weight so that the clause decreases the overall cost when the + // error is active. + clause.add_var(err_x); + clause.weight = -std::log((1 - p) / p); + } instance.add_clause(clause); } ++error_index;