diff --git a/.github/workflows/tihany-runner.yml b/.github/workflows/tihany-runner.yml new file mode 100644 index 0000000..9c395f0 --- /dev/null +++ b/.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