Add stim.Circuit.{shortest,likeliest}_error_sat_problem

[noajshu]

Summary

Adds a generator that outputs a .wcnf file string in WDIMACS format.
Added a few tests as well.

Demo for the surface code

Here is a demo:

Step 1: Generate the WCNF file

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

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

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, 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
So far, it has proven that the n=72, n=29, and n=103 circuits have the expected distance reported in the paper.
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.

[Strilanc]

Looks like you need to run the regen_docs.sh script in the dev/ directory. It expects you to build and install the stim dev wheel before doing so (see the developer docs; this is easy to do with bazel).

[noajshu]

Looks like you need to run the regen_docs.sh script in the dev/ directory. It expects you to build and install the stim dev wheel before doing so (see the developer docs; this is easy to do with bazel).

Thanks, ran this and addressed all the comments.

[Strilanc]

Note: the bug in doctest_proper is intended-behavior in doctest, where you have to say <BLANKLINE> instead of having blank output lines. But I prefer the modified print statements.

[Strilanc]

Getting closer!

[noajshu]

Hi @Strilanc , Oscar had an idea that I like for the interface and I was wondering what you thought.

The idea is to split into two python functions:

minimum_cardinality_undetectable_logical_error_problem_as_maxsat_string(format)
approximately_most_probable_undetectable_logical_error_problem_as_maxsat_string(quantization_factor, format)

The idea would be to to ignore probabilities entirely in the first method and do a "best effort" approximation in the second method. "Best effort" means negation complementation and rounding to zero where it's the closest available integer.

WDYT

[Strilanc]

I think these are close enough that they might as well be the same method with a flag of some kind.

Also those names are too long. If I was naming it I'd say shortest_logical_error_as_... and most_likely_logical_error_as_....

[noajshu]

I think these are close enough that they might as well be the same method with a flag of some kind.

Also those names are too long. If I was naming it I'd say shortest_logical_error_as_... and most_likely_logical_error_as_....

I am happy to make either 2 methods with somewhat shorter names, as you suggest, or to keep it 1 method with a flag. Which solution do you prefer?

[Strilanc]

Go with the two name solution.

[noajshu]

@Strilanc despite running this:

bazel build stim_dev_wheel
pip uninstall -y stim
pip install bazel-bin/stim-0.0.dev0-py3-none-any.whl
pytest src/stim/circuit/ && ./dev/regen_docs.sh

I don't see any updates to the docs. Yet, the CI job test_generated_docs_are_fresh does not pass. Do you have any idea what could be going wrong?

[Strilanc]

The failure message i nthe CI log is

So it looks like your doctest code is invalid. The fresh-check also verifies the .pyi file runs as if it was python. You just need to make it be exactly valid (need '...' on every line including in multiline strings)

[noajshu]

Thanks for the advice!
The problem with the docstring was simply that I used:

>>> 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]
... """)

which resulted in a """ inside a multiline string that itself used """.

I replaced these with ''' and also added a check to clean_doc_string to raise an error if there are any appearances of """ to help future fledgling Stim initiates like myself.

BTW -- it seems like some of the code in a recent commit to main was not formatted with this command you shared:

find src | grep "\.\(cc\|h\|inl\)$" | grep -Pv "crumble_data.cc|gate_data_3d_texture_data.cc" | xargs clang-format -i

you might consider running it on your branch.

[Strilanc]

Because CI doesn't enforce that the code is formatted, it often drifts a bit over time.

[viathor]

Cross-reference: This PR came up as an example to answer this question on QCSE.