diff --git a/.github/workflows/checkpoint-recovery.yml b/.github/workflows/checkpoint-recovery.yml new file mode 100644 index 0000000..20e9302 --- /dev/null +++ b/.github/workflows/checkpoint-recovery.yml @@ -0,0 +1,59 @@ +name: checkpoint-recovery +on: + push: + branches: [research/100-blitz-20261016] + paths: ['.github/workflows/checkpoint-recovery.yml'] + workflow_dispatch: +permissions: + contents: read +concurrency: + group: checkpoint-recovery-${{ github.ref }} + cancel-in-progress: false +jobs: + recover: + runs-on: ubuntu-24.04 + timeout-minutes: 15 + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + persist-credentials: false + - name: Verify repository and create exact recovery materials + env: + REVIEW_BASE: 575eb1e657fc8c5d06fd56a519efd59f95dc0a2d + run: | + set -euo pipefail + mkdir -p checkpoint-recovery + git merge-base --is-ancestor "$REVIEW_BASE" HEAD + git diff --check "$REVIEW_BASE"..HEAD + git fsck --strict + git rev-parse HEAD > checkpoint-recovery/source_commit.txt + git rev-parse HEAD^{tree} > checkpoint-recovery/source_tree.txt + printf '%s\n' "$REVIEW_BASE" > checkpoint-recovery/review_base.txt + git log --format='%H %T %s' "$REVIEW_BASE"..HEAD > checkpoint-recovery/commit_ledger.txt + git diff --binary "$REVIEW_BASE"..HEAD > checkpoint-recovery/review.patch + git format-patch --stdout --binary "$REVIEW_BASE"..HEAD > checkpoint-recovery/review-series.patch + git archive --format=tar.gz --output=checkpoint-recovery/source.tar.gz HEAD + git bundle create checkpoint-recovery/source.bundle HEAD + git bundle verify checkpoint-recovery/source.bundle > checkpoint-recovery/bundle-verify.txt 2>&1 + python - <<'PY' + import hashlib, json + from pathlib import Path + root = Path('checkpoint-recovery') + files = {} + for path in sorted(root.iterdir()): + if path.is_file() and path.name != 'SHA256SUMS.json': + files[path.name] = { + 'bytes': path.stat().st_size, + 'sha256': hashlib.sha256(path.read_bytes()).hexdigest(), + } + (root / 'SHA256SUMS.json').write_text( + json.dumps(files, indent=2, sort_keys=True) + '\n', encoding='utf-8') + PY + - uses: actions/upload-artifact@v4 + with: + name: spectra-100-blitz-recovery-${{ github.sha }} + path: checkpoint-recovery/ + include-hidden-files: true + retention-days: 90 + if-no-files-found: error diff --git a/.github/workflows/itc-exam-suite.yml b/.github/workflows/itc-exam-suite.yml new file mode 100644 index 0000000..6fa53ff --- /dev/null +++ b/.github/workflows/itc-exam-suite.yml @@ -0,0 +1,130 @@ +name: itc-exam-suite +on: + push: + branches: [research/100-blitz-20261016] + paths: + - '.github/workflows/itc-exam-suite.yml' + - 'spectra/exact*.py' + - 'spectra/exam_repair.py' + - 'spectra/itc2007_exam.py' + - 'spectra/_native/exact_binary.cpp' + - 'experiments/compiled_query/exact.py' + - 'experiments/compiled_query/exact_native.cpp' + - 'experiments/compiled_query/test_exact.py' + - 'experiments/compiled_query/itc_exam_transfer.py' + - 'experiments/compiled_query/itc_exam_suite.py' + - 'experiments/compiled_query/test_itc_exam_transfer.py' + - 'experiments/compiled_query/test_itc_exam_suite.py' + - 'experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md' + - 'experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md' + workflow_dispatch: +permissions: + contents: read +concurrency: + group: itc-exam-suite-${{ github.ref }} + cancel-in-progress: false +env: + OMP_NUM_THREADS: '1' + OPENBLAS_NUM_THREADS: '1' +jobs: + suite: + name: Prospective ITC suite (${{ matrix.runner }}, Python ${{ matrix.python }}) + runs-on: ${{ matrix.runner }} + timeout-minutes: 60 + strategy: + fail-fast: false + matrix: + include: + - {runner: ubuntu-24.04, python: '3.11'} + - {runner: ubuntu-24.04, python: '3.13'} + - {runner: ubuntu-24.04-arm, python: '3.13'} + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + persist-credentials: false + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python }} + - run: python -m pip install 'build==1.3.0' 'pytest==8.4.2' + - uses: actions/checkout@v4 + with: + repository: davidvanbulck/ITC-2007-CETT + ref: ed2d4c0cf5302b77a8b321cd0380de0bb579d538 + path: upstream/ITC-2007-CETT + persist-credentials: false + - name: Validate selector and suite contracts + run: | + set -euo pipefail + python -m pytest \ + tests/public/test_exam_repair.py \ + tests/public/test_itc2007_exam.py \ + --confcutdir=tests/public -q \ + --junitxml=suite-public-contracts.xml + python -m pytest \ + experiments/compiled_query/test_exact.py \ + experiments/compiled_query/test_itc_exam_transfer.py \ + experiments/compiled_query/test_itc_exam_suite.py \ + -q -k 'auto or tiled_witnesses or itc or suite' \ + --junitxml=suite-research-contracts.xml + - name: Build and exercise the installed application API + run: | + set -euo pipefail + python -m build --wheel --outdir suite-wheel + python -m venv suite-install + suite-install/bin/python -m pip install --no-deps suite-wheel/*.whl + suite-install/bin/python -I scripts/check_exam_repair_installation.py \ + --out installed-exam-repair.json | tee installed-exam-repair.log + - name: Freeze all roles before any holdout execution + run: | + set -euo pipefail + python -m experiments.compiled_query.itc_exam_suite freeze \ + --root itc-suite-evidence \ + --upstream-root upstream/ITC-2007-CETT \ + --queries 1024 \ + --holdout-max-auto-raw-ratio 1.15 | tee freeze.log + - name: Execute and independently audit every case + run: | + set -euo pipefail + python -m experiments.compiled_query.itc_exam_suite run \ + --root itc-suite-evidence | tee run.log + python -S -m experiments.compiled_query.itc_exam_suite audit \ + --root itc-suite-evidence | tee audit.log + python - <<'PY' + import json + from pathlib import Path + result = json.loads(Path('itc-suite-evidence/suite-audit.json').read_text()) + assert result['functional_complete'] + assert result['holdout_gate_pass'], result['holdout_failures'] + roles = [case['role'] for case in result['cases']] + assert roles == ['development', 'holdout', 'holdout'] + for case in result['cases']: + assert case['queries'] == 1024 + assert case['sat'] + case['unsat'] == 1024 + assert case['auto_vs_raw_paired_median_ratio'] > 0 + print('Prospective holdout guardrail passed. Not a full timetabling claim.') + PY + - name: Preserve exact environment and source receipts + if: always() + run: | + set -euo pipefail + mkdir -p suite-receipts + git rev-parse HEAD > suite-receipts/source_commit.txt + git rev-parse HEAD^{tree} > suite-receipts/source_tree.txt + git -C upstream/ITC-2007-CETT rev-parse HEAD > suite-receipts/upstream_commit.txt + python -VV > suite-receipts/python.txt + uname -a > suite-receipts/platform.txt + lscpu > suite-receipts/cpu.txt + cp suite-public-contracts.xml suite-research-contracts.xml \ + freeze.log run.log audit.log installed-exam-repair.json \ + installed-exam-repair.log suite-receipts/ 2>/dev/null || true + - uses: actions/upload-artifact@v4 + if: always() + with: + name: itc-exam-suite-${{ matrix.runner }}-py${{ matrix.python }}-${{ github.run_id }} + path: | + itc-suite-evidence/ + suite-receipts/ + suite-wheel/ + retention-days: 90 + if-no-files-found: warn diff --git a/.github/workflows/itc-exam-transfer.yml b/.github/workflows/itc-exam-transfer.yml new file mode 100644 index 0000000..1059345 --- /dev/null +++ b/.github/workflows/itc-exam-transfer.yml @@ -0,0 +1,118 @@ +name: itc-exam-transfer +on: + push: + branches: [research/100-blitz-20261016] + paths: + - '.github/workflows/itc-exam-transfer.yml' + - 'spectra/exact*.py' + - 'spectra/exam_repair.py' + - 'spectra/itc2007_exam.py' + - 'spectra/_native/exact_binary.cpp' + - 'experiments/compiled_query/itc_exam_transfer.py' + - 'experiments/compiled_query/test_itc_exam_transfer.py' + - 'experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md' + - 'experiments/compiled_query/itc_exam_suite.py' + - 'experiments/compiled_query/test_itc_exam_suite.py' + - 'experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md' + - 'tests/public/test_exam_repair.py' + - 'tests/public/test_itc2007_exam.py' + workflow_dispatch: +permissions: + contents: read +concurrency: + group: itc-exam-transfer-${{ github.ref }} + cancel-in-progress: false +env: + OMP_NUM_THREADS: '1' + OPENBLAS_NUM_THREADS: '1' +jobs: + transfer: + name: ITC conflict-core transfer (${{ matrix.runner }}, Python ${{ matrix.python }}) + runs-on: ${{ matrix.runner }} + timeout-minutes: 45 + strategy: + fail-fast: false + matrix: + include: + - {runner: ubuntu-24.04, python: '3.11'} + - {runner: ubuntu-24.04, python: '3.13'} + - {runner: ubuntu-24.04-arm, python: '3.13'} + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + persist-credentials: false + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python }} + - name: Install the pinned test runner + run: python -m pip install 'pytest==8.4.2' + - uses: actions/checkout@v4 + with: + repository: davidvanbulck/ITC-2007-CETT + ref: ed2d4c0cf5302b77a8b321cd0380de0bb579d538 + path: upstream/ITC-2007-CETT + persist-credentials: false + - name: Check the public adapter and immutable evidence harness + run: | + set -euo pipefail + python -m pytest \ + tests/public/test_exam_repair.py \ + tests/public/test_itc2007_exam.py \ + --confcutdir=tests/public -q \ + --junitxml=transfer-public-contracts.xml + python -m pytest \ + experiments/compiled_query/test_itc_exam_transfer.py \ + -q --junitxml=transfer-research-contracts.xml + - name: Freeze the published instance only after the protocol is committed + run: | + set -euo pipefail + python -m experiments.compiled_query.itc_exam_transfer freeze \ + --root itc-transfer-evidence \ + --instance upstream/ITC-2007-CETT/examtt-instances/Instances/set9.exam \ + --solution upstream/ITC-2007-CETT/InitMethods/SolStore/set9_OBSIFeas_0.sol \ + --license upstream/ITC-2007-CETT/LICENSE \ + --queries 1024 \ + --evaluation-role development | tee freeze.log + - name: Run every exact engine and replay every answer + run: | + set -euo pipefail + python -m experiments.compiled_query.itc_exam_transfer run \ + --root itc-transfer-evidence | tee run.log + python -S -m experiments.compiled_query.itc_exam_transfer audit \ + --root itc-transfer-evidence | tee audit.log + python - <<'PY' + import json + from pathlib import Path + result = json.loads(Path('itc-transfer-evidence/audit.json').read_text()) + assert result['functional_complete'] + assert result['baseline_valid_full_itc_hard_constraints'] + assert result['queries'] == 1024 + assert result['model']['schema'] == 'spectra.itc2007.conflict_core.v1' + assert result['modes']['auto']['auto_policy'] == 'structural-v2' + assert result['modes']['auto']['selected_mode'] == 'raw' + assert result['modes']['auto']['auto_policy_reason'] == 'high_pin_density' + print('Functional transfer complete. This is not a full ITC timetable claim.') + PY + - name: Preserve exact source and environment receipts + if: always() + run: | + set -euo pipefail + mkdir -p transfer-receipts + git rev-parse HEAD > transfer-receipts/source_commit.txt + git rev-parse HEAD^{tree} > transfer-receipts/source_tree.txt + git -C upstream/ITC-2007-CETT rev-parse HEAD > transfer-receipts/upstream_commit.txt + python -VV > transfer-receipts/python.txt + uname -a > transfer-receipts/platform.txt + lscpu > transfer-receipts/cpu.txt + cp transfer-public-contracts.xml transfer-research-contracts.xml \ + freeze.log run.log audit.log transfer-receipts/ 2>/dev/null || true + - uses: actions/upload-artifact@v4 + if: always() + with: + name: itc-exam-transfer-${{ matrix.runner }}-py${{ matrix.python }}-${{ github.run_id }} + path: | + itc-transfer-evidence/ + transfer-receipts/ + retention-days: 90 + if-no-files-found: warn diff --git a/.github/workflows/public-package.yml b/.github/workflows/public-package.yml index 4efdf81..9b60760 100644 --- a/.github/workflows/public-package.yml +++ b/.github/workflows/public-package.yml @@ -1,7 +1,7 @@ name: public-package on: pull_request: - branches: [main, "maintenance/**", "research/deductive-search-*", "research/focused-search-*", "research/research-engineering-*", "research/faster-queries-review-*"] + branches: [main, "maintenance/**", "research/deductive-search-*", "research/focused-search-*", "research/research-engineering-*", "research/faster-queries-review-*", "research/exact-public-api-*"] workflow_dispatch: permissions: contents: read @@ -48,6 +48,7 @@ jobs: .public-package/install/venv/bin/python -I scripts/check_focused_installation.py | tee .public-package/focused-install.txt .public-package/install/venv/bin/python -I scripts/check_dpll_installation.py | tee .public-package/dpll-install.txt .public-package/install/venv/bin/python -I scripts/check_exact_installation.py --out .public-package/exact-install.json | tee .public-package/exact-install.txt + .public-package/install/venv/bin/python -I scripts/check_exam_repair_installation.py --out .public-package/exam-repair-install.json | tee .public-package/exam-repair-install.txt - name: Run and replay frozen compact-state comparison run: | set -o pipefail diff --git a/docs/EXAM_REPAIR.md b/docs/EXAM_REPAIR.md new file mode 100644 index 0000000..812b150 --- /dev/null +++ b/docs/EXAM_REPAIR.md @@ -0,0 +1,70 @@ +# Proof-carrying bounded exam repair + +`spectra.exam_repair` maps a narrow operational rescheduling problem to the +versioned `spectra.exact` API: + +- each exam has one or two pre-approved candidate periods; +- exams sharing a student may not use the same period; +- explicit exam exclusions are also supported; +- current period closures, fixed moves, and allowed-period restrictions are + intersected into an exact query; +- SAT returns a complete named assignment; +- UNSAT returns an independently verifiable proof that can be translated into + named exams, periods, and a shared-student/exclusion chain. + +```python +from spectra.exam_repair import ExamRepairModel +from spectra.exact import ExactRuntime, build_exact_runtime + +model = ExamRepairModel.create( + period_ids=("Monday AM", "Monday PM"), + exam_ids=("MATH101", "CHEM101", "HIST101"), + students=((11, 20), (20, 31), (31,)), + candidate_periods=(("Monday AM", "Monday PM"),) * 3, +) +query = model.freeze_event( + closed_periods=(), + fixed=(("MATH101", "Monday AM"), ("CHEM101", "Monday AM")), +) + +runtime = ExactRuntime(build_exact_runtime("exact-native")) +with runtime.prepare(model.problem, mode="scc") as session: + answer = session.solve(query) + +if answer.status == "SAT_VERIFIED": + print(model.assignment_from_labels(answer.labels, query)) +else: + print(model.explain_unsat(query, answer.proof)) +``` + +## Scope boundary + +This is **bounded repair**, not full timetabling. The adapter does not generate +candidate periods or model room capacity, room assignment, precedence, +coincidence, or soft objectives. Those constraints must be incorporated before +admission or checked separately. + +`spectra.itc2007_exam` provides a strict reader for the ITC-2007 examination +format. Its `conflict_core` conversion preserves an immutable receipt of every +constraint class outside the bounded model and refuses conversion unless the +caller explicitly acknowledges those omissions. + +The research transfer protocol is documented in +[`ITC_EXAM_TRANSFER_PROTOCOL.md`](../experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md). + +## Prospective multi-instance evaluation + +The selector-v2 policy and its `set10`/`set12` execution holdouts are fixed in +[`ITC_EXAM_SUITE_PROTOCOL.md`](../experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md). +The completed cross-platform measurements, retained negative repetitions and +artifact digests are published in the +[`2026-10-16 suite results`](../experiments/compiled_query/ITC_EXAM_SUITE_RESULTS_20261016.md). +The suite rotates measured engine order, preserves every failed cell, and gates +only the predeclared auto/raw overhead on holdout cases. Passing that suite is +application-transfer evidence, not an operator deployment or full ITC-2007 +optimization result. + +An outside runner can reproduce the source, installed-wheel, freeze, execution and +offline-audit boundaries using the +[independent replication guide](../experiments/compiled_query/ITC_EXAM_REPLICATION.md). +Negative or conflicting replications are explicitly valid results. diff --git a/docs/README.md b/docs/README.md index f11fd18..96d2374 100644 --- a/docs/README.md +++ b/docs/README.md @@ -24,6 +24,7 @@ historical neural, MCTS, low-bit, general-SAT, or universal CPU-performance clai | Install and run the public tools | [Quick start](../README.md#base-toolkit-quick-start) | | Understand API, input formats and return values | [API and CLI](API.md) | | Build and use checked SAT/UNSAT exact queries | [Proof-carrying exact API](EXACT_API.md) | +| Apply the exact core to bounded exam rescheduling | [Proof-carrying exam repair](EXAM_REPAIR.md) | | Check released, merged, experimental and failed work | [Current status](STATUS.md) | | Run tests, build a wheel or reproduce experiments | [Development](DEVELOPMENT.md) | | Prepare a package release | [Release checklist](RELEASING.md) | diff --git a/experiments/compiled_query/ITC_EXAM_REPLICATION.md b/experiments/compiled_query/ITC_EXAM_REPLICATION.md new file mode 100644 index 0000000..3890d53 --- /dev/null +++ b/experiments/compiled_query/ITC_EXAM_REPLICATION.md @@ -0,0 +1,116 @@ +# Independent replication: proof-carrying ITC exam repair + +This guide is for an outside runner who has not changed the selector, event bank, +acceptance threshold, or result interpretation. A successful run reproduces a +bounded exam-repair transfer. It does **not** establish full ITC-2007 timetabling, +operator adoption, universal performance, or algorithmic priority. + +## 1. Pin both repositories + +Record the exact SPECTRA commit under review and use the fixed upstream revision: + +```bash +git clone https://github.com/tugrapaydiner/SPECTRA.git +cd SPECTRA +git checkout + +git clone https://github.com/davidvanbulck/ITC-2007-CETT.git upstream/ITC-2007-CETT +git -C upstream/ITC-2007-CETT checkout ed2d4c0cf5302b77a8b321cd0380de0bb579d538 +``` + +Do not substitute newer upstream bytes. Preserve the upstream `LICENSE` in every +shared evidence package. + +## 2. Record the environment before execution + +```bash +mkdir -p replication-receipts +git rev-parse HEAD > replication-receipts/spectra-commit.txt +git rev-parse HEAD^{tree} > replication-receipts/spectra-tree.txt +git -C upstream/ITC-2007-CETT rev-parse HEAD > replication-receipts/upstream-commit.txt +python -VV > replication-receipts/python.txt +uname -a > replication-receipts/platform.txt +lscpu > replication-receipts/cpu.txt 2>/dev/null || true +c++ --version > replication-receipts/compiler.txt 2>&1 +``` + +Use a GIL-enabled CPython 3.11 or 3.13 and a C++17 compiler. Do not install or load +an alternative solver for the measured calls. + +## 3. Check source and installed-package contracts + +```bash +python -m pip install 'build==1.3.0' 'pytest==8.4.2' +python -m pytest \ + tests/public/test_exam_repair.py \ + tests/public/test_itc2007_exam.py \ + --confcutdir=tests/public -q +python -m pytest \ + experiments/compiled_query/test_exact.py \ + experiments/compiled_query/test_itc_exam_transfer.py \ + experiments/compiled_query/test_itc_exam_suite.py \ + -q -k 'auto or tiled_witnesses or itc or suite' + +python -m build --wheel --outdir replication-wheel +python -m venv replication-install +replication-install/bin/python -m pip install --no-deps replication-wheel/*.whl +replication-install/bin/python -I scripts/check_exam_repair_installation.py \ + --out replication-receipts/installed-exam-repair.json +``` + +On Windows, use `replication-install/Scripts/python.exe` and a configured MSVC x64 +developer environment. + +## 4. Freeze before running any case + +The freeze must complete before inspecting any holdout answer or timing: + +```bash +python -m experiments.compiled_query.itc_exam_suite freeze \ + --root itc-suite-evidence \ + --upstream-root upstream/ITC-2007-CETT \ + --queries 1024 \ + --holdout-max-auto-raw-ratio 1.15 +``` + +Confirm that `suite-manifest.json` records, in order: + +1. `set9-development` with role `development`; +2. `set10-holdout` with role `holdout`; +3. `set12-holdout` with role `holdout`. + +Do not change the roles, query count, five-repetition schedule, selector-v2 rule or +1.15 paired-median guardrail after this point. + +## 5. Execute once and audit without native code + +```bash +python -m experiments.compiled_query.itc_exam_suite run \ + --root itc-suite-evidence +python -S -m experiments.compiled_query.itc_exam_suite audit \ + --root itc-suite-evidence +``` + +The audit must independently regenerate every derived input, replay every `SCQ2` +answer from the original `SBC1` packets, require cross-engine decision agreement, +and publish all holdout failures. Do not delete negative cells or repeat a failed +measurement under a changed rule. + +## 6. Report every result + +Publish the complete `itc-suite-evidence` directory plus the receipts above. At a +minimum, report: + +- SPECTRA commit and tree; +- upstream commit; +- OS, CPU, Python and compiler; +- all source/public/installed contract outcomes; +- each case's role, exam count, conflict count, query count, SAT/UNSAT counts, + selected automatic engine and policy reason; +- all five paired `auto_elapsed / raw_elapsed` ratios per holdout; +- paired-median ratio and pass/fail against 1.15; +- every execution or audit failure, including resource failures. + +A useful independent report explicitly says whether the bytes and conclusions +match the project-owned CI artifact. A disagreement is a valid replication result +and should not be hidden or relabelled as an environment problem without evidence. diff --git a/experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md b/experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md new file mode 100644 index 0000000..b36df50 --- /dev/null +++ b/experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md @@ -0,0 +1,91 @@ +# Prospective ITC-2007 exam-repair suite protocol + +**Status:** frozen before executing the `set10` and `set12` result panels. The +selector may be falsified by these holdouts, but it must not be retuned inside the +same suite. + +## Purpose + +The first application transfer used `set9` and exposed an important limitation: +the original automatic policy selected the SCC engine even though the explicit raw +engine was faster on that dense repair bank. The structural-v2 policy adds one +answer-independent rule: + +> For a bank of at least 64 requests, use raw traversal when the immutable request +> packet contains at least eight pins per request on average. + +The threshold was chosen from the already exposed synthetic development panel and +the `set9` development transfer. It depends only on packet geometry, not SAT/UNSAT +answers, proof sizes, or measured times. Short banks, base-infeasible graphs and +the prior SCC/component rules retain their previous ordering. + +## Fixed external source + +Every workflow checks out `davidvanbulck/ITC-2007-CETT` at commit +`ed2d4c0cf5302b77a8b321cd0380de0bb579d538` and retains its `LICENSE` in each +case directory. No upstream data is committed to SPECTRA. + +The fixed cases are: + +| Case | Role | Instance | Published feasible schedule | +|---|---|---|---| +| `set9-development` | Development | `examtt-instances/Instances/set9.exam` | `InitMethods/SolStore/set9_OBSIFeas_0.sol` | +| `set10-holdout` | Prospective holdout | `examtt-instances/Instances/set10.exam` | `InitMethods/SolStore/set10_OBSIFeas_0.sol` | +| `set12-holdout` | Prospective holdout | `examtt-instances/Instances/set12.exam` | `InitMethods/SolStore/set12_OBSIFeas_0.sol` | + +The bytes are public, so “holdout” means **execution holdout**, not secret data: +no selector-v2 answer or timing from `set10` or `set12` may influence the committed +policy or acceptance threshold. + +## Per-case construction + +Each case uses the exact construction in +[`ITC_EXAM_TRANSFER_PROTOCOL.md`](ITC_EXAM_TRANSFER_PROTOCOL.md): validate the +published schedule against all original hard constraints, freeze exams involved in +unsupported hard constraints, assign one deterministic duration-compatible +alternative to eligible exams, build the shared-student/`EXCLUSION` conflict core, +and generate 1,024 unique deterministic repair events. + +Every event is answered by `auto`, `raw`, `scc`, and `route`. Completed answers +must include a full assignment or portable contradiction proof and must replay from +the original `SBC1` packet without native code. + +## Timing schedule and prospective gate + +Each engine receives one untimed warmup. In each of five measured repetitions the +engine order rotates, preventing one mode from always running first or last: + +1. `auto, raw, scc, route` +2. `raw, scc, route, auto` +3. `scc, route, auto, raw` +4. `route, auto, raw, scc` +5. repeat from the first order + +For every holdout, pair `auto` and `raw` by repetition and compute the median of the +five `auto_elapsed / raw_elapsed` ratios. The predeclared guardrail is: + +```text +paired-median auto/raw ratio <= 1.15 +``` + +This is a bounded overhead guardrail, not a speedup claim. Development-case timing +is reported but cannot pass or fail the prospective gate. Failed holdouts remain +in the artifact and may not be removed, renamed, rerun under a changed threshold, +or converted to development cases. + +## Evidence and audit + +The suite manifest binds: + +- source commit and per-case source inventory; +- upstream repository and commit; +- exact instance and solution paths and SHA-256 identities; +- development/holdout role; +- selector policy and threshold; +- per-case manifest hashes. + +The suite audit reruns every child audit, checks every result and proof, checks the +rotated timing schedule, computes paired ratios from recorded repetitions, and +publishes all failures. A successful result is still project-owned execution, not +outside-team replication, operator adoption, full ITC-2007 feasibility, or +algorithmic-priority evidence. diff --git a/experiments/compiled_query/ITC_EXAM_SUITE_RESULTS_20261016.md b/experiments/compiled_query/ITC_EXAM_SUITE_RESULTS_20261016.md new file mode 100644 index 0000000..592fa15 --- /dev/null +++ b/experiments/compiled_query/ITC_EXAM_SUITE_RESULTS_20261016.md @@ -0,0 +1,164 @@ +# Prospective ITC exam-repair suite — 2026-10-16 + +## Result + +The prospectively fixed bounded exam-repair suite completed on all three declared +environments. Both execution holdouts passed the unchanged paired-median +automatic/raw guardrail of **1.15**. Every admitted result was independently +replayed from the original pinned ITC bytes, and no failed cell or output was +removed. + +This is application-transfer evidence for the binary-domain exam-conflict core. It +is **not** a full ITC-2007 timetabling result, an operator deployment, outside-team +replication, universal performance evidence, or an algorithmic-priority claim. + +## Frozen boundary + +| Item | Value | +|---|---| +| Measured SPECTRA commit | `ff77d802e9a2bb3c1d97c5acf70d8871dc114f7c` | +| Published implementation commit | `3036a3c97cf5706d60ab9e277708081b4f241954` | +| Upstream ITC repository commit | `ed2d4c0cf5302b77a8b321cd0380de0bb579d538` | +| Selector policy | `structural-v2` | +| Requests per case | 1,024 | +| Warmup | one untimed call per mode | +| Measured repetitions | five | +| Mode order | rotated each repetition | +| Holdout gate | paired median of `auto_elapsed / raw_elapsed <= 1.15` | +| Development case | `set9` | +| Execution holdouts | `set10`, `set12` | + +The implementation, policy, case roles, event generator, repetition count and gate +were committed before any holdout execution. The automatic engine used packet +structure only. All three cases triggered `high_pin_density` and selected `raw`. + +## Functional outcomes + +The decisions and counts were identical on x86 Python 3.11, x86 Python 3.13 and +native ARM64 Python 3.13. + +| Case | Role | Exams | Periods | Enrolments | Conflicts | Explicit exclusions | SAT | UNSAT | Pins | +|---|---|---:|---:|---:|---:|---:|---:|---:|---:| +| `set9` | development | 169 | 25 | 2,532 | 1,114 | 1 | 268 | 756 | 9,698 | +| `set10` | holdout | 214 | 32 | 7,853 | 1,133 | 0 | 327 | 697 | 9,311 | +| `set12` | holdout | 78 | 12 | 3,685 | 560 | 6 | 24 | 1,000 | 10,361 | + +For `set10`, 178 UNSAT answers used an empty-domain proof and 519 used a +forced-opposites path proof. For `set12`, those counts were 269 and 731. The native +engines agreed on every SAT/UNSAT decision, and the standard-library audit checked +every complete assignment or contradiction proof against the original fixed graph +and current restrictions. + +## Prospective guardrail + +Values below are the median of the five paired repetition ratios, not a ratio of +independently aggregated medians. + +| Environment | `set9` development | `set10` holdout | `set12` holdout | Holdout gate | +|---|---:|---:|---:|---| +| Linux x86, Python 3.11 | 0.995442 | **0.999355** | **1.003860** | PASS | +| Linux x86, Python 3.13 | 1.073799 | **1.019084** | **1.026623** | PASS | +| Linux ARM64, Python 3.13 | 1.017422 | **0.999036** | **1.000705** | PASS | + +The largest holdout paired-median ratio was **1.026623**, leaving approximately +10.7 percentage points of margin to the fixed 1.15 limit. + +Individual repetitions were intentionally retained. In particular, the first +`set12` repetition on x86 Python 3.13 had ratio **1.168387**, and the first +`set10` repetition on x86 Python 3.11 had ratio **1.158769**. Both exceed the gate +when viewed alone; the predeclared gate is the paired median over five rotating +repetitions, so these are negative retained observations rather than deleted or +retried cells. + +### Paired ratios, all repetitions + +| Environment | Case | Five `auto/raw` ratios | +|---|---|---| +| x86 / Python 3.11 | `set10` | 1.158769, 0.999355, 1.000486, 0.984425, 0.995438 | +| x86 / Python 3.11 | `set12` | 1.123582, 1.004558, 1.000192, 1.003860, 0.997922 | +| x86 / Python 3.13 | `set10` | 1.098272, 1.066995, 1.018905, 0.998810, 1.019084 | +| x86 / Python 3.13 | `set12` | 1.168387, 1.012663, 1.026623, 0.978225, 1.040015 | +| ARM64 / Python 3.13 | `set10` | 1.112409, 0.999036, 0.987604, 1.004978, 0.985442 | +| ARM64 / Python 3.13 | `set12` | 1.099958, 0.985422, 0.994436, 1.000705, 1.030142 | + +The automatic and explicit raw modes execute the same native engine after policy +selection. Ratios close to one therefore measure selection/dispatch noise and host +variation rather than an algorithmic speedup. The purpose of this gate is to stop +the automatic policy from imposing material overhead on unseen application cases. + +## Complete-call medians + +Elapsed time includes native construction, all 1,024 decisions, complete witnesses +or portable proofs, independent native checking, `SCQ2` construction, disposal and +hashing. Candidate generation, packet creation, compilation and process startup are +outside the measured call. + +| Environment | Case | Auto | Raw | SCC | Route | +|---|---|---:|---:|---:|---:| +| x86 / Python 3.11 | `set9` | 1.286 ms | 1.292 ms | 1.288 ms | 1.657 ms | +| x86 / Python 3.11 | `set10` | 1.163 ms | 1.161 ms | 1.144 ms | 1.358 ms | +| x86 / Python 3.11 | `set12` | 0.888 ms | 0.887 ms | 0.987 ms | 1.199 ms | +| x86 / Python 3.13 | `set9` | 0.823 ms | 0.765 ms | 0.788 ms | 0.952 ms | +| x86 / Python 3.13 | `set10` | 0.697 ms | 0.666 ms | 0.693 ms | 0.795 ms | +| x86 / Python 3.13 | `set12` | 0.536 ms | 0.523 ms | 0.605 ms | 0.725 ms | +| ARM64 / Python 3.13 | `set9` | 1.114 ms | 1.095 ms | 1.052 ms | 1.402 ms | +| ARM64 / Python 3.13 | `set10` | 1.004 ms | 1.004 ms | 0.972 ms | 1.172 ms | +| ARM64 / Python 3.13 | `set12` | 0.772 ms | 0.771 ms | 0.824 ms | 1.050 ms | + +SCC remains slightly faster than raw on some cells. Selector-v2 deliberately +prioritises a conservative no-material-overhead rule for heavily pinned application +banks rather than claiming a per-cell optimum. The development result does not +justify retuning after seeing the holdouts. + +## CI and artifacts + +### Development transfer + +Workflow run: `38951373279` + +- Linux x86 / Python 3.11: PASS +- Linux x86 / Python 3.13: PASS +- Native Linux ARM64 / Python 3.13: PASS + +Artifacts: + +| Environment | Artifact ID | Artifact SHA-256 | +|---|---:|---| +| x86 / Python 3.11 | `12068467826` | `3afc63b70f8499c03fe97df78eff288c8316accaf714bace3585be938cab1fe4` | +| x86 / Python 3.13 | `12068077883` | `32823ece7589b6f76901469c141210ca3796d489f8a90eaa29aaac0e933d69d1` | +| ARM64 / Python 3.13 | `12068222627` | `d5de0a96b0a8347df58296e6bad01e4cd24e49cb908e952c47056609f2acf762` | + +### Prospective suite + +Workflow run: `38951398495` + +- Linux x86 / Python 3.11: PASS +- Linux x86 / Python 3.13: PASS +- Native Linux ARM64 / Python 3.13: PASS +- Source contracts: PASS on all cells +- Installed-wheel exam-repair execution: PASS on all cells +- Freeze-before-execution: PASS on all cells +- Independent source-only audit: PASS on all cells + +Artifacts: + +| Environment | Artifact ID | Artifact SHA-256 | +|---|---:|---| +| x86 / Python 3.11 | `12068498169` | `fb100a67983b02c7969809efb680deaf5b4002c6f2242122d8cca8ff4a415c23` | +| x86 / Python 3.13 | `12068552843` | `8f86935fa6e6811c56fc4156d8dc9ea422c4a14b5ef0cba356b496d3ef4208e7` | +| ARM64 / Python 3.13 | `12068023095` | `35247cef687fc26ccbfec69d6903ed421a4a3fc9df8682b7143afa0600b055f4` | + +## Preserved failed attempts + +The first transfer run (`38951148893`) and first suite run (`38951172493`) failed +during test collection because the dependency-light public-test command loaded the +repository-wide ML `tests/conftest.py` without NumPy. They stopped before evidence +freezing or any holdout execution. The correction isolated public tests with +`--confcutdir=tests/public`; it did not change the selector, cases, event bank, +repetitions, timing order or guardrail. The failed runs remain visible. + +## Replication + +Follow [`ITC_EXAM_REPLICATION.md`](ITC_EXAM_REPLICATION.md) from a clean checkout. +An independent disagreement or negative result is valid evidence and should be +published with the complete artifacts rather than normalised away. diff --git a/experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md b/experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md new file mode 100644 index 0000000..59c79df --- /dev/null +++ b/experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md @@ -0,0 +1,127 @@ +# ITC-2007 bounded exam-repair transfer protocol + +**Status:** fixed before opening the external instance and schedule in CI. This is +an application-format transfer of the versioned proof-carrying exact-query API, +not a complete capacitated examination-timetabling result. + +## External source and attribution + +The workflow checks out `davidvanbulck/ITC-2007-CETT` at commit +`ed2d4c0cf5302b77a8b321cd0380de0bb579d538`. The selected files are: + +- `examtt-instances/Instances/set9.exam` +- `InitMethods/SolStore/set9_OBSIFeas_0.sol` +- `LICENSE` + +The upstream repository states that its solver and instances originate from the +ITC-2007 examination-timetabling setting and requests citation of Van Bulck, +Goossens and Schaerf. Every evidence package retains the upstream license and +this acknowledgment: + +> This product includes software/data distributed by David Van Bulck, Dries +> Goossens, and Andrea Schaerf, Ghent University, Belgium +> (https://github.com/davidvanbulck/ITC-2007-CETT.git). + +No upstream source or data is committed to SPECTRA. + +## Admitted question + +Start from the published feasible timetable. Each examination is assigned one +or two **pre-approved candidate periods**: + +1. The published period is always retained. +2. Exams appearing in `AFTER`, `EXAM_COINCIDENCE`, or `ROOM_EXCLUSIVE` hard + constraints are frozen to the published period. +3. Every other exam receives one deterministic alternative when available. The + alternative must have enough duration and the instance must contain a room + large enough for the exam in isolation. A SHA-256 ordering of + `(input hash, exam, period)` chooses among eligible alternatives. +4. Shared-student conflicts and explicit `EXCLUSION` constraints become graph + edges. The palette contains the instance's declared periods. + +The exact question is therefore: + +> Given current period closures and requested moves within these fixed +> one/two-period domains, does a conflict-free period assignment exist? + +A completed call must return either a full original-exam assignment or a portable +original-literal contradiction proof. The standard-library verifier replays all +answers from the frozen `SBC1` packet and `SCQ2` output. + +## Deliberately unmodelled constraints + +The reduction does **not** solve or score: + +- room reassignment or simultaneous room-capacity packing; +- soft institutional penalties; +- changes to `AFTER`, `EXAM_COINCIDENCE`, or `ROOM_EXCLUSIVE` exams; +- candidate-period generation outside the frozen deterministic rule; +- the full ITC-2007 optimization problem. + +The parser retains counts for every omitted constraint class. Conversion requires +an explicit `acknowledge_ignored_constraints=True`, and the omission receipt is +stored in every manifest and audit. A conflict-core SAT answer is not a complete +ITC timetable certificate. + +## Frozen event bank + +The bank contains 1,024 unique events in this order: + +1. the unchanged published baseline; +2. every single-period closure; +3. every single flexible-exam move to its alternative; +4. deterministic multi-exam move sets of width 2 through 12; +5. deterministic period-closure plus multi-move events. + +The seed is the first 64 bits of SHA-256 over the exact instance bytes, a NUL byte, +and the exact solution bytes. Widths, exam rankings and closed periods are then +derived directly from labelled SHA-256 words rather than Python's version-sensitive +sampling helpers. Duplicate exact queries are removed before the bank is +truncated. Failure to create 1,024 distinct events is a protocol failure, not +permission to alter the policy after observing results. + +## Engines and measured boundary + +The same immutable packet is run through `auto`, `raw`, `scc`, and `route`. Each +mode receives one untimed warmup; five measured repetitions rotate the mode order +so no mode always executes first or last. The measured boundary starts with ready +`SBC1` bytes and includes: + +- input validation and native construction; +- every query decision; +- complete SAT witnesses or portable UNSAT proofs; +- the separately owned native observer; +- `SCQ2` materialization; +- native disposal and the Python call boundary. + +External checkout, parsing, candidate generation, packet packing, native +compilation, evidence writes, and offline replay are outside the timing boundary. +Timing is descriptive for this single development transfer; there is no speed-win +gate here. The separate prospective multi-instance suite declares its holdout +threshold before execution. + +## Freeze, execution and audit + +`freeze` validates everything before atomically publishing an evidence directory. +It writes external bytes, the upstream license, candidate rows, canonical queries, +packet, source inventory, commit/tree identities and hashes with exclusive +creation. Every listed source blob must match the named commit. + +`run` explicitly builds the bundled ABI-3 runtime, records its receipt hash, runs +all engines/repetitions, requires byte-stable repeated output per engine, and +verifies every output before publication. + +`audit` is rerunnable without a native solver. It reparses the original instance +and solution, rechecks all baseline hard constraints, regenerates the seed, +candidate rows and complete event bank, reconstructs the packet, checks recorded +metadata against the certified bytes, replays every output, requires all modes to +agree on SAT/UNSAT decisions, counts proof kinds, and refuses changed evidence or +a changed prior audit. Stored candidate/query JSON is evidence, not an oracle. + +## Interpretation + +A successful run demonstrates that the exact API transfers from exposed synthetic +graph panels to a published timetabling-format repair core while retaining full +proof boundaries. It remains project-owned execution on a deterministic derived +problem. It is not operator adoption, outside-team replication, a claim of +algorithmic priority, or evidence that SPECTRA solves the full ITC-2007 task. diff --git a/experiments/compiled_query/exact.py b/experiments/compiled_query/exact.py index 780a7ff..7eee4c2 100644 --- a/experiments/compiled_query/exact.py +++ b/experiments/compiled_query/exact.py @@ -363,11 +363,13 @@ def solve_session_packet(self, packet: bytes, *, mode: str = 'route', max_bytes: int = DEFAULT_BYTES) -> ExactSessionPacketAnswer: """Construct, solve, verify, serialize and dispose one prepared SBC1 session. - Opt-in ``auto`` uses raw traversal below 64 requests or on a base-infeasible - graph. Otherwise it uses routed proofs when SCCs at least halve the - literal graph, and plain SCC batching when they do not. Selection uses - fixed-graph structure and bank length, never measured answers or timings. - ``info['selected_mode']`` names the actual engine. Explicit modes and the + Opt-in ``auto`` uses structural policy v2. It selects raw traversal below + 64 requests, on a base-infeasible graph, or when the immutable bank carries + at least eight pins per request on average. Otherwise it uses routed proofs + when SCCs at least halve the literal graph, and plain SCC batching when they + do not. Selection uses only admitted graph/request geometry, never answers + or measured timings. ``info['selected_mode']`` and + ``info['auto_policy_reason']`` expose the decision. Explicit modes and the default retain their meaning; this policy is an experimental heuristic. """ if type(packet) is not bytes: diff --git a/experiments/compiled_query/exact_native.cpp b/experiments/compiled_query/exact_native.cpp index 96182ee..96694d3 100644 --- a/experiments/compiled_query/exact_native.cpp +++ b/experiments/compiled_query/exact_native.cpp @@ -341,12 +341,13 @@ struct ObserverSessionPacket { struct Answer {bool sat=true;std::vector labels,certificate;W visits=0,arcs=0;}; struct Index { U n,k,nc=0,bad=NIL;bool condensed,sparse,routed;W cap;W full_arcs=0; + const char* auto_reason="explicit_mode"; std::vector masks; std::vector lo,hi,base; std::vector comp,opposite; std::vector inward,outward,representative,cross_from,cross_to; CSR original,dag; - Index(Input p,U mode,U bank_size=0):n(p.n),k(p.k),condensed(mode!=0),sparse(mode==2),routed(mode==3),cap(p.cap),masks(std::move(p.masks)),lo(n),hi(n,255),base(n) { + Index(Input p,U mode,U bank_size=0,U bank_pins=0):n(p.n),k(p.k),condensed(mode!=0),sparse(mode==2),routed(mode==3),cap(p.cap),masks(std::move(p.masks)),lo(n),hi(n,255),base(n) { std::vector> arcs;arcs.reserve(4*p.edges.size()+n); for(U v=0;v(comp[2*v]=64 && bad==NIL; - routed=condensed && nc<=n; + // Structural auto policy v2. set9 development evidence showed that + // large, heavily pinned repair banks can lose to raw traversal even + // when tile64 is available. The policy therefore uses only immutable + // request geometry (never answers or measured timings): raw below one + // tile, on a base contradiction, or at eight pins per row and above. + // The threshold is frozen before the set10/set12 holdout transfer. + if(bank_size<64) { + condensed=false;routed=false;auto_reason="bank_below_tile64"; + } else if(bad!=NIL) { + condensed=false;routed=false;auto_reason="base_infeasible"; + } else if(W(bank_pins)>=8*W(bank_size)) { + condensed=false;routed=false;auto_reason="high_pin_density"; + } else { + condensed=true;routed=nc<=n; + auto_reason=routed?"route_component_compression":"scc_tile64"; + } } if(condensed && bad==NIL) { opposite.assign(nc,NIL); @@ -990,6 +1002,7 @@ PyObject* solve_session_packet(PyObject*,PyObject* args) { const auto* data=reinterpret_cast(PyBytes_AS_STRING(packet)); size_t size=static_cast(PyBytes_GET_SIZE(packet)); std::unique_ptr solver;std::unique_ptr observer;BankResult result; + U bank_queries=0,bank_pins=0; { Released guard; ObserverSessionPacket observer_rows(data,size,limit); @@ -997,8 +1010,9 @@ PyObject* solve_session_packet(PyObject*,PyObject* args) { W observer_bytes=observer->bytes(); if(observer_bytes>=limit) throw Resource("SBC1 observer consumes session cap"); SolverSessionPacket solver_rows(data,size,limit-observer_bytes); + bank_queries=solver_rows.query_count();bank_pins=solver_rows.pin_count(); solver=std::make_unique(solver_rows.take_input(limit-observer_bytes), - static_cast(which),solver_rows.query_count()); + static_cast(which),bank_queries,bank_pins); result=run_rows(*solver,*observer,solver_rows,observer_rows,size,limit,"SBC1"); } PyObject* output=PyBytes_FromStringAndSize(reinterpret_cast(result.output.data()), @@ -1018,11 +1032,22 @@ PyObject* solve_session_packet(PyObject*,PyObject* args) { if(!metadata){Py_DECREF(output);return nullptr;} PyObject* kernel=PyUnicode_FromString(result.tiled?"tile64":"serial"); PyObject* tiles=PyLong_FromUnsignedLong(result.tiles); - if(!kernel || !tiles || PyDict_SetItemString(metadata,"bank_kernel",kernel)<0 - || PyDict_SetItemString(metadata,"bank_tiles",tiles)<0) { - Py_XDECREF(kernel);Py_XDECREF(tiles);Py_DECREF(output);Py_DECREF(metadata);return nullptr; + PyObject* queries=PyLong_FromUnsignedLong(bank_queries); + PyObject* pins=PyLong_FromUnsignedLong(bank_pins); + PyObject* policy=PyUnicode_FromString(which==4?"structural-v2":"explicit"); + PyObject* reason=PyUnicode_FromString(solver->auto_reason); + if(!kernel || !tiles || !queries || !pins || !policy || !reason + || PyDict_SetItemString(metadata,"bank_kernel",kernel)<0 + || PyDict_SetItemString(metadata,"bank_tiles",tiles)<0 + || PyDict_SetItemString(metadata,"bank_query_count",queries)<0 + || PyDict_SetItemString(metadata,"bank_pin_count",pins)<0 + || PyDict_SetItemString(metadata,"auto_policy",policy)<0 + || PyDict_SetItemString(metadata,"auto_policy_reason",reason)<0) { + Py_XDECREF(kernel);Py_XDECREF(tiles);Py_XDECREF(queries);Py_XDECREF(pins); + Py_XDECREF(policy);Py_XDECREF(reason);Py_DECREF(output);Py_DECREF(metadata);return nullptr; } - Py_DECREF(kernel);Py_DECREF(tiles); + Py_DECREF(kernel);Py_DECREF(tiles);Py_DECREF(queries);Py_DECREF(pins); + Py_DECREF(policy);Py_DECREF(reason); return Py_BuildValue("NKKKKKKN",output, static_cast(result.sat+result.unsat), static_cast(result.sat), diff --git a/experiments/compiled_query/itc_exam_suite.py b/experiments/compiled_query/itc_exam_suite.py new file mode 100644 index 0000000..dfc8b71 --- /dev/null +++ b/experiments/compiled_query/itc_exam_suite.py @@ -0,0 +1,352 @@ +"""Prospective multi-instance ITC-2007 exam-repair transfer suite. + +The selector-v2 rule is developed from the exposed synthetic panel and the +published ``set9`` transfer only. ``set10`` and ``set12`` are fixed holdout +instances: their execution results must not be used to retune the policy. This +suite remains a bounded conflict-core repair study, not a full timetabling claim. +""" +from __future__ import annotations + +import argparse +from dataclasses import dataclass +import json +from pathlib import Path, PurePosixPath +import shutil +import statistics +from typing import Iterable + +from experiments.compiled_query import itc_exam_transfer as transfer + +SCHEMA = "spectra.itc2007.exam_repair_suite.v1" +DEFAULT_HOLDOUT_MAX_RATIO = 1.15 + + +@dataclass(frozen=True) +class SuiteCase: + name: str + role: str + instance_path: str + solution_path: str + + def validate(self) -> "SuiteCase": + if (type(self.name) is not str or not self.name + or any(ch not in "abcdefghijklmnopqrstuvwxyz0123456789-" for ch in self.name) + or self.name.startswith("-") or self.name.endswith("-")): + raise ValueError("suite case name must be lowercase kebab-case") + if self.role not in ("development", "holdout", "replication"): + raise ValueError("suite case role differs") + for label, value in (("instance", self.instance_path), ("solution", self.solution_path)): + if type(value) is not str or not value: + raise ValueError(f"suite case {label} path must be nonempty") + path = PurePosixPath(value) + if path.is_absolute() or ".." in path.parts: + raise ValueError(f"suite case {label} path must stay under upstream root") + return self + + +DEFAULT_CASES = ( + SuiteCase( + "set9-development", "development", + "examtt-instances/Instances/set9.exam", + "InitMethods/SolStore/set9_OBSIFeas_0.sol", + ), + SuiteCase( + "set10-holdout", "holdout", + "examtt-instances/Instances/set10.exam", + "InitMethods/SolStore/set10_OBSIFeas_0.sol", + ), + SuiteCase( + "set12-holdout", "holdout", + "examtt-instances/Instances/set12.exam", + "InitMethods/SolStore/set12_OBSIFeas_0.sol", + ), +) + + +def _cases(cases: Iterable[SuiteCase]) -> tuple[SuiteCase, ...]: + checked = tuple(case.validate() for case in cases) + if not checked or len({case.name for case in checked}) != len(checked): + raise ValueError("suite requires unique nonempty cases") + if not any(case.role == "holdout" for case in checked): + raise ValueError("suite requires at least one holdout") + return checked + + +def _ratio(value: float | None) -> float | None: + if value is None: + return None + if type(value) not in (int, float) or not 1.0 <= float(value) <= 10.0: + raise ValueError("holdout max auto/raw ratio must be in [1, 10] or null") + return float(value) + + +def _manifest_path(root: Path) -> Path: + return root / "suite-manifest.json" + + +def freeze(root: Path, upstream_root: Path, *, cases: Iterable[SuiteCase] = DEFAULT_CASES, + query_count: int = 1024, + holdout_max_auto_raw_ratio: float | None = DEFAULT_HOLDOUT_MAX_RATIO, + source_commit: str | None = None) -> dict: + root = root.resolve() + upstream_root = upstream_root.resolve() + if root.exists(): + raise FileExistsError(root) + checked = _cases(cases) + threshold = _ratio(holdout_max_auto_raw_ratio) + license_path = upstream_root / "LICENSE" + if not license_path.is_file(): + raise FileNotFoundError(license_path) + staging = root.with_name(root.name + ".partial") + if staging.exists(): + raise FileExistsError(staging) + (staging / "cases").mkdir(parents=True, exist_ok=False) + try: + case_records = [] + for case in checked: + case_root = staging / "cases" / case.name + manifest = transfer.freeze( + case_root, + upstream_root / case.instance_path, + upstream_root / case.solution_path, + query_count=query_count, + license_path=license_path, + source_commit=source_commit, + dataset_instance_path=case.instance_path, + dataset_solution_path=case.solution_path, + evaluation_role=case.role, + ) + case_records.append({ + "name": case.name, + "role": case.role, + "instance_path": case.instance_path, + "solution_path": case.solution_path, + "manifest_sha256": (case_root / "manifest.sha256").read_text().strip(), + "instance_sha256": manifest["instance_sha256"], + "solution_sha256": manifest["solution_sha256"], + }) + manifest = { + "schema": SCHEMA, + "classification": ( + "prospective multi-instance bounded exam-repair transfer; set9 is " + "development and set10/set12 are fixed execution holdouts" + ), + "source_commit": case_records and json.loads( + (staging / "cases" / case_records[0]["name"] / "manifest.json").read_text() + )["source_commit"], + "dataset_repository": transfer.DATASET_REPOSITORY, + "dataset_commit": transfer.DATASET_COMMIT, + "query_count_per_case": query_count, + "selector_policy": "structural-v2", + "selector_development_sources": [ + "exposed synthetic graph panel", + "set9 development transfer", + ], + "holdout_policy": ( + "set10 and set12 results may falsify the frozen selector but may not " + "change it inside this suite" + ), + "holdout_max_auto_raw_ratio": threshold, + "gate_metric": "median of paired per-repetition auto/raw elapsed ratios", + "cases": case_records, + } + payload = transfer.canonical_json(manifest) + transfer.write_once(_manifest_path(staging), payload) + transfer.write_once( + staging / "suite-manifest.sha256", + (transfer.digest(payload) + "\n").encode(), + ) + staging.rename(root) + return manifest + except BaseException: + shutil.rmtree(staging, ignore_errors=True) + raise + + +def load_manifest(root: Path) -> dict: + root = root.resolve() + expected = (root / "suite-manifest.sha256").read_text().strip() + manifest = json.loads(transfer.read_bound(_manifest_path(root), expected)) + if (manifest.get("schema") != SCHEMA + or manifest.get("dataset_repository") != transfer.DATASET_REPOSITORY + or manifest.get("dataset_commit") != transfer.DATASET_COMMIT + or manifest.get("selector_policy") != "structural-v2" + or type(manifest.get("query_count_per_case")) is not int + or manifest["query_count_per_case"] < 1): + raise ValueError("suite manifest identity differs") + threshold = _ratio(manifest.get("holdout_max_auto_raw_ratio")) + records = manifest.get("cases") + if type(records) is not list: + raise ValueError("suite case inventory differs") + checked = _cases(SuiteCase( + item.get("name"), item.get("role"), + item.get("instance_path"), item.get("solution_path"), + ) for item in records if type(item) is dict) + if len(checked) != len(records): + raise ValueError("suite case inventory differs") + for case, item in zip(checked, records): + case_root = root / "cases" / case.name + if ((case_root / "manifest.sha256").read_text().strip() + != item.get("manifest_sha256")): + raise ValueError(f"suite case {case.name} manifest hash differs") + child = transfer.load_manifest(case_root) + if (child.get("dataset_instance_path") != case.instance_path + or child.get("dataset_solution_path") != case.solution_path + or child.get("evaluation_role") != case.role + or child.get("query_count") != manifest["query_count_per_case"] + or child.get("instance_sha256") != item.get("instance_sha256") + or child.get("solution_sha256") != item.get("solution_sha256")): + raise ValueError(f"suite case {case.name} identity differs") + manifest["holdout_max_auto_raw_ratio"] = threshold + return manifest + + +def run(root: Path) -> dict: + root = root.resolve() + manifest = load_manifest(root) + if (root / "suite-run.json").exists(): + raise FileExistsError("suite execution already exists") + records = [] + for item in manifest["cases"]: + case_root = root / "cases" / item["name"] + record = transfer.run(case_root) + records.append({ + "name": item["name"], + "run_sha256": (case_root / "run.sha256").read_text().strip(), + "execution_order": record["execution_order"], + }) + result = { + "schema": SCHEMA + ".run", + "suite_manifest_sha256": (root / "suite-manifest.sha256").read_text().strip(), + "cases": records, + } + payload = transfer.canonical_json(result) + transfer.write_once(root / "suite-run.json", payload) + transfer.write_once(root / "suite-run.sha256", (transfer.digest(payload) + "\n").encode()) + return result + + +def audit(root: Path) -> dict: + root = root.resolve() + manifest = load_manifest(root) + run_expected = (root / "suite-run.sha256").read_text().strip() + run_record = json.loads(transfer.read_bound(root / "suite-run.json", run_expected)) + if (run_record.get("schema") != SCHEMA + ".run" + or run_record.get("suite_manifest_sha256") + != (root / "suite-manifest.sha256").read_text().strip()): + raise ValueError("suite run identity differs") + run_cases = run_record.get("cases") + if type(run_cases) is not list or len(run_cases) != len(manifest["cases"]): + raise ValueError("suite run case inventory differs") + + threshold = manifest["holdout_max_auto_raw_ratio"] + summaries = [] + holdout_failures = [] + for item, run_item in zip(manifest["cases"], run_cases): + if type(run_item) is not dict or run_item.get("name") != item["name"]: + raise ValueError("suite run case order differs") + case_root = root / "cases" / item["name"] + if (case_root / "run.sha256").read_text().strip() != run_item.get("run_sha256"): + raise ValueError(f"suite case {item['name']} run hash differs") + result = transfer.audit(case_root) + child_run = json.loads(transfer.read_bound( + case_root / "run.json", (case_root / "run.sha256").read_text().strip() + )) + auto_elapsed = child_run["modes"]["auto"]["elapsed_ns"] + raw_elapsed = child_run["modes"]["raw"]["elapsed_ns"] + paired_median = statistics.median( + auto / raw for auto, raw in zip(auto_elapsed, raw_elapsed) + ) + selected = result["modes"]["auto"]["selected_mode"] + reason = result["modes"]["auto"]["auto_policy_reason"] + gate_pass = True + if item["role"] == "holdout" and threshold is not None: + gate_pass = paired_median <= threshold + if not gate_pass: + holdout_failures.append(item["name"]) + summaries.append({ + "name": item["name"], + "role": item["role"], + "functional_complete": result["functional_complete"], + "baseline_valid_full_itc_hard_constraints": result[ + "baseline_valid_full_itc_hard_constraints" + ], + "instance_sha256": result["instance_sha256"], + "solution_sha256": result["solution_sha256"], + "model": result["model"], + "queries": result["queries"], + "sat": result["modes"]["auto"]["sat"], + "unsat": result["modes"]["auto"]["unsat"], + "proof_kinds": result["modes"]["auto"]["proof_kinds"], + "auto_selected_mode": selected, + "auto_policy_reason": reason, + "auto_vs_raw_median_ratio": result["auto_vs_raw_median_ratio"], + "auto_vs_raw_paired_median_ratio": paired_median, + "holdout_gate_pass": gate_pass, + "audit_sha256": (case_root / "audit.sha256").read_text().strip(), + }) + functional = all( + item["functional_complete"] and item["baseline_valid_full_itc_hard_constraints"] + for item in summaries + ) + result = { + "schema": SCHEMA + ".audit", + "functional_complete": functional, + "source_commit": manifest["source_commit"], + "dataset_commit": manifest["dataset_commit"], + "selector_policy": manifest["selector_policy"], + "query_count_per_case": manifest["query_count_per_case"], + "holdout_max_auto_raw_ratio": threshold, + "holdout_gate_pass": not holdout_failures, + "holdout_failures": holdout_failures, + "cases": summaries, + "interpretation": [ + "set9 is development evidence; set10 and set12 are prospective execution holdouts", + "the gate limits auto-policy overhead relative to the explicit raw control", + "all outputs remain complete proof-carrying conflict-core repair answers", + "this is not full ITC-2007 timetable feasibility or optimization", + "project-owned CI is not outside-team replication or adoption", + ], + } + payload = transfer.canonical_json(result) + path = root / "suite-audit.json" + if path.exists(): + expected = (root / "suite-audit.sha256").read_text().strip() + if transfer.read_bound(path, expected) != payload: + raise ValueError("existing suite audit differs from independent replay") + else: + transfer.write_once(path, payload) + transfer.write_once( + root / "suite-audit.sha256", (transfer.digest(payload) + "\n").encode() + ) + return result + + +def main(argv: Iterable[str] | None = None) -> int: + parser = argparse.ArgumentParser() + parser.add_argument("command", choices=("freeze", "run", "audit")) + parser.add_argument("--root", type=Path, required=True) + parser.add_argument("--upstream-root", type=Path) + parser.add_argument("--queries", type=int, default=1024) + parser.add_argument( + "--holdout-max-auto-raw-ratio", type=float, + default=DEFAULT_HOLDOUT_MAX_RATIO, + ) + args = parser.parse_args(argv) + if args.command == "freeze": + if args.upstream_root is None: + parser.error("freeze requires --upstream-root") + value = freeze( + args.root, args.upstream_root, query_count=args.queries, + holdout_max_auto_raw_ratio=args.holdout_max_auto_raw_ratio, + ) + elif args.command == "run": + value = run(args.root) + else: + value = audit(args.root) + print(json.dumps(value, indent=2, sort_keys=True, allow_nan=False)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/experiments/compiled_query/itc_exam_transfer.py b/experiments/compiled_query/itc_exam_transfer.py new file mode 100644 index 0000000..fbbc025 --- /dev/null +++ b/experiments/compiled_query/itc_exam_transfer.py @@ -0,0 +1,752 @@ +"""Proof-carrying bounded repair on a pinned ITC-2007 examination instance. + +This is a transfer study for the installed ``spectra.exact`` API, not a claim to +solve the complete capacitated timetabling objective. It starts from a published +feasible timetable, freezes exams involved in unsupported hard constraints, gives +other exams one deterministic duration-compatible alternative period, and solves +only the shared-student/EXCLUSION conflict core. Every result is replayed from the +stored SBC1 packet and SCQ2 evidence without trusting the native index. +""" +from __future__ import annotations + +import argparse +from collections import Counter, defaultdict +import hashlib +import json +from pathlib import Path +import shutil +import statistics +import subprocess +import sys +import time +from typing import Iterable + +from spectra.exact import ( + ExactRuntime, + build_exact_runtime, + decode_certified_output, + pack_validated_session_packet, + verify_session_output, +) +from spectra.exact_proof import decode_proof +from spectra.itc2007_exam import ITCExamInstance, parse_itc2007_exam + +SCHEMA = "spectra.itc2007.exam_repair_transfer.v1" +DATASET_REPOSITORY = "davidvanbulck/ITC-2007-CETT" +DATASET_COMMIT = "ed2d4c0cf5302b77a8b321cd0380de0bb579d538" +DEFAULT_INSTANCE = "examtt-instances/Instances/set9.exam" +DEFAULT_SOLUTION = "InitMethods/SolStore/set9_OBSIFeas_0.sol" +MODES = ("auto", "raw", "scc", "route") +WARMUPS = 1 +REPEATS = 5 +MAX_INPUT_BYTES = 64 << 20 +SOURCE_PATHS = ( + Path("pyproject.toml"), Path("README.md"), + Path("spectra/exact.py"), Path("spectra/exact_problem.py"), + Path("spectra/exact_proof.py"), Path("spectra/exam_repair.py"), + Path("spectra/itc2007_exam.py"), + Path("spectra/_native/exact_binary.cpp"), + Path("tests/public/test_exam_repair.py"), + Path("tests/public/test_itc2007_exam.py"), + Path("scripts/check_exam_repair_installation.py"), + Path("docs/EXAM_REPAIR.md"), Path("docs/README.md"), + Path("experiments/compiled_query/exact.py"), + Path("experiments/compiled_query/exact_native.cpp"), + Path("experiments/compiled_query/test_exact.py"), + Path("experiments/compiled_query/itc_exam_transfer.py"), + Path("experiments/compiled_query/itc_exam_suite.py"), + Path("experiments/compiled_query/test_itc_exam_transfer.py"), + Path("experiments/compiled_query/test_itc_exam_suite.py"), + Path("experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md"), + Path("experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md"), + Path(".github/workflows/itc-exam-transfer.yml"), + Path(".github/workflows/itc-exam-suite.yml"), +) + +def digest(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +def canonical_json(value: object) -> bytes: + return (json.dumps(value, sort_keys=True, separators=(",", ":"), + ensure_ascii=True, allow_nan=False) + "\n").encode() + + +def write_once(path: Path, data: bytes) -> str: + path.parent.mkdir(parents=True, exist_ok=True) + with path.open("xb") as stream: + stream.write(data) + return digest(data) + + +def deterministic_word(seed: int, *parts: int) -> int: + payload = seed.to_bytes(8, "little", signed=False) + for part in parts: + if type(part) is not int or part < 0: + raise ValueError("deterministic schedule parts must be nonnegative exact integers") + payload += part.to_bytes(8, "little", signed=False) + return int.from_bytes(hashlib.sha256(payload).digest()[:8], "little") + + +def read_bound(path: Path, expected: str | None = None, + *, max_bytes: int = MAX_INPUT_BYTES) -> bytes: + with path.open("rb") as stream: + data = stream.read(max_bytes + 1) + if len(data) > max_bytes: + raise ValueError(f"{path} exceeds the bounded read limit") + if expected is not None and digest(data) != expected: + raise ValueError(f"{path} hash differs") + return data + + +def parse_solution(text: str, instance: ITCExamInstance) -> tuple[tuple[int, ...], tuple[int, ...]]: + if type(text) is not str: + raise ValueError("solution must be an exact string") + periods: list[int] = [] + rooms: list[int] = [] + for line_number, raw in enumerate(text.replace("\r\n", "\n").replace("\r", "\n").split("\n"), 1): + line = raw.strip() + if not line: + continue + fields = tuple(value.strip() for value in line.split(",")) + if len(fields) != 2 or any(not value.isascii() or not value.isdigit() for value in fields): + raise ValueError(f"line {line_number}: solution row must be period,room") + period, room = map(int, fields) + if period >= len(instance.periods) or room >= len(instance.rooms): + raise ValueError(f"line {line_number}: solution index outside instance") + periods.append(period) + rooms.append(room) + if len(periods) != len(instance.exams): + raise ValueError("solution row count differs from exam count") + return tuple(periods), tuple(rooms) + + +def check_full_baseline(instance: ITCExamInstance, periods: tuple[int, ...], + rooms: tuple[int, ...]) -> None: + """Check the published timetable's hard constraints before deriving repairs.""" + if len(periods) != len(instance.exams) or len(rooms) != len(instance.exams): + raise ValueError("baseline geometry differs") + roster: dict[int, list[int]] = defaultdict(list) + for exam_index, exam in enumerate(instance.exams): + period = periods[exam_index] + room = rooms[exam_index] + if instance.periods[period].duration < exam.duration: + raise ValueError(f"baseline exam {exam_index} exceeds period duration") + for student in exam.students: + roster[student].append(exam_index) + if not 0 <= room < len(instance.rooms): + raise ValueError("baseline room outside bank") + for student, exams in roster.items(): + seen: set[int] = set() + for exam in exams: + if periods[exam] in seen: + raise ValueError(f"baseline repeats student {student} in one period") + seen.add(periods[exam]) + for left, right in instance.exclusions: + if periods[left] == periods[right]: + raise ValueError("baseline violates an EXCLUSION constraint") + for left, right in instance.coincidences: + if periods[left] != periods[right]: + raise ValueError("baseline violates an EXAM_COINCIDENCE constraint") + for later, earlier in instance.after: + if periods[later] <= periods[earlier]: + raise ValueError("baseline violates an AFTER constraint") + usage: dict[tuple[int, int], int] = defaultdict(int) + occupants: dict[tuple[int, int], list[int]] = defaultdict(list) + for exam_index, exam in enumerate(instance.exams): + key = (periods[exam_index], rooms[exam_index]) + usage[key] += len(exam.students) + occupants[key].append(exam_index) + for (period, room), count in usage.items(): + if count > instance.rooms[room].capacity: + raise ValueError(f"baseline room capacity exceeded at period {period}, room {room}") + for exam in instance.room_exclusive: + if len(occupants[periods[exam], rooms[exam]]) != 1: + raise ValueError("baseline violates ROOM_EXCLUSIVE") + + +def protected_exams(instance: ITCExamInstance) -> set[int]: + protected = set(instance.room_exclusive) + for left, right in (*instance.after, *instance.coincidences): + protected.add(left) + protected.add(right) + return protected + + +def derive_candidates(instance: ITCExamInstance, baseline_periods: tuple[int, ...], + *, seed: int) -> tuple[tuple[tuple[int, ...], ...], tuple[int, ...]]: + """Choose one deterministic alternative while retaining the baseline witness.""" + protected = protected_exams(instance) + rows: list[tuple[int, ...]] = [] + flexible: list[int] = [] + max_room = max((room.capacity for room in instance.rooms), default=0) + for exam_index, exam in enumerate(instance.exams): + base = baseline_periods[exam_index] + if exam_index in protected: + rows.append((base,)) + continue + alternatives = [ + period for period, record in enumerate(instance.periods) + if period != base and record.duration >= exam.duration + and len(exam.students) <= max_room + ] + if not alternatives: + rows.append((base,)) + continue + # Hash-shuffled choice avoids concentrating all repairs in the earliest + # periods while remaining fixed by the frozen source/solution identity. + alternatives.sort(key=lambda period: hashlib.sha256( + f"{seed}/{exam_index}/{period}".encode("ascii")).digest()) + alternate = alternatives[0] + rows.append((base, alternate)) + flexible.append(exam_index) + return tuple(rows), tuple(flexible) + + +def generate_queries(core, baseline_periods: tuple[int, ...], flexible: tuple[int, ...], + *, target: int, seed: int) -> tuple[tuple[tuple[int, int], ...], ...]: + if type(target) is not int or not 1 <= target <= 100_000: + raise ValueError("query target outside [1, 100000]") + model = core.model + names = model.period_ids + exam_names = model.exam_ids + alternatives: dict[int, str] = {} + for exam in flexible: + base_name = names[baseline_periods[exam]] + alternatives[exam] = next(name for name in model.candidates[exam] if name != base_name) + queries: list[tuple[tuple[int, int], ...]] = [] + seen: set[tuple[tuple[int, int], ...]] = set() + + def add(query: tuple[tuple[int, int], ...]) -> None: + if query not in seen: + seen.add(query) + queries.append(query) + + add(()) + for period in names: + add(model.freeze_event(closed_periods=(period,))) + for exam in flexible: + add(model.freeze_event(fixed=((exam_names[exam], alternatives[exam]),))) + attempts = 0 + while len(queries) < target and attempts < target * 200: + attempts += 1 + if not flexible: + break + maximum = min(12, len(flexible)) + width = (2 + deterministic_word(seed, attempts, 0) % (maximum - 1) + if maximum >= 2 else 1) + ranked = sorted( + flexible, + key=lambda exam: (deterministic_word(seed, attempts, 1, exam), exam), + ) + chosen = tuple(sorted(ranked[:width])) + fixed = tuple((exam_names[exam], alternatives[exam]) for exam in chosen) + if attempts % 3 == 0: + closed = (names[deterministic_word(seed, attempts, 2) % len(names)],) + query = model.freeze_event(closed_periods=closed, fixed=fixed) + else: + query = model.freeze_event(fixed=fixed) + add(query) + if len(queries) < target: + raise ValueError(f"could create only {len(queries)} distinct repair events") + return tuple(queries[:target]) + + +def _git(*args: str) -> str: + return subprocess.check_output(("git", *args), text=True).strip() + + +def source_inventory() -> dict[str, str]: + root = Path(__file__).resolve().parents[2] + return {str(path): digest((root / path).read_bytes()) for path in SOURCE_PATHS} + + +def validate_source_commit(commit: str, inventory: dict[str, str]) -> str: + if (type(commit) is not str or len(commit) != 40 + or any(character not in "0123456789abcdef" for character in commit)): + raise ValueError("source_commit must be a full lowercase commit SHA") + resolved = _git("rev-parse", "--verify", commit + "^{commit}") + if resolved != commit: + raise ValueError("source_commit must identify the commit itself") + for path, expected in inventory.items(): + try: + data = subprocess.check_output(("git", "show", f"{commit}:{path}")) + except subprocess.CalledProcessError as error: + raise ValueError(f"source commit does not contain {path}") from error + if digest(data) != expected: + raise ValueError(f"working source differs from source_commit at {path}") + return _git("rev-parse", commit + "^{tree}") + + +def freeze(root: Path, instance_path: Path, solution_path: Path, *, query_count: int, + license_path: Path | None = None, source_commit: str | None = None, + dataset_instance_path: str = DEFAULT_INSTANCE, + dataset_solution_path: str = DEFAULT_SOLUTION, + evaluation_role: str = "development") -> dict: + root = root.resolve() + if root.exists(): + raise FileExistsError(root) + if license_path is None: + raise ValueError("freeze requires the upstream redistribution license") + if (type(dataset_instance_path) is not str or not dataset_instance_path + or type(dataset_solution_path) is not str or not dataset_solution_path): + raise ValueError("dataset paths must be nonempty exact strings") + if evaluation_role not in ("development", "holdout", "replication"): + raise ValueError("evaluation_role must be development, holdout or replication") + instance_bytes = read_bound(instance_path) + solution_bytes = read_bound(solution_path) + license_bytes = read_bound(license_path) + instance = parse_itc2007_exam(instance_bytes.decode("utf-8")) + baseline_periods, baseline_rooms = parse_solution(solution_bytes.decode("utf-8"), instance) + check_full_baseline(instance, baseline_periods, baseline_rooms) + seed = int.from_bytes(hashlib.sha256(instance_bytes + b"\0" + solution_bytes).digest()[:8], "little") + if len(instance.periods) > 64: + raise ValueError("selected ITC instance exceeds the exact API's 64-period palette") + candidates, flexible = derive_candidates(instance, baseline_periods, seed=seed) + core = instance.conflict_core(candidates, acknowledge_ignored_constraints=True) + if not core.model.problem.check(bytes(baseline_periods)): + raise ValueError("published baseline does not witness the derived conflict core") + queries = generate_queries(core, baseline_periods, flexible, target=query_count, seed=seed) + packet = pack_validated_session_packet(core.model.problem, queries) + inventory = source_inventory() + commit = source_commit or _git("rev-parse", "HEAD") + source_tree: str | None = None + if source_commit is None: + changed = _git("status", "--porcelain", "--", *(str(path) for path in SOURCE_PATHS)) + if changed: + raise ValueError("commit the transfer sources before freezing evidence") + source_tree = validate_source_commit(commit, inventory) + elif type(source_commit) is not str or not source_commit: + raise ValueError("source_commit fixture identity must be a nonempty string") + + state = { + "baseline_periods": baseline_periods, + "baseline_rooms": baseline_rooms, + "candidate_periods": candidates, + "flexible_exams": flexible, + "protected_exams": tuple(sorted(protected_exams(instance))), + "seed": seed, + } + staging = root.with_name(root.name + ".partial") + if staging.exists(): + raise FileExistsError(staging) + staging.mkdir(parents=True, exist_ok=False) + try: + artifacts = { + "inputs/instance.exam": write_once(staging / "inputs/instance.exam", instance_bytes), + "inputs/baseline.sol": write_once(staging / "inputs/baseline.sol", solution_bytes), + "inputs/UPSTREAM_LICENSE.txt": write_once( + staging / "inputs/UPSTREAM_LICENSE.txt", license_bytes + ), + "candidates.json": write_once(staging / "candidates.json", canonical_json(state)), + "queries.json": write_once(staging / "queries.json", canonical_json(queries)), + "session.sbc1": write_once(staging / "session.sbc1", packet), + } + manifest = { + "schema": SCHEMA, + "classification": ( + "published ITC-2007 input and feasible schedule; deterministic bounded " + "conflict-core transfer, not full timetabling or outside-team replication" + ), + "source_commit": commit, + "source_tree": source_tree, + "source_inventory": inventory, + "dataset_repository": DATASET_REPOSITORY, + "dataset_commit": DATASET_COMMIT, + "dataset_instance_path": dataset_instance_path, + "dataset_solution_path": dataset_solution_path, + "evaluation_role": evaluation_role, + "instance_sha256": digest(instance_bytes), + "solution_sha256": digest(solution_bytes), + "upstream_acknowledgment": ( + "This product includes software/data distributed by David Van Bulck, " + "Dries Goossens, and Andrea Schaerf, Ghent University, Belgium " + "(https://github.com/davidvanbulck/ITC-2007-CETT.git)." + ), + "upstream_license_sha256": digest(license_bytes), + "model": core.info, + "candidate_policy": ( + "published baseline; freeze AFTER/coincidence/room-exclusive exams; " + "one hash-selected duration/individual-room-compatible alternative otherwise" + ), + "query_policy": ( + "base, every single-period closure, every single-exam move, then seeded " + "multi-move and closure-plus-move events" + ), + "query_count": len(queries), + "modes": MODES, + "warmups": WARMUPS, + "repeats": REPEATS, + "timing_schedule": "one warmup per mode; measured modes rotate by repetition", + "timing_scope": ( + "ready immutable SBC1 through construction, decisions, full evidence, " + "independent native check, SCQ2 materialization and disposal" + ), + "artifacts": artifacts, + } + manifest_bytes = canonical_json(manifest) + write_once(staging / "manifest.json", manifest_bytes) + write_once(staging / "manifest.sha256", (digest(manifest_bytes) + "\n").encode()) + staging.rename(root) + return manifest + except BaseException: + shutil.rmtree(staging, ignore_errors=True) + raise + + +def load_manifest(root: Path) -> dict: + expected = (root / "manifest.sha256").read_text().strip() + manifest_bytes = read_bound(root / "manifest.json", expected) + manifest = json.loads(manifest_bytes) + if (manifest.get("schema") != SCHEMA or tuple(manifest.get("modes", ())) != MODES + or type(manifest.get("warmups")) is not int or manifest["warmups"] < 0 + or type(manifest.get("repeats")) is not int or manifest["repeats"] < 1 + or type(manifest.get("query_count")) is not int or manifest["query_count"] < 1 + or manifest.get("timing_schedule") + != "one warmup per mode; measured modes rotate by repetition"): + raise ValueError("transfer manifest schema, modes or schedule differ") + if (manifest.get("dataset_repository") != DATASET_REPOSITORY + or manifest.get("dataset_commit") != DATASET_COMMIT + or type(manifest.get("dataset_instance_path")) is not str + or not manifest["dataset_instance_path"] + or type(manifest.get("dataset_solution_path")) is not str + or not manifest["dataset_solution_path"] + or manifest.get("evaluation_role") not in + ("development", "holdout", "replication")): + raise ValueError("transfer dataset identity differs") + inventory = manifest.get("source_inventory") + if type(inventory) is not dict or inventory != source_inventory(): + raise ValueError("transfer source inventory differs") + if manifest.get("source_tree") is not None: + if validate_source_commit(manifest.get("source_commit"), inventory) != manifest["source_tree"]: + raise ValueError("transfer source tree differs") + required = {"inputs/instance.exam", "inputs/baseline.sol", "candidates.json", + "queries.json", "session.sbc1", "inputs/UPSTREAM_LICENSE.txt"} + inventory = set(manifest.get("artifacts", ())) + if inventory != required: + raise ValueError("transfer manifest artifact inventory differs") + for name, checksum in manifest["artifacts"].items(): + read_bound(root / name, checksum) + if manifest["artifacts"]["inputs/instance.exam"] != manifest.get("instance_sha256"): + raise ValueError("manifest instance identity differs") + if manifest["artifacts"]["inputs/baseline.sol"] != manifest.get("solution_sha256"): + raise ValueError("manifest solution identity differs") + if (manifest["artifacts"]["inputs/UPSTREAM_LICENSE.txt"] + != manifest.get("upstream_license_sha256")): + raise ValueError("manifest upstream-license identity differs") + return manifest + + +def reconstruct(root: Path, manifest: dict): + instance_bytes = read_bound( + root / "inputs/instance.exam", manifest["artifacts"]["inputs/instance.exam"] + ) + solution_bytes = read_bound( + root / "inputs/baseline.sol", manifest["artifacts"]["inputs/baseline.sol"] + ) + instance = parse_itc2007_exam(instance_bytes.decode("utf-8")) + baseline_periods, baseline_rooms = parse_solution(solution_bytes.decode("utf-8"), instance) + check_full_baseline(instance, baseline_periods, baseline_rooms) + seed = int.from_bytes( + hashlib.sha256(instance_bytes + b"\0" + solution_bytes).digest()[:8], "little" + ) + candidates, flexible = derive_candidates(instance, baseline_periods, seed=seed) + expected_state = { + "baseline_periods": baseline_periods, + "baseline_rooms": baseline_rooms, + "candidate_periods": candidates, + "flexible_exams": flexible, + "protected_exams": tuple(sorted(protected_exams(instance))), + "seed": seed, + } + state = json.loads(read_bound( + root / "candidates.json", manifest["artifacts"]["candidates.json"] + )) + if canonical_json(state) != canonical_json(expected_state): + raise ValueError("stored candidate policy differs from original inputs") + core = instance.conflict_core(candidates, acknowledge_ignored_constraints=True) + if core.info != manifest.get("model"): + raise ValueError("stored model receipt differs from reconstructed inputs") + queries = tuple(tuple(tuple(pin) for pin in row) for row in json.loads(read_bound( + root / "queries.json", manifest["artifacts"]["queries.json"] + ))) + expected_queries = generate_queries( + core, baseline_periods, flexible, + target=manifest["query_count"], seed=seed, + ) + if queries != expected_queries: + raise ValueError("stored query bank differs from deterministic policy") + packet = read_bound(root / "session.sbc1", manifest["artifacts"]["session.sbc1"]) + if pack_validated_session_packet(core.model.problem, queries) != packet: + raise ValueError("stored packet differs from reconstructed original inputs") + if not core.model.problem.check(bytes(baseline_periods)): + raise ValueError("stored baseline no longer witnesses the reconstructed core") + return instance, state, core, queries + + +def run(root: Path) -> dict: + root = root.resolve() + manifest = load_manifest(root) + reconstruct(root, manifest) + if (root / "run.json").exists() or (root / "outputs").exists() or (root / "native-build").exists(): + raise FileExistsError("transfer execution already exists") + packet = read_bound(root / "session.sbc1", manifest["artifacts"]["session.sbc1"]) + build = root / "native-build" + library = build_exact_runtime(build) + runtime = ExactRuntime(library) + states: dict[str, dict[str, object]] = { + mode: {"elapsed_ns": [], "output": None, "metadata": None} for mode in MODES + } + execution_order: list[list[str]] = [] + + def execute(mode: str, *, measured: bool) -> None: + start = time.perf_counter_ns() + result = runtime.solve_session_packet(packet, mode=mode) + elapsed = time.perf_counter_ns() - start + if not verify_session_output(packet, result.output): + raise AssertionError(f"{mode} output failed standard-library replay") + current = { + "query_count": result.query_count, + "sat_count": result.sat_count, + "unsat_count": result.unsat_count, + "proof_bytes": result.proof_bytes, + "visited": result.visited, + "arcs_scanned": result.arcs_scanned, + "selected_mode": result.info.get("selected_mode", mode), + "bank_query_count": result.info.get("bank_query_count"), + "bank_pin_count": result.info.get("bank_pin_count"), + "bank_kernel": result.info.get("bank_kernel"), + "bank_tiles": result.info.get("bank_tiles"), + "auto_policy": result.info.get("auto_policy"), + "auto_policy_reason": result.info.get("auto_policy_reason"), + } + if (current["query_count"] != manifest["query_count"] + or current["sat_count"] + current["unsat_count"] != manifest["query_count"] + or current["bank_query_count"] != manifest["query_count"] + or any(type(current[name]) is not int or current[name] < 0 + for name in ("proof_bytes", "visited", "arcs_scanned", + "bank_pin_count", "bank_tiles")) + or current["selected_mode"] not in ("raw", "scc", "route") + or current["bank_kernel"] not in ("serial", "tile64") + or current["auto_policy"] not in ("explicit", "structural-v2") + or type(current["auto_policy_reason"]) is not str + or (mode == "auto" and current["auto_policy"] != "structural-v2") + or (mode != "auto" and (current["selected_mode"] != mode + or current["auto_policy"] != "explicit"))): + raise AssertionError(f"{mode} returned inconsistent metadata") + state = states[mode] + if state["output"] is None: + state["output"], state["metadata"] = result.output, current + elif state["output"] != result.output or state["metadata"] != current: + raise AssertionError(f"{mode} result changed across identical calls") + if measured: + elapsed_rows = state["elapsed_ns"] + assert isinstance(elapsed_rows, list) + elapsed_rows.append(elapsed) + + for _ in range(manifest["warmups"]): + for mode in MODES: + execute(mode, measured=False) + for repeat in range(manifest["repeats"]): + offset = repeat % len(MODES) + order = (*MODES[offset:], *MODES[:offset]) + execution_order.append(list(order)) + for mode in order: + execute(mode, measured=True) + + records: dict[str, object] = { + "schema": SCHEMA + ".run", + "manifest_sha256": (root / "manifest.sha256").read_text().strip(), + "build_receipt_sha256": digest((build / "build.json").read_bytes()), + "warmups": manifest["warmups"], + "execution_order": execution_order, + "modes": {}, + } + for mode in MODES: + state = states[mode] + output = state["output"] + metadata = state["metadata"] + elapsed = state["elapsed_ns"] + assert isinstance(output, bytes) and isinstance(metadata, dict) and isinstance(elapsed, list) + if len(elapsed) != manifest["repeats"]: + raise AssertionError(f"{mode} timing count differs") + output_name = f"outputs/{mode}.scq2" + output_hash = write_once(root / output_name, output) + records["modes"][mode] = { + **metadata, + "elapsed_ns": elapsed, + "output": output_name, + "output_sha256": output_hash, + } + run_bytes = canonical_json(records) + write_once(root / "run.json", run_bytes) + write_once(root / "run.sha256", (digest(run_bytes) + "\n").encode()) + return records + + +def audit(root: Path) -> dict: + root = root.resolve() + manifest = load_manifest(root) + run_hash = (root / "run.sha256").read_text().strip() + record = json.loads(read_bound(root / "run.json", run_hash)) + if record.get("schema") != SCHEMA + ".run" or set(record.get("modes", ())) != set(MODES): + raise ValueError("run schema or mode inventory differs") + if record.get("manifest_sha256") != (root / "manifest.sha256").read_text().strip(): + raise ValueError("run belongs to a different frozen manifest") + expected_order = [] + for repeat in range(manifest["repeats"]): + offset = repeat % len(MODES) + expected_order.append(list((*MODES[offset:], *MODES[:offset]))) + if (record.get("warmups") != manifest.get("warmups") + or record.get("execution_order") != expected_order): + raise ValueError("run warmup or rotated timing schedule differs") + packet = read_bound(root / "session.sbc1", manifest["artifacts"]["session.sbc1"]) + instance, state, core, queries = reconstruct(root, manifest) + receipt = read_bound(root / "native-build/build.json") + if digest(receipt) != record.get("build_receipt_sha256"): + raise ValueError("native build receipt hash differs") + decisions: tuple[int, ...] | None = None + summaries = {} + sample = None + for mode in MODES: + item = record["modes"][mode] + if type(item) is not dict or item.get("output") != f"outputs/{mode}.scq2": + raise ValueError(f"{mode} output location differs") + elapsed = item.get("elapsed_ns") + if (type(elapsed) is not list or len(elapsed) != manifest["repeats"] + or any(type(value) is not int or value <= 0 for value in elapsed)): + raise ValueError(f"{mode} timing schedule differs") + output = read_bound(root / item["output"], item["output_sha256"]) + if not verify_session_output(packet, output): + raise ValueError(f"{mode} output fails replay") + rows = decode_certified_output(output, core.model.problem.n, len(queries)) + current = tuple(code for code, _, _ in rows) + sat_count = sum(current) + unsat_count = len(current) - sat_count + proof_bytes = sum(len(proof) for code, _labels, proof in rows if not code) + selected = item.get("selected_mode") + policy = item.get("auto_policy") + reason = item.get("auto_policy_reason") + if (item.get("query_count") != len(queries) + or item.get("bank_query_count") != len(queries) + or item.get("sat_count") != sat_count + or item.get("unsat_count") != unsat_count + or item.get("proof_bytes") != proof_bytes + or any(type(item.get(name)) is not int or item[name] < 0 + for name in ("visited", "arcs_scanned", "bank_pin_count", "bank_tiles")) + or item.get("bank_kernel") not in ("serial", "tile64") + or selected not in ("raw", "scc", "route") + or policy not in ("explicit", "structural-v2") + or type(reason) is not str + or (mode == "auto" and policy != "structural-v2") + or (mode != "auto" and (selected != mode or policy != "explicit"))): + raise ValueError(f"{mode} metadata differs from certified output") + if decisions is None: + decisions = current + elif decisions != current: + raise ValueError("engine modes disagree on SAT/UNSAT decisions") + kinds = Counter() + for index, (code, _labels, proof) in enumerate(rows): + if not code: + kind, _, _ = decode_proof(proof, core.model.problem.n) + kinds[str(kind)] += 1 + if sample is None: + sample = { + "query_index": index, + "mode": mode, + "explanation": core.model.explain_unsat(queries[index], proof), + } + summaries[mode] = { + "median_elapsed_ns": statistics.median(elapsed), + "minimum_elapsed_ns": min(elapsed), + "maximum_elapsed_ns": max(elapsed), + "sat": sat_count, + "unsat": unsat_count, + "proof_kinds": dict(kinds), + "selected_mode": selected, + "bank_query_count": item["bank_query_count"], + "bank_pin_count": item["bank_pin_count"], + "bank_kernel": item["bank_kernel"], + "bank_tiles": item["bank_tiles"], + "auto_policy": policy, + "auto_policy_reason": reason, + "output_sha256": item["output_sha256"], + } + result = { + "schema": SCHEMA + ".audit", + "functional_complete": decisions is not None and len(decisions) == manifest["query_count"], + "source_commit": manifest["source_commit"], + "dataset_commit": manifest["dataset_commit"], + "dataset_instance_path": manifest["dataset_instance_path"], + "dataset_solution_path": manifest["dataset_solution_path"], + "evaluation_role": manifest["evaluation_role"], + "instance_sha256": manifest["instance_sha256"], + "solution_sha256": manifest["solution_sha256"], + "model": core.info, + "baseline_valid_full_itc_hard_constraints": True, + "flexible_exams": len(state["flexible_exams"]), + "protected_exams": len(state["protected_exams"]), + "queries": len(queries), + "warmups": manifest["warmups"], + "repeats": manifest["repeats"], + "timing_schedule": manifest["timing_schedule"], + "modes": summaries, + "auto_vs_raw_median_ratio": ( + summaries["auto"]["median_elapsed_ns"] / summaries["raw"]["median_elapsed_ns"] + ), + "sample_unsat": sample, + "limitations": [ + "conflict-core bounded repair, not complete ITC-2007 timetabling", + "room reassignment and soft objective are not solved", + "project-owned execution, not outside-team replication", + "ready-packet timing excludes candidate generation, packing and compilation", + ], + } + audit_bytes = canonical_json(result) + audit_path = root / "audit.json" + if audit_path.exists(): + expected = (root / "audit.sha256").read_text().strip() + existing = read_bound(audit_path, expected) + if existing != audit_bytes: + raise ValueError("existing audit differs from independent replay") + else: + write_once(audit_path, audit_bytes) + write_once(root / "audit.sha256", (digest(audit_bytes) + "\n").encode()) + return result + + +def main(argv: Iterable[str] | None = None) -> int: + parser = argparse.ArgumentParser() + parser.add_argument("command", choices=("freeze", "run", "audit")) + parser.add_argument("--root", type=Path, required=True) + parser.add_argument("--instance", type=Path) + parser.add_argument("--solution", type=Path) + parser.add_argument("--queries", type=int, default=1024) + parser.add_argument("--license", type=Path) + parser.add_argument("--dataset-instance-path", default=DEFAULT_INSTANCE) + parser.add_argument("--dataset-solution-path", default=DEFAULT_SOLUTION) + parser.add_argument( + "--evaluation-role", choices=("development", "holdout", "replication"), + default="development", + ) + args = parser.parse_args(argv) + if args.command == "freeze": + if args.instance is None or args.solution is None: + parser.error("freeze requires --instance and --solution") + value = freeze( + args.root, args.instance, args.solution, query_count=args.queries, + license_path=args.license, + dataset_instance_path=args.dataset_instance_path, + dataset_solution_path=args.dataset_solution_path, + evaluation_role=args.evaluation_role, + ) + elif args.command == "run": + value = run(args.root) + else: + value = audit(args.root) + print(json.dumps(value, indent=2, sort_keys=True, allow_nan=False)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/experiments/compiled_query/test_exact.py b/experiments/compiled_query/test_exact.py index c7042e0..4cc8d54 100644 --- a/experiments/compiled_query/test_exact.py +++ b/experiments/compiled_query/test_exact.py @@ -450,7 +450,10 @@ def test_tiled_witnesses_keep_high_colours_and_last_lane(exact_runtime, mode): if index % 3 and rng.random() < .3)) rows = tuple(rows) expected = [] - with exact_runtime.prepare(p, mode='scc' if mode == 'auto' else mode) as session: + # The bank averages well above eight pins per request, so structural-v2 + # intentionally selects raw rather than paying for tile64 propagation. + expected_mode = 'raw' if mode == 'auto' else mode + with exact_runtime.prepare(p, mode=expected_mode) as session: for query in rows: answer = session.solve(query) assert answer.status == 'SAT_VERIFIED' @@ -459,9 +462,29 @@ def test_tiled_witnesses_keep_high_colours_and_last_lane(exact_runtime, mode): for count in (64, 65, 129): answer = exact_runtime.solve_session_packet(pack_session_packet(p, rows[:count]), mode=mode) assert answer.sat_count == count and answer.proof_bytes == 0 + if mode == 'auto': + assert answer.info['selected_mode'] == 'raw' + assert answer.info['auto_policy'] == 'structural-v2' + assert answer.info['auto_policy_reason'] == 'high_pin_density' assert decode_certified_output(answer.output, n, count) == tuple(expected[:count]) +def test_auto_structural_v2_freezes_the_eight_pin_density_boundary(exact_runtime): + p = BinaryListProblem.create(16, 2, (), (3,) * 16) + low_rows = tuple(tuple((v, 3) for v in range(7)) for _ in range(64)) + high_rows = tuple(tuple((v, 3) for v in range(8)) for _ in range(64)) + low = exact_runtime.solve_session_packet(pack_session_packet(p, low_rows), mode='auto') + high = exact_runtime.solve_session_packet(pack_session_packet(p, high_rows), mode='auto') + assert low.info['selected_mode'] == 'scc' + assert low.info['auto_policy_reason'] == 'scc_tile64' + assert low.info['bank_query_count'] == 64 and low.info['bank_pin_count'] == 448 + assert high.info['selected_mode'] == 'raw' + assert high.info['auto_policy_reason'] == 'high_pin_density' + assert high.info['bank_query_count'] == 64 and high.info['bank_pin_count'] == 512 + assert high.output == exact_runtime.solve_session_packet( + pack_session_packet(p, high_rows), mode='raw').output + + @pytest.mark.parametrize('count', (0, 1, 63, 64, 65, 129)) @pytest.mark.parametrize('structure', ('empty', 'independent', 'chain', 'odd_cycle')) def test_auto_packet_exposes_and_matches_its_selected_engine(exact_runtime, count, structure): @@ -477,6 +500,8 @@ def test_auto_packet_exposes_and_matches_its_selected_engine(exact_runtime, coun selected = ('raw' if count < 64 or structure == 'odd_cycle' else 'route' if structure in ('chain', 'empty') else 'scc') assert answer.info['mode'] == 'auto' + assert answer.info['auto_policy'] == 'structural-v2' + assert answer.info['bank_query_count'] == count assert answer.info['selected_mode'] == selected assert answer.output == exact_runtime.solve_session_packet(packet, mode=selected).output for query, (decision, labels, certificate) in zip(rows, decode_certified_output(answer.output, n, count)): diff --git a/experiments/compiled_query/test_itc_exam_suite.py b/experiments/compiled_query/test_itc_exam_suite.py new file mode 100644 index 0000000..79b00aa --- /dev/null +++ b/experiments/compiled_query/test_itc_exam_suite.py @@ -0,0 +1,76 @@ +"""Contracts for the prospective multi-instance ITC transfer suite.""" +from __future__ import annotations + +import json +from pathlib import Path + +import pytest + +from experiments.compiled_query import itc_exam_suite as suite +from experiments.compiled_query import itc_exam_transfer as transfer +from experiments.compiled_query.test_itc_exam_transfer import INSTANCE, SOLUTION + + +def fixture_cases(upstream: Path) -> tuple[suite.SuiteCase, ...]: + records = ( + suite.SuiteCase("fixture-development", "development", "instances/dev.exam", "solutions/dev.sol"), + suite.SuiteCase("fixture-holdout-a", "holdout", "instances/a.exam", "solutions/a.sol"), + suite.SuiteCase("fixture-holdout-b", "holdout", "instances/b.exam", "solutions/b.sol"), + ) + (upstream / "instances").mkdir(parents=True) + (upstream / "solutions").mkdir(parents=True) + for case in records: + (upstream / case.instance_path).write_text(INSTANCE) + (upstream / case.solution_path).write_text(SOLUTION) + (upstream / "LICENSE").write_text("fixture redistribution license\n") + return records + + +def test_case_validation_rejects_escape_and_missing_holdout(): + with pytest.raises(ValueError, match="under upstream root"): + suite.SuiteCase("bad", "holdout", "../bad.exam", "x.sol").validate() + with pytest.raises(ValueError, match="holdout"): + suite._cases((suite.SuiteCase("dev", "development", "x.exam", "x.sol"),)) + + +def test_suite_freeze_run_and_audit(tmp_path, monkeypatch): + upstream = tmp_path / "upstream" + cases = fixture_cases(upstream) + root = tmp_path / "suite" + monkeypatch.setattr(transfer, "WARMUPS", 0) + monkeypatch.setattr(transfer, "REPEATS", 1) + manifest = suite.freeze( + root, upstream, cases=cases, query_count=8, + holdout_max_auto_raw_ratio=None, + source_commit="fixture-source", + ) + assert [item["role"] for item in manifest["cases"]] == [ + "development", "holdout", "holdout" + ] + assert manifest["holdout_max_auto_raw_ratio"] is None + run = suite.run(root) + assert len(run["cases"]) == 3 + result = suite.audit(root) + assert result["functional_complete"] + assert result["holdout_gate_pass"] + assert result["holdout_failures"] == [] + assert all(case["queries"] == 8 for case in result["cases"]) + assert all(case["auto_vs_raw_paired_median_ratio"] > 0 for case in result["cases"]) + assert json.loads((root / "suite-audit.json").read_text()) == result + + +def test_suite_detects_child_manifest_substitution(tmp_path, monkeypatch): + upstream = tmp_path / "upstream" + cases = fixture_cases(upstream) + root = tmp_path / "suite" + monkeypatch.setattr(transfer, "WARMUPS", 0) + monkeypatch.setattr(transfer, "REPEATS", 1) + suite.freeze( + root, upstream, cases=cases, query_count=8, + holdout_max_auto_raw_ratio=None, + source_commit="fixture-source", + ) + child = root / "cases" / cases[1].name / "manifest.sha256" + child.write_text("0" * 64 + "\n") + with pytest.raises(ValueError, match="manifest hash differs"): + suite.load_manifest(root) diff --git a/experiments/compiled_query/test_itc_exam_transfer.py b/experiments/compiled_query/test_itc_exam_transfer.py new file mode 100644 index 0000000..8795156 --- /dev/null +++ b/experiments/compiled_query/test_itc_exam_transfer.py @@ -0,0 +1,179 @@ +"""End-to-end contracts for the ITC exam bounded-repair transfer harness.""" +from __future__ import annotations + +import json +from pathlib import Path + +import pytest + +from experiments.compiled_query import itc_exam_transfer as transfer +from spectra.itc2007_exam import parse_itc2007_exam + + +INSTANCE = """[Exams:5] +120, 1, 2 +180, 2, 3 +120, 9 +120, 4 +120, 4 +[Periods:4] +01:01:2030, 09:00:00, 180, 0 +01:01:2030, 14:00:00, 120, 5 +02:01:2030, 09:00:00, 240, 0 +02:01:2030, 14:00:00, 180, 0 +[Rooms:1] +100, 0 +[PeriodHardConstraints] +0, EXCLUSION, 2 +1, AFTER, 0 +[RoomHardConstraints] +2, ROOM_EXCLUSIVE +[InstitutionalWeightings] +TWOINAROW, 30 +""" +SOLUTION = """0, 0 +2, 0 +1, 0 +0, 0 +3, 0 +""" + + +def write_inputs(tmp_path: Path) -> tuple[Path, Path, Path]: + instance = tmp_path / "fixture.exam" + solution = tmp_path / "fixture.sol" + instance.write_text(INSTANCE) + solution.write_text(SOLUTION) + license_path = tmp_path / "LICENSE" + license_path.write_text("fixture redistribution license\n") + return instance, solution, license_path + + +def test_solution_parser_and_full_hard_constraint_check(): + instance = parse_itc2007_exam(INSTANCE) + periods, rooms = transfer.parse_solution(SOLUTION, instance) + transfer.check_full_baseline(instance, periods, rooms) + assert periods == (0, 2, 1, 0, 3) + assert transfer.protected_exams(instance) == {0, 1, 2} + with pytest.raises(ValueError, match="AFTER"): + transfer.check_full_baseline(instance, (2, 0, 1, 0, 3), rooms) + + +def test_candidate_policy_retains_baseline_and_flexes_unprotected_exams(): + instance = parse_itc2007_exam(INSTANCE) + periods, _ = transfer.parse_solution(SOLUTION, instance) + candidates, flexible = transfer.derive_candidates(instance, periods, seed=7) + assert candidates[0] == (0,) and candidates[1] == (2,) and candidates[2] == (1,) + assert flexible == (3, 4) + assert all(periods[index] in candidates[index] for index in range(5)) + + +def test_freeze_run_and_independent_audit(tmp_path, monkeypatch): + instance, solution, license_path = write_inputs(tmp_path) + root = tmp_path / "evidence" + monkeypatch.setattr(transfer, "WARMUPS", 0) + monkeypatch.setattr(transfer, "REPEATS", 2) + manifest = transfer.freeze( + root, instance, solution, query_count=8, license_path=license_path, + source_commit="fixture-source", + dataset_instance_path="fixtures/custom.exam", + dataset_solution_path="fixtures/custom.sol", + evaluation_role="holdout", + ) + assert manifest["query_count"] == 8 + assert manifest["model"]["exams"] == 5 + assert manifest["dataset_instance_path"] == "fixtures/custom.exam" + assert manifest["dataset_solution_path"] == "fixtures/custom.sol" + assert manifest["evaluation_role"] == "holdout" + assert manifest["warmups"] == 0 and manifest["repeats"] == 2 + record = transfer.run(root) + assert tuple(record["modes"]) == transfer.MODES + assert record["warmups"] == 0 + assert record["execution_order"] == [ + ["auto", "raw", "scc", "route"], + ["raw", "scc", "route", "auto"], + ] + result = transfer.audit(root) + assert result["functional_complete"] + assert result["baseline_valid_full_itc_hard_constraints"] + assert result["flexible_exams"] == 2 + assert result["protected_exams"] == 3 + assert result["queries"] == 8 + assert result["evaluation_role"] == "holdout" + assert result["dataset_instance_path"] == "fixtures/custom.exam" + assert result["warmups"] == 0 and result["repeats"] == 2 + assert result["auto_vs_raw_median_ratio"] > 0 + assert all(item["sat"] + item["unsat"] == 8 for item in result["modes"].values()) + assert result["modes"]["auto"]["auto_policy"] == "structural-v2" + assert result["modes"]["auto"]["bank_query_count"] == 8 + assert result["modes"]["raw"]["auto_policy"] == "explicit" + assert json.loads((root / "audit.json").read_text()) == result + + + +def test_manifest_rejects_invalid_role_and_schedule(tmp_path): + instance, solution, license_path = write_inputs(tmp_path) + with pytest.raises(ValueError, match="evaluation_role"): + transfer.freeze( + tmp_path / "bad-role", instance, solution, query_count=8, + license_path=license_path, source_commit="fixture-source", + evaluation_role="training", + ) + + root = tmp_path / "evidence" + transfer.freeze( + root, instance, solution, query_count=8, license_path=license_path, + source_commit="fixture-source", + ) + manifest_path = root / "manifest.json" + manifest = json.loads(manifest_path.read_text()) + manifest["timing_schedule"] = "mode-by-mode" + payload = transfer.canonical_json(manifest) + manifest_path.write_bytes(payload) + (root / "manifest.sha256").write_text(transfer.digest(payload) + "\n") + with pytest.raises(ValueError, match="schedule differ"): + transfer.load_manifest(root) + +def test_frozen_artifact_hash_mutation_is_rejected(tmp_path): + instance, solution, license_path = write_inputs(tmp_path) + root = tmp_path / "evidence" + transfer.freeze(root, instance, solution, query_count=8, license_path=license_path, + source_commit="fixture-source") + packet = root / "session.sbc1" + packet.write_bytes(packet.read_bytes() + b"x") + with pytest.raises(ValueError, match="hash differs"): + transfer.load_manifest(root) + + +def test_audit_rederives_candidates_and_queries_instead_of_trusting_json(tmp_path): + instance, solution, license_path = write_inputs(tmp_path) + root = tmp_path / "evidence" + transfer.freeze(root, instance, solution, query_count=8, license_path=license_path, + source_commit="fixture-source") + + state_path = root / "candidates.json" + state = json.loads(state_path.read_text()) + state["seed"] += 1 + state_bytes = transfer.canonical_json(state) + state_path.write_bytes(state_bytes) + manifest_path = root / "manifest.json" + manifest = json.loads(manifest_path.read_text()) + manifest["artifacts"]["candidates.json"] = transfer.digest(state_bytes) + manifest_bytes = transfer.canonical_json(manifest) + manifest_path.write_bytes(manifest_bytes) + (root / "manifest.sha256").write_text(transfer.digest(manifest_bytes) + "\n") + + loaded = transfer.load_manifest(root) + with pytest.raises(ValueError, match="candidate policy differs"): + transfer.reconstruct(root, loaded) + + +def test_failed_freeze_does_not_publish_a_partial_evidence_root(tmp_path): + instance, solution, license_path = write_inputs(tmp_path) + root = tmp_path / "evidence" + solution.write_text("0, 0\n") + with pytest.raises(ValueError, match="row count differs"): + transfer.freeze(root, instance, solution, query_count=8, license_path=license_path, + source_commit="fixture-source") + assert not root.exists() + assert not root.with_name(root.name + ".partial").exists() diff --git a/scripts/check_exam_repair_installation.py b/scripts/check_exam_repair_installation.py new file mode 100644 index 0000000..f523897 --- /dev/null +++ b/scripts/check_exam_repair_installation.py @@ -0,0 +1,89 @@ +"""Exercise the installed exam-repair API without repository imports.""" +from __future__ import annotations + +import argparse +import json +from pathlib import Path +import tempfile + +from spectra.exam_repair import ExamRepairModel +from spectra.exact import ExactRuntime, build_exact_runtime, verify_answer +from spectra.itc2007_exam import parse_itc2007_exam + +FIXTURE = """[Exams:3] +120, 7 +120, 7, 9 +120, 9 +[Periods:2] +01:01:2030, 09:00:00, 180, 0 +01:01:2030, 14:00:00, 180, 0 +[Rooms:1] +100, 0 +[PeriodHardConstraints] +[RoomHardConstraints] +[InstitutionalWeightings] +TWOINAROW, 1 +""" + + +def check() -> dict: + instance = parse_itc2007_exam(FIXTURE) + core = instance.conflict_core(((0, 1), (0, 1), (0, 1)), + acknowledge_ignored_constraints=True) + model: ExamRepairModel = core.model + sat_query = model.freeze_event(fixed=(("exam-0000", model.period_ids[0]),)) + unsat_query = model.freeze_event(fixed=( + ("exam-0000", model.period_ids[0]), + ("exam-0001", model.period_ids[0]), + )) + with tempfile.TemporaryDirectory(prefix="spectra-exam-install-") as directory: + library = build_exact_runtime(Path(directory) / "native") + runtime = ExactRuntime(library) + with runtime.prepare(model.problem, mode="scc") as session: + sat = session.solve(sat_query) + unsat = session.solve(unsat_query) + if sat.status != "SAT_VERIFIED" or unsat.status != "UNSAT_VERIFIED": + raise AssertionError("installed exact runtime returned unexpected status") + if not verify_answer(model.problem, sat_query, sat.status, sat.labels, sat.proof): + raise AssertionError("installed SAT result failed replay") + if not verify_answer( + model.problem, unsat_query, unsat.status, unsat.labels, unsat.proof): + raise AssertionError("installed UNSAT result failed replay") + assignment = model.assignment_from_labels(sat.labels, sat_query) + explanation = model.explain_unsat(unsat_query, unsat.proof) + info = session.info + if tuple(exam for exam, _period in assignment) != model.exam_ids: + raise AssertionError("installed repair omitted or reordered exams") + if not model.check_assignment(assignment, sat_query): + raise AssertionError("installed named assignment failed adapter replay") + if explanation.get("kind") not in ("EMPTY_DOMAIN", "FORCED_OPPOSITES"): + raise AssertionError("installed repair returned an unknown proof explanation") + return { + "schema": "spectra.exam_repair.installation_check.v1", + "exams": model.problem.n, + "periods": model.problem.palette, + "conflicts": len(model.problem.edges), + "sat_status": sat.status, + "unsat_status": unsat.status, + "proof_kind": explanation["kind"], + "assignment_complete": True, + "native_abi": info["native_abi"], + "exact_api_version": info["exact_api_version"], + } + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--out", type=Path) + args = parser.parse_args() + result = check() + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.out is not None: + args.out.parent.mkdir(parents=True, exist_ok=True) + args.out.write_text(payload, encoding="utf-8") + print(payload, end="") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/spectra/_native/exact_binary.cpp b/spectra/_native/exact_binary.cpp index 96182ee..96694d3 100644 --- a/spectra/_native/exact_binary.cpp +++ b/spectra/_native/exact_binary.cpp @@ -341,12 +341,13 @@ struct ObserverSessionPacket { struct Answer {bool sat=true;std::vector labels,certificate;W visits=0,arcs=0;}; struct Index { U n,k,nc=0,bad=NIL;bool condensed,sparse,routed;W cap;W full_arcs=0; + const char* auto_reason="explicit_mode"; std::vector masks; std::vector lo,hi,base; std::vector comp,opposite; std::vector inward,outward,representative,cross_from,cross_to; CSR original,dag; - Index(Input p,U mode,U bank_size=0):n(p.n),k(p.k),condensed(mode!=0),sparse(mode==2),routed(mode==3),cap(p.cap),masks(std::move(p.masks)),lo(n),hi(n,255),base(n) { + Index(Input p,U mode,U bank_size=0,U bank_pins=0):n(p.n),k(p.k),condensed(mode!=0),sparse(mode==2),routed(mode==3),cap(p.cap),masks(std::move(p.masks)),lo(n),hi(n,255),base(n) { std::vector> arcs;arcs.reserve(4*p.edges.size()+n); for(U v=0;v(comp[2*v]=64 && bad==NIL; - routed=condensed && nc<=n; + // Structural auto policy v2. set9 development evidence showed that + // large, heavily pinned repair banks can lose to raw traversal even + // when tile64 is available. The policy therefore uses only immutable + // request geometry (never answers or measured timings): raw below one + // tile, on a base contradiction, or at eight pins per row and above. + // The threshold is frozen before the set10/set12 holdout transfer. + if(bank_size<64) { + condensed=false;routed=false;auto_reason="bank_below_tile64"; + } else if(bad!=NIL) { + condensed=false;routed=false;auto_reason="base_infeasible"; + } else if(W(bank_pins)>=8*W(bank_size)) { + condensed=false;routed=false;auto_reason="high_pin_density"; + } else { + condensed=true;routed=nc<=n; + auto_reason=routed?"route_component_compression":"scc_tile64"; + } } if(condensed && bad==NIL) { opposite.assign(nc,NIL); @@ -990,6 +1002,7 @@ PyObject* solve_session_packet(PyObject*,PyObject* args) { const auto* data=reinterpret_cast(PyBytes_AS_STRING(packet)); size_t size=static_cast(PyBytes_GET_SIZE(packet)); std::unique_ptr solver;std::unique_ptr observer;BankResult result; + U bank_queries=0,bank_pins=0; { Released guard; ObserverSessionPacket observer_rows(data,size,limit); @@ -997,8 +1010,9 @@ PyObject* solve_session_packet(PyObject*,PyObject* args) { W observer_bytes=observer->bytes(); if(observer_bytes>=limit) throw Resource("SBC1 observer consumes session cap"); SolverSessionPacket solver_rows(data,size,limit-observer_bytes); + bank_queries=solver_rows.query_count();bank_pins=solver_rows.pin_count(); solver=std::make_unique(solver_rows.take_input(limit-observer_bytes), - static_cast(which),solver_rows.query_count()); + static_cast(which),bank_queries,bank_pins); result=run_rows(*solver,*observer,solver_rows,observer_rows,size,limit,"SBC1"); } PyObject* output=PyBytes_FromStringAndSize(reinterpret_cast(result.output.data()), @@ -1018,11 +1032,22 @@ PyObject* solve_session_packet(PyObject*,PyObject* args) { if(!metadata){Py_DECREF(output);return nullptr;} PyObject* kernel=PyUnicode_FromString(result.tiled?"tile64":"serial"); PyObject* tiles=PyLong_FromUnsignedLong(result.tiles); - if(!kernel || !tiles || PyDict_SetItemString(metadata,"bank_kernel",kernel)<0 - || PyDict_SetItemString(metadata,"bank_tiles",tiles)<0) { - Py_XDECREF(kernel);Py_XDECREF(tiles);Py_DECREF(output);Py_DECREF(metadata);return nullptr; + PyObject* queries=PyLong_FromUnsignedLong(bank_queries); + PyObject* pins=PyLong_FromUnsignedLong(bank_pins); + PyObject* policy=PyUnicode_FromString(which==4?"structural-v2":"explicit"); + PyObject* reason=PyUnicode_FromString(solver->auto_reason); + if(!kernel || !tiles || !queries || !pins || !policy || !reason + || PyDict_SetItemString(metadata,"bank_kernel",kernel)<0 + || PyDict_SetItemString(metadata,"bank_tiles",tiles)<0 + || PyDict_SetItemString(metadata,"bank_query_count",queries)<0 + || PyDict_SetItemString(metadata,"bank_pin_count",pins)<0 + || PyDict_SetItemString(metadata,"auto_policy",policy)<0 + || PyDict_SetItemString(metadata,"auto_policy_reason",reason)<0) { + Py_XDECREF(kernel);Py_XDECREF(tiles);Py_XDECREF(queries);Py_XDECREF(pins); + Py_XDECREF(policy);Py_XDECREF(reason);Py_DECREF(output);Py_DECREF(metadata);return nullptr; } - Py_DECREF(kernel);Py_DECREF(tiles); + Py_DECREF(kernel);Py_DECREF(tiles);Py_DECREF(queries);Py_DECREF(pins); + Py_DECREF(policy);Py_DECREF(reason); return Py_BuildValue("NKKKKKKN",output, static_cast(result.sat+result.unsat), static_cast(result.sat), diff --git a/spectra/exact.py b/spectra/exact.py index 983d335..60ed10e 100644 --- a/spectra/exact.py +++ b/spectra/exact.py @@ -402,11 +402,13 @@ def solve_session_packet(self, packet: bytes, *, mode: str = 'route', max_bytes: int = DEFAULT_BYTES) -> ExactSessionPacketAnswer: """Construct, solve, verify, serialize and dispose one prepared SBC1 session. - Opt-in ``auto`` uses raw traversal below 64 requests or on a base-infeasible - graph. Otherwise it uses routed proofs when SCCs at least halve the - literal graph, and plain SCC batching when they do not. Selection uses - fixed-graph structure and bank length, never measured answers or timings. - ``info['selected_mode']`` names the actual engine. Explicit modes and the + Opt-in ``auto`` uses structural policy v2. It selects raw traversal below + 64 requests, on a base-infeasible graph, or when the immutable bank carries + at least eight pins per request on average. Otherwise it uses routed proofs + when SCCs at least halve the literal graph, and plain SCC batching when they + do not. Selection uses only admitted graph/request geometry, never answers + or measured timings. ``info['selected_mode']`` and + ``info['auto_policy_reason']`` expose the decision. Explicit modes and the default retain their meaning; this policy is an experimental heuristic. """ if type(packet) is not bytes: diff --git a/spectra/exam_repair.py b/spectra/exam_repair.py new file mode 100644 index 0000000..121ae9e --- /dev/null +++ b/spectra/exam_repair.py @@ -0,0 +1,418 @@ +"""Proof-carrying bounded exam rescheduling on top of :mod:`spectra.exact`. + +This adapter models a deliberately narrow operational problem: every exam has one +or two pre-approved candidate periods, and exams that share a student (or an +explicit exclusion) may not use the same period. Period closures and exam pins +become current-query restrictions. The exact backend can then return either a +complete checked repair or a portable contradiction proof. + +Room capacities, room exclusivity, precedence, coincidence, soft penalties and +candidate generation are outside this model. They must be handled before +admission or checked separately; the module never silently drops them. +""" +from __future__ import annotations + +from dataclasses import dataclass +from typing import Iterable, Mapping, Sequence + +from .exact_problem import ExactProblem +from .exact_proof import decode_proof, verify_answer + +MAX_IDENTIFIER_CHARS = 512 +MAX_ENROLLMENTS = 4_000_000 +MAX_CONFLICTS = 2_000_000 +MAX_PAIR_EMISSIONS = 8_000_000 + + +@dataclass(frozen=True, slots=True) +class ExamConflictReason: + """One deterministic witness for an admitted conflict edge.""" + + kind: str + student: int | None = None + + def __post_init__(self) -> None: + if self.kind not in ("shared_student", "explicit_exclusion"): + raise ValueError("unsupported exam conflict reason") + if self.kind == "shared_student": + if type(self.student) is not int or not 0 <= self.student < 1 << 63: + raise ValueError("shared-student reason needs a bounded student id") + elif self.student is not None: + raise ValueError("explicit exclusion must not carry a student id") + + +@dataclass(frozen=True, slots=True) +class ExamRepairModel: + """A checked reduction from bounded exam repair to exact list colouring. + + ``problem`` uses exam positions as vertices and period positions as colours. + ``conflict_reasons`` is aligned with ``problem.edges`` and is explanatory + metadata only; the exact solver and verifier receive the original graph. + """ + + problem: ExactProblem + exam_ids: tuple[str, ...] + period_ids: tuple[str, ...] + students: tuple[tuple[int, ...], ...] + conflict_reasons: tuple[ExamConflictReason, ...] + + @classmethod + def create( + cls, + period_ids: Iterable[str], + exam_ids: Iterable[str], + students: Iterable[Iterable[int]], + candidate_periods: Iterable[Iterable[str]], + *, + exclusions: Iterable[Sequence[str]] = (), + ) -> "ExamRepairModel": + periods = cls._bounded_snapshot(period_ids, 64, "period identifier") + exams = cls._bounded_snapshot(exam_ids, 100_000, "exam identifier") + student_rows: list[tuple[int, ...]] = [] + try: + for row in students: + if len(student_rows) >= len(exams): + raise ValueError("exam, student and candidate row counts differ") + if isinstance(row, (str, bytes)): + raise ValueError("student rows must be integer iterables, not strings") + student_rows.append(tuple(row)) + except TypeError as error: + raise ValueError("student rows must be iterable") from error + candidate_rows: list[tuple[str, ...]] = [] + try: + iterator = iter(candidate_periods) + except TypeError as error: + raise ValueError("candidate rows must be iterable") from error + for row in iterator: + if len(candidate_rows) >= len(exams): + raise ValueError("exam, student and candidate row counts differ") + if isinstance(row, (str, bytes)): + raise ValueError("candidate rows must be period iterables, not strings") + try: + candidate_rows.append(tuple(row)) + except TypeError as error: + raise ValueError("candidate rows must be iterable") from error + if not 1 <= len(periods) <= 64: + raise ValueError("period count must be in [1, 64]") + if len(student_rows) != len(exams) or len(candidate_rows) != len(exams): + raise ValueError("exam, student and candidate row counts differ") + candidates = tuple(candidate_rows) + cls._check_identifiers(periods, "period") + cls._check_identifiers(exams, "exam") + if len(set(periods)) != len(periods): + raise ValueError("period identifiers must be unique") + if len(set(exams)) != len(exams): + raise ValueError("exam identifiers must be unique") + + period_at = {name: index for index, name in enumerate(periods)} + masks: list[int] = [] + for row in candidates: + if not 1 <= len(row) <= 2 or any(type(value) is not str for value in row): + raise ValueError("each exam needs one or two exact period identifiers") + if len(set(row)) != len(row): + raise ValueError("candidate periods must be unique within an exam") + try: + indices = tuple(period_at[value] for value in row) + except KeyError as error: + raise ValueError("candidate names an unknown period") from error + masks.append(sum(1 << index for index in indices)) + + normalized_students: list[tuple[int, ...]] = [] + enrollment_total = 0 + roster: dict[int, list[int]] = {} + for vertex, row in enumerate(student_rows): + if any(type(value) is not int or not 0 <= value < 1 << 63 for value in row): + raise ValueError("student identifiers must be bounded nonnegative integers") + normalized = tuple(sorted(set(row))) + enrollment_total += len(normalized) + if enrollment_total > MAX_ENROLLMENTS: + raise ValueError("enrollment count exceeds adapter bound") + normalized_students.append(normalized) + for student in normalized: + roster.setdefault(student, []).append(vertex) + + reasons: dict[tuple[int, int], ExamConflictReason] = {} + pair_emissions = 0 + for student in sorted(roster): + vertices = roster[student] + # A single very large cohort can otherwise spend unbounded time before + # the native edge limit is reached. This is a conservative admission + # check; duplicate pairs from other students do not earn extra budget. + pairs = len(vertices) * (len(vertices) - 1) // 2 + pair_emissions += pairs + if pairs > MAX_CONFLICTS or pair_emissions > MAX_PAIR_EMISSIONS: + raise ValueError("student cohorts exceed bounded conflict-generation work") + for offset, left in enumerate(vertices): + for right in vertices[offset + 1:]: + edge = (left, right) + reasons.setdefault(edge, ExamConflictReason("shared_student", student)) + if len(reasons) > MAX_CONFLICTS: + raise ValueError("conflict edge count exceeds native bound") + + exam_at = {name: index for index, name in enumerate(exams)} + for item in exclusions: + if isinstance(item, (str, bytes)): + raise ValueError("exclusion must contain two exact exam identifiers") + row = tuple(item) + if len(row) != 2 or any(type(value) is not str for value in row): + raise ValueError("exclusion must contain two exact exam identifiers") + try: + left, right = exam_at[row[0]], exam_at[row[1]] + except KeyError as error: + raise ValueError("exclusion names an unknown exam") from error + if left == right: + raise ValueError("an exam cannot exclude itself") + edge = (min(left, right), max(left, right)) + reasons.setdefault(edge, ExamConflictReason("explicit_exclusion")) + if len(reasons) > MAX_CONFLICTS: + raise ValueError("conflict edge count exceeds native bound") + + edges = tuple(sorted(reasons)) + problem = ExactProblem.create(len(exams), len(periods), edges, masks) + return cls( + problem=problem, + exam_ids=exams, + period_ids=periods, + students=tuple(normalized_students), + conflict_reasons=tuple(reasons[edge] for edge in problem.edges), + ) + + @staticmethod + def _bounded_snapshot(values: Iterable[str], limit: int, name: str) -> tuple[str, ...]: + try: + iterator = iter(values) + except TypeError as error: + raise ValueError(f"{name}s must be iterable") from error + copied: list[str] = [] + for value in iterator: + if len(copied) >= limit: + raise ValueError(f"{name} count exceeds adapter bound") + copied.append(value) + return tuple(copied) + + @staticmethod + def _check_identifiers(values: tuple[str, ...], kind: str) -> None: + for value in values: + if type(value) is not str or not value or len(value) > MAX_IDENTIFIER_CHARS: + raise ValueError( + f"{kind} identifiers must be nonempty exact strings of at most " + f"{MAX_IDENTIFIER_CHARS} characters" + ) + + @property + def candidates(self) -> tuple[tuple[str, ...], ...]: + """Return each exam's admitted candidate periods in colour order.""" + return tuple( + tuple(self.period_ids[index] for index in range(len(self.period_ids)) if mask >> index & 1) + for mask in self.problem.masks + ) + + @property + def info(self) -> dict: + shared = sum(reason.kind == "shared_student" for reason in self.conflict_reasons) + return { + "schema": "spectra.exam_repair.model.v1", + "exams": self.problem.n, + "periods": self.problem.palette, + "conflicts": len(self.problem.edges), + "shared_student_conflicts": shared, + "explicit_exclusions": len(self.problem.edges) - shared, + "enrollments": sum(map(len, self.students)), + "scope": "one/two pre-approved periods; shared students and explicit exclusions only", + } + + def freeze_event( + self, + *, + closed_periods: Iterable[str] = (), + fixed: Iterable[Sequence[str]] = (), + allowed: Iterable[Sequence[object]] = (), + ) -> tuple[tuple[int, int], ...]: + """Translate current closures/pins into one canonical exact query. + + ``fixed`` rows are ``(exam_id, period_id)``. ``allowed`` rows are + ``(exam_id, iterable_of_period_ids)``. Multiple sources of restriction + are intersected. A zero resulting mask is retained so the exact service + can return a portable empty-domain proof instead of raising. + """ + period_at = {name: index for index, name in enumerate(self.period_ids)} + exam_at = {name: index for index, name in enumerate(self.exam_ids)} + closed = tuple(closed_periods) + if any(type(name) is not str for name in closed) or len(set(closed)) != len(closed): + raise ValueError("closed periods must be unique exact strings") + try: + closed_mask = sum(1 << period_at[name] for name in closed) + except KeyError as error: + raise ValueError("closed-period event names an unknown period") from error + + effective = [mask & ~closed_mask for mask in self.problem.masks] + fixed_seen: set[int] = set() + for item in fixed: + if isinstance(item, (str, bytes)): + raise ValueError("fixed rows must be exact exam/period string pairs") + row = tuple(item) + if len(row) != 2 or any(type(value) is not str for value in row): + raise ValueError("fixed rows must be exact exam/period string pairs") + try: + vertex, period = exam_at[row[0]], period_at[row[1]] + except KeyError as error: + raise ValueError("fixed row names an unknown exam or period") from error + if vertex in fixed_seen: + raise ValueError("an exam appears more than once in fixed rows") + fixed_seen.add(vertex) + effective[vertex] &= 1 << period + + allowed_seen: set[int] = set() + for item in allowed: + if isinstance(item, (str, bytes)): + raise ValueError("allowed rows must contain an exam and a period iterable") + row = tuple(item) + if len(row) != 2 or type(row[0]) is not str or isinstance(row[1], (str, bytes)): + raise ValueError("allowed rows must contain an exam and a period iterable") + try: + vertex = exam_at[row[0]] + except KeyError as error: + raise ValueError("allowed row names an unknown exam") from error + if vertex in allowed_seen: + raise ValueError("an exam appears more than once in allowed rows") + allowed_seen.add(vertex) + try: + choices = tuple(row[1]) + except TypeError as error: + raise ValueError( + "allowed rows must contain an exam and a period iterable" + ) from error + if any(type(name) is not str for name in choices) or len(set(choices)) != len(choices): + raise ValueError("allowed period identifiers must be unique exact strings") + try: + mask = sum(1 << period_at[name] for name in choices) + except KeyError as error: + raise ValueError("allowed row names an unknown period") from error + effective[vertex] &= mask + + return tuple( + (vertex, mask) + for vertex, (original, mask) in enumerate(zip(self.problem.masks, effective)) + if mask != original + ) + + def assignment_from_labels( + self, + labels: bytes, + query: Iterable[Sequence[int]] = (), + ) -> tuple[tuple[str, str], ...]: + """Decode a complete checked label vector into stable exam/period rows.""" + frozen = self.problem.freeze_query(query) + if not self.problem.check(labels, frozen): + raise ValueError("labels do not satisfy the admitted repair problem and event") + return tuple((exam, self.period_ids[labels[index]]) + for index, exam in enumerate(self.exam_ids)) + + def check_assignment( + self, + assignment: Mapping[str, str] | Iterable[Sequence[str]], + query: Iterable[Sequence[int]] = (), + ) -> bool: + """Check a named assignment against original adapter inputs only.""" + try: + rows = tuple(assignment.items()) if isinstance(assignment, Mapping) else tuple( + tuple(row) for row in assignment + ) + exam_at = {name: index for index, name in enumerate(self.exam_ids)} + period_at = {name: index for index, name in enumerate(self.period_ids)} + labels = [-1] * self.problem.n + for row in rows: + if len(row) != 2 or any(type(value) is not str for value in row): + return False + vertex = exam_at[row[0]] + if labels[vertex] != -1: + return False + labels[vertex] = period_at[row[1]] + if any(value < 0 for value in labels): + return False + return self.problem.check(bytes(labels), query) + except (KeyError, TypeError, ValueError, OverflowError): + return False + + def explain_unsat( + self, + query: Iterable[Sequence[int]], + certificate: bytes, + ) -> dict: + """Verify and translate an SBP1 contradiction into named repair steps.""" + frozen = self.problem.freeze_query(query) + if not verify_answer(self.problem, frozen, "UNSAT_VERIFIED", b"", certificate): + raise ValueError("certificate does not prove this repair event infeasible") + kind, left, right = decode_proof(certificate, self.problem.n) + effective = list(self.problem.masks) + for vertex, mask in frozen: + effective[vertex] &= mask + if kind == 1: + vertex = left[0] + return { + "schema": "spectra.exam_repair.proof.v1", + "kind": "EMPTY_DOMAIN", + "exam": self.exam_ids[vertex], + "original_candidates": list(self.candidates[vertex]), + "remaining_candidates": [], + } + return { + "schema": "spectra.exam_repair.proof.v1", + "kind": "FORCED_OPPOSITES" if kind == 2 else "BASE_CONTRADICTION", + "left": self._explain_path(left, effective), + "right": self._explain_path(right, effective), + } + + def _literal(self, literal: int) -> dict: + vertex, side = divmod(literal, 2) + colors = tuple(index for index in range(self.problem.palette) + if self.problem.masks[vertex] >> index & 1) + period = self.period_ids[colors[side]] if side < len(colors) else None + return { + "literal": literal, + "exam": self.exam_ids[vertex], + "exam_index": vertex, + "period": period, + "side": side, + } + + def _explain_path(self, path: tuple[int, ...], effective: list[int]) -> dict: + reasons = {edge: reason for edge, reason in zip( + self.problem.edges, self.conflict_reasons + )} + nodes = [self._literal(literal) for literal in path] + steps = [] + for before, after in zip(path, path[1:]): + left, right = before // 2, after // 2 + if left == right: + steps.append({ + "kind": "SINGLETON_DOMAIN", + "exam": self.exam_ids[left], + "therefore_period": self._literal(after)["period"], + }) + continue + edge = (min(left, right), max(left, right)) + reason = reasons[edge] + before_node = self._literal(before) + after_node = self._literal(after) + step = { + "kind": "SHARED_STUDENT_CONFLICT" if reason.kind == "shared_student" + else "EXPLICIT_EXCLUSION", + "from_exam": before_node["exam"], + "from_period": before_node["period"], + "to_exam": after_node["exam"], + "therefore_period": after_node["period"], + } + if reason.student is not None: + step["student"] = reason.student + steps.append(step) + root = nodes[0] + root_mask = effective[root["exam_index"]] + root["forced_by_event"] = ( + root["period"] is not None + and root_mask == 1 << self.period_ids.index(root["period"]) + ) + return {"nodes": nodes, "steps": steps} + + +__all__ = ["ExamConflictReason", "ExamRepairModel"] diff --git a/spectra/itc2007_exam.py b/spectra/itc2007_exam.py new file mode 100644 index 0000000..b0f9c52 --- /dev/null +++ b/spectra/itc2007_exam.py @@ -0,0 +1,316 @@ +"""Strict ITC 2007 examination-timetabling reader and bounded-repair adapter. + +The reader preserves the complete hard/soft section inventory. Conversion to +:class:`spectra.exam_repair.ExamRepairModel` is intentionally explicit about the +smaller problem being solved: shared-student and EXCLUSION conflicts over one or +two pre-approved periods per exam. AFTER, EXAM_COINCIDENCE, room assignment, +room exclusivity, and soft objectives are never silently interpreted as solved. +""" +from __future__ import annotations + +from dataclasses import dataclass +import hashlib +import re +from typing import Iterable + +from .exam_repair import ExamRepairModel + +_HEADER = re.compile(r"^\[([A-Za-z]+)(?::([0-9]+))?\]$") +_REQUIRED = ( + "Exams", "Periods", "Rooms", "PeriodHardConstraints", + "RoomHardConstraints", "InstitutionalWeightings", +) + + +@dataclass(frozen=True, slots=True) +class ITCExam: + duration: int + students: tuple[int, ...] + + +@dataclass(frozen=True, slots=True) +class ITCPeriod: + date: str + time: str + duration: int + penalty: int + + @property + def identifier(self) -> str: + return f"{self.date} {self.time}" + + +@dataclass(frozen=True, slots=True) +class ITCRoom: + capacity: int + penalty: int + + +@dataclass(frozen=True, slots=True) +class ITCConflictCore: + """One exact conflict-core model plus an immutable omitted-constraint receipt.""" + + model: ExamRepairModel + source_sha256: str + ignored_constraints: tuple[tuple[str, int], ...] + + @property + def info(self) -> dict: + return { + **self.model.info, + "schema": "spectra.itc2007.conflict_core.v1", + "source_sha256": self.source_sha256, + "ignored_constraints": dict(self.ignored_constraints), + "claim_boundary": ( + "bounded candidate-period repair only; not a complete ITC 2007 " + "timetable, room assignment, precedence solution or soft-score result" + ), + } + + +@dataclass(frozen=True, slots=True) +class ITCExamInstance: + exams: tuple[ITCExam, ...] + periods: tuple[ITCPeriod, ...] + rooms: tuple[ITCRoom, ...] + after: tuple[tuple[int, int], ...] + exclusions: tuple[tuple[int, int], ...] + coincidences: tuple[tuple[int, int], ...] + room_exclusive: tuple[int, ...] + institutional_weightings: tuple[tuple[str, ...], ...] + source_sha256: str + + @property + def ignored_constraint_counts(self) -> tuple[tuple[str, int], ...]: + values = ( + ("after", len(self.after)), + ("exam_coincidence", len(self.coincidences)), + ("room_exclusive", len(self.room_exclusive)), + ("room_assignment", len(self.rooms)), + ("period_penalties", sum(period.penalty != 0 for period in self.periods)), + ("room_penalties", sum(room.penalty != 0 for room in self.rooms)), + ("institutional_weightings", len(self.institutional_weightings)), + ) + return tuple((name, count) for name, count in values if count) + + def conflict_core( + self, + candidate_periods: Iterable[Iterable[int]], + *, + acknowledge_ignored_constraints: bool = False, + ) -> ITCConflictCore: + """Build the exact shared-student/EXCLUSION repair core. + + Candidate rows contain one or two period indices and are assumed to have + been pre-approved by the operator. Period duration is still checked here. + Any unmodelled ITC section requires an explicit acknowledgement flag and + remains listed in the returned receipt. + """ + ignored = self.ignored_constraint_counts + if ignored and not acknowledge_ignored_constraints: + names = ", ".join(name for name, _ in ignored) + raise ValueError("ITC conflict-core conversion would ignore: " + names) + copied_rows: list[tuple[int, ...]] = [] + try: + for row in candidate_periods: + if len(copied_rows) >= len(self.exams): + raise ValueError("candidate row count differs from exam count") + if isinstance(row, (str, bytes)): + raise ValueError("candidate rows must be period-index iterables") + copied_rows.append(tuple(row)) + except TypeError as error: + raise ValueError("candidate rows must be period-index iterables") from error + rows = tuple(copied_rows) + if len(rows) != len(self.exams): + raise ValueError("candidate row count differs from exam count") + names = tuple( + f"{index:02d}:{period.identifier}" + for index, period in enumerate(self.periods) + ) + candidates: list[tuple[str, ...]] = [] + for exam_index, (exam, row) in enumerate(zip(self.exams, rows)): + if not 1 <= len(row) <= 2 or any(type(value) is not int for value in row): + raise ValueError("every exam needs one or two exact period indices") + if len(set(row)) != len(row) or any(not 0 <= value < len(self.periods) for value in row): + raise ValueError("candidate period indices must be unique and in range") + if any(self.periods[value].duration < exam.duration for value in row): + raise ValueError(f"exam {exam_index} does not fit a candidate period") + candidates.append(tuple(names[value] for value in row)) + exam_ids = tuple(f"exam-{index:04d}" for index in range(len(self.exams))) + exclusions = tuple((exam_ids[left], exam_ids[right]) + for left, right in self.exclusions) + model = ExamRepairModel.create( + names, + exam_ids, + (exam.students for exam in self.exams), + candidates, + exclusions=exclusions, + ) + return ITCConflictCore(model, self.source_sha256, ignored) + + +def parse_itc2007_exam(text: str, *, max_chars: int = 64 << 20) -> ITCExamInstance: + """Parse one canonical ITC 2007 examination instance without dependencies.""" + if type(text) is not str: + raise ValueError("ITC input must be an exact string") + if type(max_chars) is not int or not 1 <= max_chars <= 1 << 30: + raise ValueError("max_chars must be a bounded positive exact integer") + if len(text) > max_chars: + raise ValueError("ITC input exceeds max_chars") + normalized = text.removeprefix("\ufeff").replace("\r\n", "\n").replace("\r", "\n") + sections: dict[str, tuple[int | None, list[tuple[int, str]]]] = {} + current: str | None = None + for line_number, raw in enumerate(normalized.split("\n"), 1): + line = raw.strip() + if not line: + continue + match = _HEADER.fullmatch(line) + if match: + name, count_text = match.groups() + if name not in _REQUIRED: + raise ValueError(f"line {line_number}: unknown ITC section {name}") + if name in sections: + raise ValueError(f"line {line_number}: duplicate ITC section {name}") + expected = int(count_text) if count_text is not None else None + if name in ("Exams", "Periods", "Rooms") and expected is None: + raise ValueError(f"line {line_number}: {name} requires a count") + if name not in ("Exams", "Periods", "Rooms") and expected is not None: + raise ValueError(f"line {line_number}: {name} must not carry a count") + sections[name] = (expected, []) + current = name + continue + if current is None: + raise ValueError(f"line {line_number}: data appears before a section header") + sections[current][1].append((line_number, line)) + if tuple(sections) != _REQUIRED: + raise ValueError("ITC sections are missing, duplicated or out of canonical order") + for name in ("Exams", "Periods", "Rooms"): + expected, rows = sections[name] + if expected != len(rows): + raise ValueError(f"{name} row count differs: expected {expected}, found {len(rows)}") + + exams: list[ITCExam] = [] + for line_number, line in sections["Exams"][1]: + fields = _fields(line, line_number) + if len(fields) < 1: + raise ValueError(f"line {line_number}: empty exam row") + duration = _nonnegative(fields[0], line_number, "exam duration", positive=True) + student_values = tuple(_nonnegative(value, line_number, "student id") + for value in fields[1:]) + if len(set(student_values)) != len(student_values): + raise ValueError(f"line {line_number}: duplicate student within an exam") + exams.append(ITCExam(duration, tuple(sorted(student_values)))) + + periods: list[ITCPeriod] = [] + for line_number, line in sections["Periods"][1]: + fields = _fields(line, line_number) + if len(fields) != 4 or not fields[0] or not fields[1]: + raise ValueError(f"line {line_number}: period row must have date,time,duration,penalty") + periods.append(ITCPeriod( + fields[0], fields[1], + _nonnegative(fields[2], line_number, "period duration", positive=True), + _nonnegative(fields[3], line_number, "period penalty"), + )) + identifiers = tuple(period.identifier for period in periods) + if len(set(identifiers)) != len(identifiers): + raise ValueError("period date/time identifiers must be unique") + + rooms: list[ITCRoom] = [] + for line_number, line in sections["Rooms"][1]: + fields = _fields(line, line_number) + if len(fields) != 2: + raise ValueError(f"line {line_number}: room row must have capacity,penalty") + rooms.append(ITCRoom( + _nonnegative(fields[0], line_number, "room capacity"), + _nonnegative(fields[1], line_number, "room penalty"), + )) + + after: list[tuple[int, int]] = [] + exclusions: list[tuple[int, int]] = [] + coincidences: list[tuple[int, int]] = [] + seen_hard: set[tuple[int, str, int]] = set() + for line_number, line in sections["PeriodHardConstraints"][1]: + fields = _fields(line, line_number) + if len(fields) != 3: + raise ValueError(f"line {line_number}: period hard constraint must have three fields") + left = _exam_index(fields[0], line_number, len(exams)) + right = _exam_index(fields[2], line_number, len(exams)) + relation = fields[1] + if relation not in ("AFTER", "EXCLUSION", "EXAM_COINCIDENCE"): + raise ValueError(f"line {line_number}: unsupported period relation {relation}") + if left == right: + raise ValueError(f"line {line_number}: hard constraint repeats one exam") + key = ((min(left, right), relation, max(left, right)) + if relation in ("EXCLUSION", "EXAM_COINCIDENCE") + else (left, relation, right)) + if key in seen_hard: + raise ValueError(f"line {line_number}: duplicate period hard constraint") + seen_hard.add(key) + if relation == "AFTER": + after.append((left, right)) + elif relation == "EXCLUSION": + exclusions.append((min(left, right), max(left, right))) + else: + coincidences.append((min(left, right), max(left, right))) + + room_exclusive: list[int] = [] + for line_number, line in sections["RoomHardConstraints"][1]: + fields = _fields(line, line_number) + if len(fields) != 2 or fields[1] != "ROOM_EXCLUSIVE": + raise ValueError(f"line {line_number}: invalid room hard constraint") + exam = _exam_index(fields[0], line_number, len(exams)) + if exam in room_exclusive: + raise ValueError(f"line {line_number}: duplicate room-exclusive exam") + room_exclusive.append(exam) + + weightings: list[tuple[str, ...]] = [] + for line_number, line in sections["InstitutionalWeightings"][1]: + fields = _fields(line, line_number) + if not fields[0] or any(not value for value in fields): + raise ValueError(f"line {line_number}: empty institutional weighting field") + # The exact weighting vocabulary is not interpreted by the conflict-core + # adapter, but every numeric payload must still be canonical and bounded. + for value in fields[1:]: + _nonnegative(value, line_number, "institutional weighting") + weightings.append(fields) + + return ITCExamInstance( + exams=tuple(exams), + periods=tuple(periods), + rooms=tuple(rooms), + after=tuple(after), + exclusions=tuple(sorted(set(exclusions))), + coincidences=tuple(sorted(set(coincidences))), + room_exclusive=tuple(room_exclusive), + institutional_weightings=tuple(weightings), + source_sha256=hashlib.sha256(normalized.encode("utf-8")).hexdigest(), + ) + + +def _fields(line: str, line_number: int) -> tuple[str, ...]: + values = tuple(value.strip() for value in line.split(",")) + if any(not value for value in values): + raise ValueError(f"line {line_number}: empty comma-separated field") + return values + + +def _nonnegative(value: str, line_number: int, name: str, *, positive: bool = False) -> int: + if not value.isascii() or not value.isdigit(): + raise ValueError(f"line {line_number}: {name} must be a canonical nonnegative integer") + number = int(value) + if number >= 1 << 63 or (positive and number == 0): + raise ValueError(f"line {line_number}: {name} is outside the supported bound") + return number + + +def _exam_index(value: str, line_number: int, count: int) -> int: + index = _nonnegative(value, line_number, "exam index") + if index >= count: + raise ValueError(f"line {line_number}: exam index outside declared exam bank") + return index + + +__all__ = [ + "ITCExam", "ITCPeriod", "ITCRoom", "ITCExamInstance", "ITCConflictCore", + "parse_itc2007_exam", +] diff --git a/tests/public/test_exam_repair.py b/tests/public/test_exam_repair.py new file mode 100644 index 0000000..c50f125 --- /dev/null +++ b/tests/public/test_exam_repair.py @@ -0,0 +1,146 @@ +"""Public bounded exam-repair adapter contracts.""" +from __future__ import annotations + +import shutil +import struct +import sys + +import pytest + +from spectra.exam_repair import ExamRepairModel +from spectra.exact import ExactRuntime, build_exact_runtime + + +def path_model() -> ExamRepairModel: + return ExamRepairModel.create( + period_ids=("P0", "P1"), + exam_ids=("A", "B", "C"), + students=((1,), (1, 2), (2,)), + candidate_periods=(("P0", "P1"),) * 3, + ) + + +def test_adapter_builds_deterministic_conflicts_and_named_metadata(): + model = ExamRepairModel.create( + period_ids=("AM", "PM", "EVENING"), + exam_ids=("MATH", "CHEM", "HIST"), + students=((4, 2, 4), (2,), (9,)), + candidate_periods=(("AM", "PM"), ("PM",), ("AM", "EVENING")), + exclusions=(("CHEM", "HIST"),), + ) + assert model.problem.edges == ((0, 1), (1, 2)) + assert tuple(reason.kind for reason in model.conflict_reasons) == ( + "shared_student", "explicit_exclusion" + ) + assert model.conflict_reasons[0].student == 2 + assert model.candidates == (("AM", "PM"), ("PM",), ("AM", "EVENING")) + assert model.info == { + "schema": "spectra.exam_repair.model.v1", + "exams": 3, + "periods": 3, + "conflicts": 2, + "shared_student_conflicts": 1, + "explicit_exclusions": 1, + "enrollments": 4, + "scope": "one/two pre-approved periods; shared students and explicit exclusions only", + } + + +def test_event_intersects_closures_pins_and_allowed_periods(): + model = path_model() + query = model.freeze_event( + closed_periods=("P1",), + fixed=(("B", "P1"),), + allowed=(("C", ("P0",)),), + ) + assert query == ((0, 0b01), (1, 0), (2, 0b01)) + with pytest.raises(ValueError, match="unknown period"): + model.freeze_event(closed_periods=("P2",)) + with pytest.raises(ValueError, match="more than once"): + model.freeze_event(fixed=(("A", "P0"), ("A", "P1"))) + with pytest.raises(ValueError, match="period iterable"): + model.freeze_event(allowed=(("A", 7),)) + + +def test_named_assignment_is_checked_against_event_and_conflicts(): + model = path_model() + query = model.freeze_event(fixed=(("A", "P0"), ("C", "P0"))) + labels = b"\x00\x01\x00" + assert model.assignment_from_labels(labels, query) == ( + ("A", "P0"), ("B", "P1"), ("C", "P0") + ) + assert model.check_assignment({"A": "P0", "B": "P1", "C": "P0"}, query) + assert not model.check_assignment({"A": "P0", "B": "P0", "C": "P1"}, query) + assert not model.check_assignment({"A": "P0", "B": "P1"}, query) + + +def test_portable_proof_translates_to_shared_student_chain(): + model = ExamRepairModel.create( + period_ids=("P0", "P1"), + exam_ids=("A", "B"), + students=((17,), (17,)), + candidate_periods=(("P0", "P1"), ("P0", "P1")), + ) + query = model.freeze_event(fixed=(("A", "P0"), ("B", "P0"))) + # A=P0 implies B=P1; the independently forced B=P0 reaches the opposite. + certificate = struct.pack("<4sIII3I", b"SBP1", 2, 2, 1, 0, 3, 2) + record = model.explain_unsat(query, certificate) + assert record["kind"] == "FORCED_OPPOSITES" + assert record["left"]["nodes"][0]["forced_by_event"] is True + assert record["left"]["steps"] == [{ + "kind": "SHARED_STUDENT_CONFLICT", + "from_exam": "A", + "from_period": "P0", + "to_exam": "B", + "therefore_period": "P1", + "student": 17, + }] + with pytest.raises(ValueError, match="does not prove"): + model.explain_unsat((), certificate) + + +def test_empty_domain_proof_names_the_closed_exam(): + model = path_model() + query = model.freeze_event(closed_periods=("P0", "P1")) + certificate = struct.pack("<4sIIII", b"SBP1", 1, 1, 0, 0) + assert model.explain_unsat(query, certificate) == { + "schema": "spectra.exam_repair.proof.v1", + "kind": "EMPTY_DOMAIN", + "exam": "A", + "original_candidates": ["P0", "P1"], + "remaining_candidates": [], + } + + +def test_adapter_rejects_ambiguous_or_out_of_scope_input_shapes(): + with pytest.raises(ValueError, match="one or two"): + ExamRepairModel.create(("P",), ("A",), ((),), ((),)) + with pytest.raises(ValueError, match="unique"): + ExamRepairModel.create(("P", "P"), (), (), ()) + with pytest.raises(ValueError, match="cannot exclude itself"): + ExamRepairModel.create(("P",), ("A",), ((),), (("P",),), exclusions=(("A", "A"),)) + with pytest.raises(ValueError, match="period identifier count exceeds"): + ExamRepairModel.create((f"P{i}" for i in range(65)), (), (), ()) + + +def _compiler_available() -> bool: + return bool(shutil.which("cl" if sys.platform == "win32" else "g++")) + + +@pytest.mark.skipif(sys.platform not in ("linux", "win32") or not _compiler_available(), + reason="supported native compiler unavailable") +def test_adapter_runs_through_public_native_api(tmp_path): + model = path_model() + runtime = ExactRuntime(build_exact_runtime(tmp_path / "native")) + sat_query = model.freeze_event(fixed=(("A", "P0"), ("C", "P0"))) + unsat_query = model.freeze_event(fixed=(("A", "P0"), ("B", "P0"))) + with runtime.prepare(model.problem, mode="scc") as session: + sat = session.solve(sat_query) + unsat = session.solve(unsat_query) + assert sat.status == "SAT_VERIFIED" + assert model.check_assignment(model.assignment_from_labels(sat.labels, sat_query), sat_query) + assert unsat.status == "UNSAT_VERIFIED" + explained = model.explain_unsat(unsat_query, unsat.proof) + assert explained["kind"] == "FORCED_OPPOSITES" + assert any(step.get("student") == 1 + for side in ("left", "right") for step in explained[side]["steps"]) diff --git a/tests/public/test_itc2007_exam.py b/tests/public/test_itc2007_exam.py new file mode 100644 index 0000000..bdbbf1b --- /dev/null +++ b/tests/public/test_itc2007_exam.py @@ -0,0 +1,85 @@ +"""Strict ITC 2007 parser and bounded conflict-core adapter contracts.""" +from __future__ import annotations + +import pytest + +from spectra.itc2007_exam import parse_itc2007_exam + + +FIXTURE = """[Exams:3] +120, 1, 2 +180, 2, 3 +120, 9 +[Periods:3] +01:01:2030, 09:00:00, 180, 0 +01:01:2030, 14:00:00, 120, 5 +02:01:2030, 09:00:00, 240, 0 +[Rooms:1] +100, 0 +[PeriodHardConstraints] +0, EXCLUSION, 2 +1, AFTER, 0 +[RoomHardConstraints] +2, ROOM_EXCLUSIVE +[InstitutionalWeightings] +TWOINAROW, 30 +""" + + +def test_parser_preserves_complete_constraint_inventory(): + instance = parse_itc2007_exam(FIXTURE) + assert len(instance.exams) == 3 + assert instance.exams[0].students == (1, 2) + assert len(instance.periods) == 3 + assert instance.after == ((1, 0),) + assert instance.exclusions == ((0, 2),) + assert instance.room_exclusive == (2,) + assert dict(instance.ignored_constraint_counts) == { + "after": 1, + "room_exclusive": 1, + "room_assignment": 1, + "period_penalties": 1, + "institutional_weightings": 1, + } + assert len(instance.source_sha256) == 64 + + +def test_conflict_core_requires_explicit_scope_acknowledgement(): + instance = parse_itc2007_exam(FIXTURE) + candidates = ((0, 1), (0, 2), (1, 2)) + with pytest.raises(ValueError, match="would ignore"): + instance.conflict_core(candidates) + core = instance.conflict_core(candidates, acknowledge_ignored_constraints=True) + # Exam 0/1 share student 2; exam 0/2 have explicit EXCLUSION. + assert core.model.problem.edges == ((0, 1), (0, 2)) + assert core.model.candidates[0] == ( + "00:01:01:2030 09:00:00", "01:01:01:2030 14:00:00" + ) + assert core.info["schema"] == "spectra.itc2007.conflict_core.v1" + assert "not a complete ITC 2007 timetable" in core.info["claim_boundary"] + + +def test_duration_check_rejects_unapproved_short_period(): + instance = parse_itc2007_exam(FIXTURE) + # Exam 1 lasts 180 minutes; period 1 lasts only 120. + with pytest.raises(ValueError, match="does not fit"): + instance.conflict_core(((0,), (1,), (2,)), acknowledge_ignored_constraints=True) + + +def test_conflict_core_rejects_noniterable_candidate_rows(): + instance = parse_itc2007_exam(FIXTURE) + with pytest.raises(ValueError, match="period-index iterables"): + instance.conflict_core(((0,), 1, (2,)), acknowledge_ignored_constraints=True) + + +@pytest.mark.parametrize("damage, message", [ + (FIXTURE.replace("[Exams:3]", "[Exams:4]"), "row count differs"), + (FIXTURE.replace("[Periods:3]", "[Unknown:3]"), "unknown ITC section"), + (FIXTURE.replace("120, 1, 2", "120, 1, 1"), "duplicate student"), + (FIXTURE.replace("0, EXCLUSION, 2", "0, OTHER, 2"), "unsupported period relation"), + (FIXTURE.replace("0, EXCLUSION, 2", "0, EXCLUSION, 2\n2, EXCLUSION, 0"), + "duplicate period hard constraint"), +]) +def test_parser_fails_closed_on_malformed_instances(damage, message): + with pytest.raises(ValueError, match=message): + parse_itc2007_exam(damage)