Solver-Hard Is Not Model-Hard

Code, data, and deterministic receipts for “Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning” by Lucky Verma (Independent Researcher).

The scoped result is negative: Glucose conflict counts separate the Tseitin expander and ladder families by 3.3x to 51.4x across registered size bins, while the pooled three-model accuracy contrast is +1.7 percentage points (p=0.73981) and 0/3 models pass the registered transfer gate. Conflict counts are solver-specific proxies, and the model endpoint is parsed verdict accuracy—not certificate-verified SAT solving.

Quick start

Python 3.11 or newer is recommended.

git clone https://github.com/lucky-verma/solver-hard-is-not-model-hard.git
cd solver-hard-is-not-model-hard
python3 -m pip install -r requirements.txt
python3 scripts/verify_release.py
python3 -m pytest -q

The verifier checks all release checksums, JSON schemas and row counts, headline receipts, source normalization, filenames, generated-text exclusion, and common secret/local-path patterns.

Contents

data/instances/       Synthetic SAT/CNF instances
data/results/         Derived model measurements and aggregate receipts
docs/                 Registered analysis and multi-solver protocols
figures/              Deterministic plotting scripts
provenance/           Claim map and source/transformation ledger
scripts/              Generators, runners, scorers, and release verifier
tests/                Release and analysis regression tests

The exact old-to-public filename map is in provenance/SOURCE_ARTIFACT.json. Legacy experiment IDs retained inside records are provenance fields, not public file names.

Reproduce the analyses

Write outputs outside the repository so the released receipts remain immutable:

python3 scripts/score_hardness_transfer.py \
  --out /tmp/primary_three_model_summary.json
python3 scripts/score_surface_controls.py \
  --out /tmp/surface_control_summary.json
python3 scripts/analyze_surface_clusters.py \
  --out /tmp/surface_cluster_summary.json
python3 scripts/analyze_token_spend.py \
  --out /tmp/token_spend_summary.json
python3 scripts/run_multi_solver_sensitivity.py \
  --raw-out /tmp/multi_solver_rows.jsonl \
  --summary-out /tmp/multi_solver_summary.json

The first three are exact deterministic recomputations. The token-spend receipt includes runtime provenance fields that will differ. The multi-solver rerun should preserve the registered CONFIRM verdict; wall-clock fields may differ.

Generate the paper figures with:

python3 figures/plot_hardness_transfer.py
python3 figures/plot_surface_controls.py
python3 figures/plot_token_spend.py

Generated PDFs are ignored by Git.

Data boundary

The release includes synthetic inputs, parsed labels, accuracy/abstention fields, token and character counts, timing, solver metrics, and aggregate statistics. It does not redistribute generated model response text, credentials, personal/client data, or local machine paths. Stable error categories replace raw provider exception messages. See DATA_CARD.md for scope and limitations.

The provider runners are included for protocol inspection and optional replay. Replay requires caller-supplied credentials, may incur cost, and cannot guarantee immutable checkpoint identity for hosted models.

Provenance

This tree was normalized from the attested anonymous artifact rhd-blackboxnlp2026-20260716-v1 (SHA-256 ed2bce85abda95c629b32b6031b35a961923a6202aa5fb37a74fb5e9958b5c4c). Synthetic inputs and solver receipts remain byte-identical. Model-result rows were deterministically sanitized by removing raw_tail and reducing raw exception messages to stable categories; the transformation is bound in the source ledger and release checksums.

License and citation

Code is Apache-2.0; released data under data/ is CC BY 4.0. See LICENSE, LICENSE-DATA.md, and CITATION.cff.