From 124a803bfe8b8f63790d5bcb31739f9023fbec53 Mon Sep 17 00:00:00 2001 From: Kinvectum <134240819+KAVentures@users.noreply.github.com> Date: Mon, 27 Jul 2026 20:31:19 +0200 Subject: [PATCH 1/6] Add isolated runner for exact Tihany search --- .github/workflows/tihany-runner.yml | 75 +++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 .github/workflows/tihany-runner.yml diff --git a/.github/workflows/tihany-runner.yml b/.github/workflows/tihany-runner.yml new file mode 100644 index 0000000..747d141 --- /dev/null +++ b/.github/workflows/tihany-runner.yml @@ -0,0 +1,75 @@ +name: Isolated Tihany exact search + +on: + push: + branches: + - research/tihany-runner + pull_request: + branches: + - master + paths: + - '.github/workflows/tihany-runner.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + validate-and-search: + runs-on: ubuntu-24.04 + timeout-minutes: 350 + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.12' + - name: Fetch audited research source + run: | + git clone --depth 1 --branch research/tihany-exact-core \ + https://github.com/KAVentures/stable-set-flow-gadgets.git tihany-source + git -C tihany-source rev-parse HEAD | tee source-commit.txt + - name: Install exact dependencies + run: pip install 'python-sat[pblib,aiger]' networkx + - name: Compile independent verifier + run: | + g++ -O3 -std=c++17 -Wall -Wextra -pedantic \ + tihany-source/experiments/tihany/verify_graph.cpp \ + -o tihany-source/experiments/tihany/verify_graph + - name: Run validation suite + working-directory: tihany-source/experiments/tihany + run: python tests.py + - name: Run direct core CEGAR + run: | + set +e + timeout --signal=INT --kill-after=90s 19600s \ + python tihany-source/experiments/tihany/core_search.py \ + --mode core --out artifacts/core --max-seconds 19400 + status=$? + set -e + case "$status" in 0|10|20|124|130) ;; *) exit "$status";; esac + - name: Verify any candidate independently + if: always() + run: | + if [[ -f artifacts/core/candidate.edges ]]; then + python tihany-source/experiments/tihany/verify_graph.py \ + artifacts/core/candidate.edges --output artifacts/core/python-independent.json + tihany-source/experiments/tihany/verify_graph \ + artifacts/core/candidate.edges | tee artifacts/core/cpp-independent.log + fi + - name: Produce proof certificate if core converged to UNSAT + if: always() + run: | + if [[ -f artifacts/core/static_core.cnf ]]; then + bash tihany-source/experiments/tihany/run_certified.sh \ + artifacts/core/static_core.cnf artifacts/core/certificate + else + echo 'No static UNSAT formula yet.' + fi + - uses: actions/upload-artifact@v4 + if: always() + with: + name: isolated-tihany-core + path: | + artifacts/core + source-commit.txt + retention-days: 90 From addfd1497841252b7f3beba3ab7d8612fb5b1830 Mon Sep 17 00:00:00 2001 From: Kinvectum <134240819+KAVentures@users.noreply.github.com> Date: Mon, 27 Jul 2026 20:36:21 +0200 Subject: [PATCH 2/6] Run common-rainbow ablations in parallel --- .github/workflows/tihany-runner.yml | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/.github/workflows/tihany-runner.yml b/.github/workflows/tihany-runner.yml index 747d141..f7e1ea6 100644 --- a/.github/workflows/tihany-runner.yml +++ b/.github/workflows/tihany-runner.yml @@ -73,3 +73,32 @@ jobs: artifacts/core source-commit.txt retention-days: 90 + + rainbow-ablation: + runs-on: ubuntu-24.04 + timeout-minutes: 350 + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.12' + - name: Fetch audited research source + run: | + git clone --depth 1 --branch research/tihany-exact-core \ + https://github.com/KAVentures/stable-set-flow-gadgets.git tihany-source + git -C tihany-source rev-parse HEAD | tee ablation-source-commit.txt + - name: Install exact dependencies + run: pip install 'python-sat[pblib,aiger]' + - name: Run structural ablation grid + run: | + timeout --signal=TERM --kill-after=60s 19800s \ + python tihany-source/experiments/tihany/ablation.py \ + --out artifacts/ablation --timeout 600 --profiles + - uses: actions/upload-artifact@v4 + if: always() + with: + name: isolated-tihany-ablation + path: | + artifacts/ablation + ablation-source-commit.txt + retention-days: 90 From ca1422bc404d97b018df5b1ecde6591a417fc5cc Mon Sep 17 00:00:00 2001 From: Kinvectum <134240819+KAVentures@users.noreply.github.com> Date: Mon, 27 Jul 2026 20:37:51 +0200 Subject: [PATCH 3/6] Probe orders 18 and 19 in parallel --- .github/workflows/tihany-runner.yml | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/.github/workflows/tihany-runner.yml b/.github/workflows/tihany-runner.yml index f7e1ea6..0e0aef3 100644 --- a/.github/workflows/tihany-runner.yml +++ b/.github/workflows/tihany-runner.yml @@ -102,3 +102,32 @@ jobs: artifacts/ablation ablation-source-commit.txt retention-days: 90 + + higher-order-sweep: + runs-on: ubuntu-24.04 + timeout-minutes: 350 + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.12' + - name: Fetch audited research source + run: | + git clone --depth 1 --branch research/tihany-exact-core \ + https://github.com/KAVentures/stable-set-flow-gadgets.git tihany-source + git -C tihany-source rev-parse HEAD | tee sweep-source-commit.txt + - name: Install exact dependencies + run: pip install 'python-sat[pblib,aiger]' + - name: Probe orders 18 and 19 + run: | + timeout --signal=TERM --kill-after=60s 19800s \ + python tihany-source/experiments/tihany/order_sweep.py \ + --orders 18 19 --out artifacts/sweep --timeout 3000 + - uses: actions/upload-artifact@v4 + if: always() + with: + name: isolated-tihany-order-sweep + path: | + artifacts/sweep + sweep-source-commit.txt + retention-days: 90 From 93bc2d157f41d2ceed606063ac1677909963dd41 Mon Sep 17 00:00:00 2001 From: Kinvectum <134240819+KAVentures@users.noreply.github.com> Date: Mon, 27 Jul 2026 20:46:40 +0200 Subject: [PATCH 4/6] Cancel stale exact-search workflow attempts --- .github/workflows/tihany-runner.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/tihany-runner.yml b/.github/workflows/tihany-runner.yml index 0e0aef3..ef5cad8 100644 --- a/.github/workflows/tihany-runner.yml +++ b/.github/workflows/tihany-runner.yml @@ -11,6 +11,10 @@ on: - '.github/workflows/tihany-runner.yml' workflow_dispatch: +concurrency: + group: isolated-tihany-${{ github.repository }}-${{ github.ref }} + cancel-in-progress: true + permissions: contents: read From 1bc45eb1384faa50e793255bf067d27e28eafc59 Mon Sep 17 00:00:00 2001 From: Kinvectum <134240819+KAVentures@users.noreply.github.com> Date: Mon, 27 Jul 2026 21:01:06 +0200 Subject: [PATCH 5/6] Use general GitHub hosted runner label --- .github/workflows/tihany-runner.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/tihany-runner.yml b/.github/workflows/tihany-runner.yml index ef5cad8..5218d70 100644 --- a/.github/workflows/tihany-runner.yml +++ b/.github/workflows/tihany-runner.yml @@ -20,7 +20,7 @@ permissions: jobs: validate-and-search: - runs-on: ubuntu-24.04 + runs-on: ubuntu-latest timeout-minutes: 350 steps: - uses: actions/checkout@v4 @@ -79,7 +79,7 @@ jobs: retention-days: 90 rainbow-ablation: - runs-on: ubuntu-24.04 + runs-on: ubuntu-latest timeout-minutes: 350 steps: - uses: actions/checkout@v4 @@ -108,7 +108,7 @@ jobs: retention-days: 90 higher-order-sweep: - runs-on: ubuntu-24.04 + runs-on: ubuntu-latest timeout-minutes: 350 steps: - uses: actions/checkout@v4 From 7feeb416c0163f983bb0211132f0d3d4ab580d85 Mon Sep 17 00:00:00 2001 From: Kinvectum <134240819+KAVentures@users.noreply.github.com> Date: Mon, 27 Jul 2026 23:20:15 +0200 Subject: [PATCH 6/6] Add audited core and reduction-independent ultracore runs --- .github/workflows/tihany-runner.yml | 78 +++++++++++++++++++++++++++-- 1 file changed, 74 insertions(+), 4 deletions(-) diff --git a/.github/workflows/tihany-runner.yml b/.github/workflows/tihany-runner.yml index 5218d70..9c395f0 100644 --- a/.github/workflows/tihany-runner.yml +++ b/.github/workflows/tihany-runner.yml @@ -34,11 +34,14 @@ jobs: git -C tihany-source rev-parse HEAD | tee source-commit.txt - name: Install exact dependencies run: pip install 'python-sat[pblib,aiger]' networkx - - name: Compile independent verifier + - name: Compile independent verifiers run: | g++ -O3 -std=c++17 -Wall -Wextra -pedantic \ tihany-source/experiments/tihany/verify_graph.cpp \ -o tihany-source/experiments/tihany/verify_graph + g++ -O3 -std=c++17 -Wall -Wextra -pedantic \ + tihany-source/experiments/tihany/verify_graph_generic.cpp \ + -o tihany-source/experiments/tihany/verify_graph_generic - name: Run validation suite working-directory: tihany-source/experiments/tihany run: python tests.py @@ -51,7 +54,7 @@ jobs: status=$? set -e case "$status" in 0|10|20|124|130) ;; *) exit "$status";; esac - - name: Verify any candidate independently + - name: Verify any core candidate independently if: always() run: | if [[ -f artifacts/core/candidate.edges ]]; then @@ -60,14 +63,19 @@ jobs: tihany-source/experiments/tihany/verify_graph \ artifacts/core/candidate.edges | tee artifacts/core/cpp-independent.log fi - - name: Produce proof certificate if core converged to UNSAT + - name: Audit and certify any static core UNSAT formula if: always() run: | if [[ -f artifacts/core/static_core.cnf ]]; then + python tihany-source/experiments/tihany/audit_static.py \ + --mode core \ + --cuts artifacts/core/cuts.jsonl \ + --static artifacts/core/static_core.cnf \ + --output artifacts/core/static-audit.json bash tihany-source/experiments/tihany/run_certified.sh \ artifacts/core/static_core.cnf artifacts/core/certificate else - echo 'No static UNSAT formula yet.' + echo 'No static core UNSAT formula yet.' fi - uses: actions/upload-artifact@v4 if: always() @@ -78,6 +86,68 @@ jobs: source-commit.txt retention-days: 90 + ultracore-search: + runs-on: ubuntu-latest + timeout-minutes: 350 + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.12' + - name: Fetch audited research source + run: | + git clone --depth 1 --branch research/tihany-exact-core \ + https://github.com/KAVentures/stable-set-flow-gadgets.git tihany-source + git -C tihany-source rev-parse HEAD | tee ultracore-source-commit.txt + - name: Install exact dependencies + run: pip install 'python-sat[pblib,aiger]' + - name: Compile generic verifier + run: | + g++ -O3 -std=c++17 -Wall -Wextra -pedantic \ + tihany-source/experiments/tihany/verify_graph_generic.cpp \ + -o tihany-source/experiments/tihany/verify_graph_generic + - name: Run reduction-independent CEGAR + run: | + set +e + timeout --signal=INT --kill-after=90s 19600s \ + python tihany-source/experiments/tihany/ultracore_search.py \ + --out artifacts/ultracore --max-seconds 19400 + status=$? + set -e + case "$status" in 0|10|20|124|130) ;; *) exit "$status";; esac + - name: Verify any ultracore candidate independently + if: always() + run: | + if [[ -f artifacts/ultracore/candidate.edges ]]; then + python tihany-source/experiments/tihany/verify_graph_generic.py \ + artifacts/ultracore/candidate.edges \ + --output artifacts/ultracore/python-generic.json + tihany-source/experiments/tihany/verify_graph_generic \ + artifacts/ultracore/candidate.edges | tee artifacts/ultracore/cpp-generic.log + fi + - name: Audit and certify any ultracore UNSAT formula + if: always() + run: | + if [[ -f artifacts/ultracore/static_ultracore.cnf ]]; then + python tihany-source/experiments/tihany/audit_static.py \ + --mode ultracore \ + --cuts artifacts/ultracore/cuts.jsonl \ + --static artifacts/ultracore/static_ultracore.cnf \ + --output artifacts/ultracore/static-audit.json + bash tihany-source/experiments/tihany/run_certified.sh \ + artifacts/ultracore/static_ultracore.cnf artifacts/ultracore/certificate + else + echo 'No static ultracore UNSAT formula yet.' + fi + - uses: actions/upload-artifact@v4 + if: always() + with: + name: isolated-tihany-ultracore + path: | + artifacts/ultracore + ultracore-source-commit.txt + retention-days: 90 + rainbow-ablation: runs-on: ubuntu-latest timeout-minutes: 350