1#!/bin/sh2# Rebuilds the tractable experiments of the study and re-checks the certificates.3#4# sh code/reproduce.sh default : bounded reproduction, about 25 min on 16 cores (our run: steps 0-7 in 26 min5# before trimming; now bounded well inside the platform's 60 min limit)6# QUICK=1 sh code/reproduce.sh checks only, about 10 min7# FULL=1 sh code/reproduce.sh everything (adds roughly 5-6 h; see step 11)8#9# Where it writes. Nothing in the shipped archive is modified: the script makes a working copy10# of code/ and of the small result files under results/reproduction/work/ (symlinking the11# shipped certificate directory and .pydeps), runs every step there, writes regenerated12# certificates to results/reproduction/work/certificates/, and finally compares the working13# copy with the shipped files (code/tools/compare_reproduction.py) into14# results/reproduction/summary.json. Its execution log is results/reproduction/experiment-log.jsonl.15# INPLACE=1 runs in the archive itself instead (appends to the shipped record files; not16# recommended), REPRO_WORK=DIR chooses another working directory.17#18# What each mode does (manuscript Appendix C):19# QUICK : steps 0-3, 9, 10. Builds the tools, re-runs the graph-invariant, order-independence and20# lemma checks, replays every stored witness, and re-verifies with drat-trim the shipped21# fort-cover proofs for n = 11..21 and a fixed sample of the boundary proofs22# (n = 24, 26..40, 60) if they are present on disk; rebuilds tables and metrics23# in the working copy; re-runs the Stage 5 robustness checks that need no enumeration.24# Proofs not present on disk are reported as "skipped", never as verified.25# default : adds steps 4-8: exhaustive oracle n = 11..22 (rows 11..22 of Table 2), the boundary26# table for p = 16..20, the certified window for 26 <= n <= 40 regenerated with fresh27# DRAT proofs (checked, and their CNF digests compared with the shipped records), the28# fort-cover certificates n = 11..21 (column F of Table 1 for n <= 21; the round-based29# encoding only for n <= 17 with a 60 s limit), then a re-check of the regenerated30# certificates.31# FULL=1 : adds step 11: exhaustive oracle n = 23..27 (rows 23..27 of Table 2, about 70 min),32# the complete boundary table p = 12..24, the complete certified window 26 <= n <= 15433# (about 35 min on 12 cores), the fort-cover certificate n = 22 (about 11 min), a re-check of34# every shipped proof present on disk including the 4.0 GB (n = 23) fort-cover proof (about35# 2 h), a drat-trim check of the stored 7.7 GB n = 25 proof file (status unknown; 1-2 h),36# proof-logging re-solves of the stored fort-cover CNFs for n = 23 and 25 (about 2-3 h37# including drat-trim), the round encoding n = 18..22 with the original 600 s limit,38# the second enumerator E' through n = 40 (about 1 h) and the exhaustive boundary-encoding39# checks of Section 8(c).40# Any interrupted step leaves the result rows of that step unchanged; a timed-out or killed solver is41# never recorded as UNSAT.42set -e43ROOT=$(cd "$(dirname "$0")/.." && pwd)44cd "$ROOT"45MODE=default; [ -n "$QUICK" ] && MODE=quick; [ "${FULL:-0}" = "1" ] && MODE=full46T0=$(date -u +%FT%TZ)4748if [ "${INPLACE:-0}" = "1" ]; then49 WORK="$ROOT"50 export AUTOSCHOLAR_CERTS_DIR="$ROOT/results/reproduction/certificates"51else52 WORK=${REPRO_WORK:-$ROOT/results/reproduction/work}53 rm -rf "$WORK"; mkdir -p "$WORK/code/proofs" "$WORK/results"54 rsync -a --exclude proofs/certificates --exclude brute_force --exclude robustness/ff_brute --exclude robustness/beta_brute \55 --exclude tools/drat-trim/drat-trim "$ROOT/code/" "$WORK/code/"56 ln -s "$ROOT/code/proofs/certificates" "$WORK/code/proofs/certificates"57 [ -d "$ROOT/.pydeps" ] && ln -s "$ROOT/.pydeps" "$WORK/.pydeps"58 cp "$ROOT"/results/*.json "$ROOT"/results/*.jsonl "$ROOT"/results/*.csv "$ROOT"/results/*.md "$WORK/results/" 2>/dev/null || true59 for d in tables robustness; do [ -d "$ROOT/results/$d" ] && cp -R "$ROOT/results/$d" "$WORK/results/$d"; done60 export AUTOSCHOLAR_CERTS_DIR="$WORK/certificates"61fi62mkdir -p "$ROOT/results/reproduction" "$WORK/results/logs" "$AUTOSCHOLAR_CERTS_DIR"63export AUTOSCHOLAR_EXPLOG="$WORK/results/experiment-log.jsonl"64[ "$WORK" = "$ROOT" ] || : > "$AUTOSCHOLAR_EXPLOG"65cd "$WORK"66export PYTHONPATH=.pydeps:code67run() { name=$1; shift; echo "== $name: $*"; python3 code/tools/logrun.py "$name" --log "results/logs/$name.log" -- "$@"; }6869echo "[0] dependencies and tools (mode: $MODE, work: $WORK)"70[ -d .pydeps/pysat ] || python3 -m pip install --no-index --target "$ROOT/.pydeps" "$ROOT"/code/wheels/*.whl71run build_drat_trim gcc -O2 -o code/tools/drat-trim/drat-trim code/tools/drat-trim/drat-trim.c72run build_brute_force gcc -O2 -o code/brute_force code/brute_force.c73run build_ff_brute gcc -O2 -o code/robustness/ff_brute code/robustness/ff_brute.c -lpthread74run build_beta_brute gcc -O2 -o code/robustness/beta_brute code/robustness/beta_brute.c -lpthread7576echo "[1] graph invariants (T1) and order independence (T2)"77run T1_graph_invariants python3 code/graph_constructor.py 5 4878run T2_order_independence python3 code/closure_oracle.py7980echo "[2] lemma checks (CS6, T8, sympy)"81run lemma_checks python3 code/verify_lemmas.py8283echo "[3] independent certificate checks: witness replay; drat-trim on shipped proofs present on disk"84run verify_upper_bounds python3 code/verify_upper_bounds.py 6085if [ "$MODE" = "full" ]; then86 run verify_lower_bounds_all_shipped python3 code/verify_lower_bounds.py 887else88 VERIFY_BOUNDARY_N="24,26-40,60" VERIFY_FORTCOVER_N="11-21" VERIFY_MAX_PROOF_BYTES=1500000000 \89 run verify_lower_bounds_sample python3 code/verify_lower_bounds.py 890fi9192if [ "$MODE" != "quick" ]; then93 echo "[4] exhaustive oracle n = 11..22 (C program, 16 threads, ~2 min)"94 BF_TIME_LIMIT=3600 run brute_force_11_22 python3 code/brute_force.py 11 12 13 14 15 16 17 18 19 20 21 2295 echo "[5] boundary table p = 16..20, n = 13..30 (~2 min)"96 run boundary_table_p16_20 python3 code/run_boundary_table.py 16 20 13 30 1297 echo "[6] certified boundary window p = 18, n = 26..40, fresh DRAT proofs (~2 min)"98 run boundary_window_26_40 python3 code/run_boundary_window.py 18 26 40 1299 echo "[7] fort-cover certificates n = 11..21 (round encoding only n <= 17, 60 s limit; ~8 min; n = 22 is in FULL mode)"100 FORT_LIMIT=300 ROUND_LIMIT=60 run exact_fortcover_11_17 python3 code/run_exact.py 11 12 13 14 15 16 17101 FORT_LIMIT=600 SKIP_ROUND=1 run exact_fortcover_18_21 python3 code/run_exact.py 18 19 20 21102 echo "[8] re-check of the regenerated certificates with the independent checker"103 run verify_upper_bounds_again python3 code/verify_upper_bounds.py 60104 VERIFY_BOUNDARY_N="26-40" VERIFY_FORTCOVER_N="11-21" VERIFY_MAX_PROOF_BYTES=1500000000 \105 VERIFY_OUT=results/lower_bound_verification_regenerated.json run verify_lower_bounds_regenerated python3 code/verify_lower_bounds.py 8106fi107108echo "[9] tables and metrics (working copy)"109run build_tables python3 code/build_tables.py110111echo "[10] Stage 5 robustness checks that need no enumeration (see code/robustness/README.md)"112run robustness_check_counts python3 code/robustness/check_counts.py113run robustness_witness_replay python3 code/robustness/check_witness_replay.py114run robustness_deletion_lemma python3 code/robustness/check_deletion_lemma.py115run robustness_drat_negative_controls python3 code/robustness/check_drat_negative_controls.py116run robustness_margin python3 code/robustness/check_margin.py117run robustness_local_search python3 code/robustness/attack_local_search.py118119if [ "$MODE" = "full" ]; then120 echo "[11] FULL: exhaustive oracle n = 23..27, complete boundary table and window, big proof re-solves, E' enumerations"121 BF_TIME_LIMIT=3600 run brute_force_23_27 python3 code/brute_force.py 23 24 25 26 27122 run boundary_table_full python3 code/run_boundary_table.py 12 24 13 30 12123 run boundary_window_41_154 python3 code/run_boundary_window.py 18 41 154 12124 FORT_LIMIT=600 SKIP_ROUND=1 run exact_fortcover_22 python3 code/run_exact.py 22125 FORT_LIMIT=600 ROUND_LIMIT=600 run exact_round_18_22 python3 code/run_exact.py 18 19 20 21 22126 run regen_fortcover_proof_23 python3 code/regen_fortcover_proof.py 23 11127 run regen_fortcover_proof_25 python3 code/regen_fortcover_proof.py 25 11128 # drat-trim on the stored n = 25 proof file (exit 1 and no record if it does not verify)129 run check_fortcover_proof_25 python3 code/check_fortcover_proof.py 25 11 18000 || true130 VERIFY_OUT=results/lower_bound_verification_regenerated.json run verify_lower_bounds_regenerated_full python3 code/verify_lower_bounds.py 8131 run build_tables_full python3 code/build_tables.py132 run robustness_beta_brute sh code/robustness/run_beta_brute.sh133 run robustness_boundary_encoding python3 code/robustness/check_boundary_encoding.py134 run robustness_ff_brute sh code/robustness/run_ff_brute.sh135 for n in 31 32 33 34 35 36 37 38 39 40; do code/robustness/ff_brute $n 5 11 16; done >> results/robustness/ff_brute_stdout_31_40.txt136fi137run robustness_collect python3 code/robustness/collect_robustness_metrics.py138139echo "[12] comparison with the shipped artifacts"140cd "$ROOT"141set +e142python3 code/tools/compare_reproduction.py "$WORK" "$ROOT" "$MODE" "$ROOT/results/reproduction/summary.json"143CMP=$?144set -e145[ "$WORK" = "$ROOT" ] || cp "$AUTOSCHOLAR_EXPLOG" "$ROOT/results/reproduction/experiment-log.jsonl"146# remove compiled binaries (rebuilt by step 0) and regenerated DRAT proofs (their digests are in the records)147rm -f "$WORK/code/brute_force" "$WORK/code/robustness/ff_brute" "$WORK/code/robustness/beta_brute" "$WORK/code/tools/drat-trim/drat-trim"148find "$AUTOSCHOLAR_CERTS_DIR" -name '*.drat' -delete 2>/dev/null || true149echo "reproduce.sh finished: mode=$MODE started=$T0 ended=$(date -u +%FT%TZ) comparison_exit=$CMP (results/reproduction/summary.json)"150exit $CMP151