NOCQ ATVA Artifact

NOCQ: A Constraint-Based Toolchain for Parity Games with Quantitative Conditions This release provides the official, self-contained artifact accompanying our paper submission to ATVA 2026. Abstract Solving parity games is a cornerstone problem in formal verification and synthesis, with significant applications across industrial-scale system design. This artifact presents the complete, open-source toolchain and evaluation framework for NOCQ, an efficient constraint-based toolchain designed to solve parity games under quantitative conditions using Constraint Programming (CP) techniques. The artifact is packaged as a single, self-contained environment to allow reviewers to independently verify, compile, and execute the tool without complex local dependency configurations. It includes: (1) a pre-compiled Docker image containing the full NOCQ binary and its runtime environment; (2) a representative subset of benchmark instances derived from the public PGSolver suite; and (3) automated evaluation scripts demonstrating the performance and correctness claims of the toolchain under parity, energy, and mean-payoff conditions. Additionally, the original cluster-scale Slurm scripts used to collect the comprehensive experimental tables in the accompanying paper are included for archival reference. The artifact source and full setup instructions are publicly hosted at https://github.com/gonzalohernandez/nocq. Artifact Contents (Contained within the unified ZIP archive) In complete compliance with ATVA evaluation instructions, all components are packaged in this container. Core Toolchain & Documentation Bundle (nocq-atva-artifact.zip): A single compressed archive enclosing the primary environment and setup files: solver-image.tar.gz: Pre-built and self-contained, enclosing the full execution environment, NOCQ, and baseline solvers (Oink, Cadical, Kissat, MiniSat), LICENSE File: Outlining the open-source licensing terms governing this software framework, and README.md: This instruction and configuration guide. Benchmark Sets: 5 Zip archives containing game instances categorized by evaluation type (equivchecking, modelchecking, pgsolver, random, and sprand). Package of python scripts (python_scripts.zip): 4 Main Python Scripts: Execution entry points (benchmarking_t*.py) configured to reconstruct Tables 1–4 from the accompanying paper, and 8 Auxiliary Python Scripts: Configuration files (games_*.py) that manage and map specific game suites to the main evaluation runs. Please see README.md file first.