Skip to content

Commit

Permalink
Add stim.Circuit.{shortest,likeliest}_error_sat_problem (#703)
Browse files Browse the repository at this point in the history
## Summary
Adds a generator that outputs a .wcnf file string in [WDIMACS
format](http://www.maxhs.org/docs/wdimacs.html).
Added a few tests as well.

## Demo for the surface code
Here is a demo:

**Step 1:** Generate the WCNF file
```python
import stim
c = stim.Circuit.generated(
            "surface_code:rotated_memory_z",
            distance=5,
            rounds=2,
            after_clifford_depolarization=0.001,
)
wcnf = c.shortest_error_sat_problem()
with open('d5problem.wcnf', 'w') as outfile:
    outfile.write(wcnf)
```

**Step 2:** Fetch a solver from the [2023 maxSAT
competition](https://maxsat-evaluations.github.io/2023/)
```bash
wget https://maxsat-evaluations.github.io/2023/mse23-solver-src/exact/CASHWMaxSAT-CorePlus.zip
unzip CASHWMaxSAT-CorePlus.zip
```

**Step 3:** Run the solver on the produced file
```bash
time ./CASHWMaxSAT-CorePlus/bin/cashwmaxsatcoreplus -bm -m d5problem.wcnf 
c Parsing MaxSAT file...
c Using SCIP solver, version 8.0.3, https://www.scipopt.org
c scip_time = 0.000000
c Starting SCIP solver in a separate thread (with time-limit = 0s) ...
c Using COMiniSatPS SAT solver by Chanseok Oh (2016)
o 5
c ============================[  Problem Statistics ]============================
c |  Number of variables:           995                                         |
c |  Number of clauses:            4377 (incl.            5 soft in queue)      |
c ===============================================================================
c Optimal solution: 5
c _______________________________________________________________________________
c 
c restarts               : 881
c conflicts              : 88351          (20350 /sec)
c decisions              : 257865         (0.00 % random) (59394 /sec)
c propagations           : 6079046        (1400176 /sec)
c conflict literals      : 4980307        (6.84 % deleted)
c =======================[ UWrMaxSat resources usage ]===========================
c Memory used            : 164.00 MB
c CPU time               : 4.34163 s
c Wall clock time        : 3 s
c OptExp Enc: Srt/BDD/Add: 12 0 0
c _______________________________________________________________________________
v 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000110010100001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010100000100010000010010000000000001
s OPTIMUM FOUND

real	0m2.215s
user	0m4.345s
sys	0m0.051s
```

## Verifying distances of several quasicyclic codes
I ran this on some circuits from [this
paper](https://arxiv.org/pdf/2308.07915.pdf), with help from
@oscarhiggott to generate the circuits.
The log file is attached below:

[n72_n90_n103_quasicyclic_codes_have_expected_distances_6_8_8.txt](https://github.com/quantumlib/Stim/files/14427119/n72_n90_n103_quasicyclic_codes_have_expected_distances_6_8_8.txt)
So far, it has proven that the n=72, n=29, and n=103 circuits have the
expected distance reported in [the
paper](https://arxiv.org/pdf/2308.07915.pdf).
I am still running solvers on the n=144 and n=288 cases. My computer got
rebooted so I had to start over. I am cautiously optimistic that the
solvers will finish within a few weeks.
  • Loading branch information
noajshu authored Mar 18, 2024
1 parent 2161fc9 commit 26416fc
Showing 13 changed files with 1,255 additions and 9 deletions.
163 changes: 163 additions & 0 deletions doc/python_api_reference_vDev.md
Original file line number Diff line number Diff line change
@@ -40,6 +40,7 @@ API references for stable versions are kept on the [stim github wiki](https://gi
- [`stim.Circuit.has_all_flows`](#stim.Circuit.has_all_flows)
- [`stim.Circuit.has_flow`](#stim.Circuit.has_flow)
- [`stim.Circuit.inverse`](#stim.Circuit.inverse)
- [`stim.Circuit.likeliest_error_sat_problem`](#stim.Circuit.likeliest_error_sat_problem)
- [`stim.Circuit.num_detectors`](#stim.Circuit.num_detectors)
- [`stim.Circuit.num_measurements`](#stim.Circuit.num_measurements)
- [`stim.Circuit.num_observables`](#stim.Circuit.num_observables)
@@ -48,6 +49,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_sat_problem`](#stim.Circuit.shortest_error_sat_problem)
- [`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)
@@ -2342,6 +2344,93 @@ def inverse(
"""
```

<a name="stim.Circuit.likeliest_error_sat_problem"></a>
```python
# stim.Circuit.likeliest_error_sat_problem

# (in class stim.Circuit)
def likeliest_error_sat_problem(
self,
*,
quantization: int = 100,
format: str = 'WDIMACS',
) -> str:
"""Makes a maxSAT problem of the circuit's most likely undetectable logical
error, that other tools can solve.
The output is a string describing the maxSAT problem in WDIMACS format
(see https://maxhs.org/docs/wdimacs.html). The optimal solution to the
problem is the highest likelihood set of error mechanisms that combine to
flip any logical observable while producing no detection events).
If there are any errors with probability p > 0.5, they are inverted so
that the resulting weight ends up being positive. If there are errors
with weight close or equal to 0.5, they can end up with 0 weight meaning
that they can be included or not in the solution with no affect on the
likelihood.
There are many tools that can solve maxSAT problems in WDIMACS format.
One quick way to get started is to install pysat by running this BASH
terminal command:
pip install python-sat
Afterwards, you can run the included maxSAT solver "RC2" with this
Python code:
from pysat.examples.rc2 import RC2
from pysat.formula import WCNF
wcnf = WCNF(from_string="p wcnf 1 2 3\n3 -1 0\n3 1 0\n")
with RC2(wcnf) as rc2:
print(rc2.compute())
print(rc2.cost)
Much faster solvers are available online. For example, you can download
one of the entries in the 2023 maxSAT competition (see
https://maxsat-evaluations.github.io/2023) and run it on your problem by
running these BASH terminal commands:
wget https://maxsat-evaluations.github.io/2023/mse23-solver-src/exact/CASHWMaxSAT-CorePlus.zip
unzip CASHWMaxSAT-CorePlus.zip
./CASHWMaxSAT-CorePlus/bin/cashwmaxsatcoreplus -bm -m your_problem.wcnf
Args:
format: Defaults to "WDIMACS", corresponding to WDIMACS format which is
described here: http://www.maxhs.org/docs/wdimacs.html
quantization: Defaults to 10. Error probabilities are converted to log-odds
and scaled/rounded to be positive integers at most this large. Setting
this argument to a larger number results in more accurate quantization
such that the returned error set should have a likelihood closer to the
true most likely solution. This comes at the cost of making some maxSAT
solvers slower.
Returns:
A string corresponding to the contents of a maxSAT problem file in the
requested format.
Examples:
>>> import stim
>>> 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.likeliest_error_sat_problem(
... quantization=1000
... ), end='')
p wcnf 2 4 4001
185 -1 0
1000 -2 0
4001 -1 0
4001 2 0
"""
```

<a name="stim.Circuit.num_detectors"></a>
```python
# stim.Circuit.num_detectors
@@ -2647,6 +2736,80 @@ def search_for_undetectable_logical_errors(
"""
```

<a name="stim.Circuit.shortest_error_sat_problem"></a>
```python
# stim.Circuit.shortest_error_sat_problem

# (in class stim.Circuit)
def shortest_error_sat_problem(
self,
*,
format: str = 'WDIMACS',
) -> str:
"""Makes a maxSAT problem of the circuit's distance, that other tools can solve.
The output is a string describing the maxSAT problem in WDIMACS format
(see https://maxhs.org/docs/wdimacs.html). The optimal solution to the
problem is the fault distance of the circuit (the minimum number of error
mechanisms that combine to flip any logical observable while producing no
detection events). This method ignores the probabilities of the error
mechanisms since it only cares about minimizing the number of errors
triggered.
There are many tools that can solve maxSAT problems in WDIMACS format.
One quick way to get started is to install pysat by running this BASH
terminal command:
pip install python-sat
Afterwards, you can run the included maxSAT solver "RC2" with this
Python code:
from pysat.examples.rc2 import RC2
from pysat.formula import WCNF
wcnf = WCNF(from_string="p wcnf 1 2 3\n3 -1 0\n3 1 0\n")
with RC2(wcnf) as rc2:
print(rc2.compute())
print(rc2.cost)
Much faster solvers are available online. For example, you can download
one of the entries in the 2023 maxSAT competition (see
https://maxsat-evaluations.github.io/2023) and run it on your problem by
running these BASH terminal commands:
wget https://maxsat-evaluations.github.io/2023/mse23-solver-src/exact/CASHWMaxSAT-CorePlus.zip
unzip CASHWMaxSAT-CorePlus.zip
./CASHWMaxSAT-CorePlus/bin/cashwmaxsatcoreplus -bm -m your_problem.wcnf
Args:
format: Defaults to "WDIMACS", corresponding to WDIMACS format which is
described here: http://www.maxhs.org/docs/wdimacs.html
Returns:
A string corresponding to the contents of a maxSAT problem file in the
requested format.
Examples:
>>> import stim
>>> 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_sat_problem(), end='')
p wcnf 2 4 5
1 -1 0
1 -2 0
5 -1 0
5 2 0
"""
```

<a name="stim.Circuit.shortest_graphlike_error"></a>
```python
# stim.Circuit.shortest_graphlike_error
147 changes: 147 additions & 0 deletions doc/stim.pyi
Original file line number Diff line number Diff line change
@@ -1718,6 +1718,86 @@ class Circuit:
H 1 0
''')
"""
def likeliest_error_sat_problem(
self,
*,
quantization: int = 100,
format: str = 'WDIMACS',
) -> str:
"""Makes a maxSAT problem of the circuit's most likely undetectable logical
error, that other tools can solve.
The output is a string describing the maxSAT problem in WDIMACS format
(see https://maxhs.org/docs/wdimacs.html). The optimal solution to the
problem is the highest likelihood set of error mechanisms that combine to
flip any logical observable while producing no detection events).
If there are any errors with probability p > 0.5, they are inverted so
that the resulting weight ends up being positive. If there are errors
with weight close or equal to 0.5, they can end up with 0 weight meaning
that they can be included or not in the solution with no affect on the
likelihood.
There are many tools that can solve maxSAT problems in WDIMACS format.
One quick way to get started is to install pysat by running this BASH
terminal command:
pip install python-sat
Afterwards, you can run the included maxSAT solver "RC2" with this
Python code:
from pysat.examples.rc2 import RC2
from pysat.formula import WCNF
wcnf = WCNF(from_string="p wcnf 1 2 3\n3 -1 0\n3 1 0\n")
with RC2(wcnf) as rc2:
print(rc2.compute())
print(rc2.cost)
Much faster solvers are available online. For example, you can download
one of the entries in the 2023 maxSAT competition (see
https://maxsat-evaluations.github.io/2023) and run it on your problem by
running these BASH terminal commands:
wget https://maxsat-evaluations.github.io/2023/mse23-solver-src/exact/CASHWMaxSAT-CorePlus.zip
unzip CASHWMaxSAT-CorePlus.zip
./CASHWMaxSAT-CorePlus/bin/cashwmaxsatcoreplus -bm -m your_problem.wcnf
Args:
format: Defaults to "WDIMACS", corresponding to WDIMACS format which is
described here: http://www.maxhs.org/docs/wdimacs.html
quantization: Defaults to 10. Error probabilities are converted to log-odds
and scaled/rounded to be positive integers at most this large. Setting
this argument to a larger number results in more accurate quantization
such that the returned error set should have a likelihood closer to the
true most likely solution. This comes at the cost of making some maxSAT
solvers slower.
Returns:
A string corresponding to the contents of a maxSAT problem file in the
requested format.
Examples:
>>> import stim
>>> 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.likeliest_error_sat_problem(
... quantization=1000
... ), end='')
p wcnf 2 4 4001
185 -1 0
1000 -2 0
4001 -1 0
4001 2 0
"""
@property
def num_detectors(
self,
@@ -1967,6 +2047,73 @@ class Circuit:
... )))
5
"""
def shortest_error_sat_problem(
self,
*,
format: str = 'WDIMACS',
) -> str:
"""Makes a maxSAT problem of the circuit's distance, that other tools can solve.
The output is a string describing the maxSAT problem in WDIMACS format
(see https://maxhs.org/docs/wdimacs.html). The optimal solution to the
problem is the fault distance of the circuit (the minimum number of error
mechanisms that combine to flip any logical observable while producing no
detection events). This method ignores the probabilities of the error
mechanisms since it only cares about minimizing the number of errors
triggered.
There are many tools that can solve maxSAT problems in WDIMACS format.
One quick way to get started is to install pysat by running this BASH
terminal command:
pip install python-sat
Afterwards, you can run the included maxSAT solver "RC2" with this
Python code:
from pysat.examples.rc2 import RC2
from pysat.formula import WCNF
wcnf = WCNF(from_string="p wcnf 1 2 3\n3 -1 0\n3 1 0\n")
with RC2(wcnf) as rc2:
print(rc2.compute())
print(rc2.cost)
Much faster solvers are available online. For example, you can download
one of the entries in the 2023 maxSAT competition (see
https://maxsat-evaluations.github.io/2023) and run it on your problem by
running these BASH terminal commands:
wget https://maxsat-evaluations.github.io/2023/mse23-solver-src/exact/CASHWMaxSAT-CorePlus.zip
unzip CASHWMaxSAT-CorePlus.zip
./CASHWMaxSAT-CorePlus/bin/cashwmaxsatcoreplus -bm -m your_problem.wcnf
Args:
format: Defaults to "WDIMACS", corresponding to WDIMACS format which is
described here: http://www.maxhs.org/docs/wdimacs.html
Returns:
A string corresponding to the contents of a maxSAT problem file in the
requested format.
Examples:
>>> import stim
>>> 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_sat_problem(), end='')
p wcnf 2 4 5
1 -1 0
1 -2 0
5 -1 0
5 2 0
"""
def shortest_graphlike_error(
self,
*,
1 change: 1 addition & 0 deletions file_lists/source_files_no_main
Original file line number Diff line number Diff line change
@@ -77,6 +77,7 @@ src/stim/search/hyper/edge.cc
src/stim/search/hyper/graph.cc
src/stim/search/hyper/node.cc
src/stim/search/hyper/search_state.cc
src/stim/search/sat/wcnf.cc
src/stim/simulators/error_analyzer.cc
src/stim/simulators/error_matcher.cc
src/stim/simulators/force_streaming.cc
1 change: 1 addition & 0 deletions file_lists/test_files
Original file line number Diff line number Diff line change
@@ -57,6 +57,7 @@ src/stim/search/hyper/edge.test.cc
src/stim/search/hyper/graph.test.cc
src/stim/search/hyper/node.test.cc
src/stim/search/hyper/search_state.test.cc
src/stim/search/sat/wcnf.test.cc
src/stim/simulators/count_determined_measurements.test.cc
src/stim/simulators/dem_sampler.test.cc
src/stim/simulators/error_analyzer.test.cc
Loading

0 comments on commit 26416fc

Please sign in to comment.