QDistSAT

Benchmark SAT and MaxSAT solvers on minimum-distance search for CSS / QLDPC codes, using parity-check matrices Hx, Hz and logical bases Gx, Gz.

Matrix file layout and attribution: see NOTICE.

License: GPL-3.0-or-later (LICENSE).

Quick start

Clone with HTTPS or SSH (pick one):

# HTTPS — works everywhere; GitHub may prompt for a personal access token
git clone https://github.com/guluchen/QDistSAT.git

# SSH — if you use GitHub SSH keys (no username/password prompt)
git clone git@github.com:guluchen/QDistSAT.git

Linux (Debian / Ubuntu)

Minimal Python on Debian often lacks venv and blocks system-wide pip (PEP 668). Install once:

sudo apt install -y python3-venv python3-pip git make g++ zlib1g-dev libgmp-dev libm4ri-dev
# if `python3 -m venv` still fails, match your version, e.g.:
# sudo apt install -y python3.12-venv

Install and run

cd QDistSAT

# if a previous `venv` creation failed, remove it first:
# rm -rf venv

python3 -m venv venv
source venv/bin/activate   # required on Debian/Ubuntu (PEP 668 blocks system pip)
python3 -m pip install --upgrade pip
python3 -m pip install -e ".[dev]"

# full benchmark stack (must run inside venv — uses venv/bin/python3, not /usr/bin/python3)
python3 scripts/install_benchmark_deps.py
python3 scripts/install_benchmark_deps.py --list   # distqldpc, maxcdcl, codedistance, dist_m4ri
# ./bin/distqldpc data/BB/BB_108_8_10   # smoke test

# logical bases (if Gx/Gz missing; requires pip install above)
precompute-logicals BB_108_8_10 --benchmark-dir data

# benchmark default: all PySAT backends + distqldpc + codedistance (cd-* ×4)
python3 benchmarks/benchmark_solver_performance.py --stem BB_108_8_10 -d 10
# narrower run: --solvers rc2-glucose42 maxcdcl distqldpc
# distqldpc: two runs per stem; codedistance: four cd-* (skip if pip/binary missing)

Use python3 (not bare python) on Debian unless you installed python-is-python3. Inside an active venv, python also works after pip install succeeds.

On macOS, MSE linux_elf solvers (e.g. maxcdcl) are skipped; use Linux or Dockerfile.bench.

Benchmark dependencies

PySAT SAT/RC2 solvers work after pip install -e ".[dev]" only. For the full benchmark stack (recommended on Linux servers):

python3 scripts/install_benchmark_deps.py
python3 scripts/install_benchmark_deps.py --list

This installs by default:

Component	How
z3py, cvc5	pip install cvc5 z3-solver
codedistance, ortools	pip install -e ".[comparison]"
dist_m4ri (cd-m4ri-cc)	scripts/install_dist_m4ri.py → bin/dist_m4ri (libm4ri-dev / brew install m4ri)
maxcdcl, evalmaxsat, cashw-*, …	MSE zip download (Linux x86_64 only)
open-wbo	compiled locally (libgmp-dev / brew install gmp)
distqldpc	clone + make → bin/distqldpc

On macOS, MSE linux_elf binaries install but are skipped at run time; open-wbo, DistQLDPC, and dist-m4ri still work. Debian system packages: git make g++ zlib1g-dev libgmp-dev libm4ri-dev.

Fine-grained installs:

You want	Command
Everything (default)	python3 scripts/install_benchmark_deps.py
Skip codeDistance / dist-m4ri	python3 scripts/install_benchmark_deps.py --no-comparison
SMT only	pip install -e ".[benchmark]" or pip install z3-solver cvc5
MaxSAT + DistQLDPC only	python3 scripts/download_maxsat_solvers.py --bench
One MaxSAT solver	python3 scripts/download_maxsat_solvers.py --only maxcdcl
DistQLDPC only	python3 scripts/install_distqldpc.py
codeDistance pip only	pip install -e ".[comparison]"
dist-m4ri only	python3 scripts/install_dist_m4ri.py

codeDistance comparison (default: codedistance)

Default --solvers includes codedistance (runs cd-gurobi, cd-mip-scip, cd-m4ri-cc, cd-magma). Install via install_benchmark_deps.py; missing deps show as skipped rows, not a hard error.

python3 benchmarks/benchmark_solver_performance.py --stem BB_72_12_6 -d 6 \
  --solvers codedistance   # only the four cd-* backends

GurobiDist needs a Gurobi license; magmaMinWord needs the magma binary on PATH, or:

export MAGMA_HOME=/home/path/to/magma   # directory containing magma executable
# or: export QEECC_SAT_MAGMA=/full/path/to/magma

Details: bin/maxsat/README.md.

Input data

data/{batch}/{STEM}_Hx.txt, _Hz.txt, _Gx.txt, _Gz.txt (batches BB, BB2, LP, LP2, QT, QT2) — see data/README.md and NOTICE.

Main commands

Command	Purpose
precompute-logicals STEM	Write Gx / Gz from Hx / Hz
python3 benchmarks/benchmark_solver_performance.py …	Multi-solver distance benchmark
python3 scripts/install_benchmark_deps.py	Install SMT + MaxSAT + DistQLDPC + codeDistance + dist-m4ri
python3 scripts/download_maxsat_solvers.py --bench	MaxSAT + DistQLDPC only
./scripts/run_benchmark_stems_dir.sh data	All batch subdirs + log
./scripts/run_benchmark_stems_dir.sh data/BB	One batch folder + log

python3 benchmarks/benchmark_solver_performance.py --list-solvers
python3 scripts/parse_benchmark_log_to_latex.py logs/your_run.log

Repository layout

QDistSAT/
├── src/qecc_sat/              # Library (pip install -e .)
│   ├── sat_solver.py          # PySAT backends
│   ├── maxsat_*.py            # RC2 + external MaxSAT
│   ├── qecc_distance.py       # Distance API
│   ├── distance/              # Encodings used by the benchmark
│   ├── io.py                  # Matrix I/O
│   ├── literature_distances.py
│   └── cli/precompute_logical_bases.py
├── data/                      # Benchmark matrices by batch (BB, LP, QT, …; see NOTICE)
├── benchmarks/
│   └── benchmark_solver_performance.py
├── scripts/                   # install_benchmark_deps, MaxSAT download, LaTeX
├── tests/
├── bin/maxsat/                # manifest + README (binaries gitignored)
├── LICENSE                    # GPL-3.0-or-later
├── NOTICE                     # Matrix + third-party attribution
└── docs/REPO_SCOPE.md

Development

source venv/bin/activate   # after python3 -m venv venv
python3 -m pip install -e ".[dev]"
python3 -m pytest tests/ -q

See docs/PUBLISHING.md and docs/REPO_SCOPE.md.