Research artifacts for the queen domination problem, organized across separate branches.
SAT-based enumeration of minimum dom. sets up to symmetry, with independently verifiable completeness proofs, for boards up to (n=19).
- v1 (
sat-solving): Original SAT encoding with Hilbert-curve literal ordering, symmetry breaking, and Cube-and-Conquer. - v2 (
gamma-plus, ADAM 2026): Improved line-variable encoding and integrated proof-producing enumeration pipeline.
Hint and Conquer — hint-and-conquer
SAT-based unsatisfiability proofs using counting hints, establishing six new exact queen domination numbers for even boards up to (n=38).
Larger Type E Constructions — upper-bound
Constraint-programming search for Type E dominating sets, producing constructions up to (n=1585) and improved asymptotic upper bounds.
Released under the MIT License.