Isolated runner for the exact Tihany order-17 search

.github/workflows/tihany-runner.yml

@@ -0,0 +1,207 @@
+name: Isolated Tihany exact search
+
+on:
+  push:
+    branches:
+      - research/tihany-runner
+  pull_request:
+    branches:
+      - master
+    paths:
+      - '.github/workflows/tihany-runner.yml'
+  workflow_dispatch:
+
+concurrency:
+  group: isolated-tihany-${{ github.repository }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  validate-and-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 source-commit.txt
+      - name: Install exact dependencies
+        run: pip install 'python-sat[pblib,aiger]' networkx
+      - 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
+      - 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 core 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: 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 core 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
+
+  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
+    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
+
+  higher-order-sweep:
+    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 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