Source
Satisfiability (already in codebase)
Target
MaximumDomaticNumber (see #878)
Motivation
The NP-completeness of the Domatic Number problem is established by reduction from 3-SATISFIABILITY (Garey, Johnson, and Tarjan, 1976b). This is the canonical reduction listed in Garey & Johnson A1.1 GT3 (R236). Since 3-SAT is a special case of Satisfiability, this reduction applies from the existing Satisfiability model.
Reference
- Garey, M.R., Johnson, D.S., and Tarjan, R.E. (1976). "The planar Hamiltonian circuit problem is NP-complete." SIAM Journal on Computing, 5(4):704-714.
- Garey & Johnson, Computers and Intractability, A1.1 GT3, reference R236.
Reduction Algorithm
Given a 3-CNF formula F with variables x_1, ..., x_n and clauses C_1, ..., C_m (an instance of Satisfiability):
- For each variable x_i, create a variable gadget that enforces true/false assignment via domination constraints.
- For each clause C_j, create a clause gadget that is satisfiable (can participate in a valid partition) only if at least one literal in the clause is true.
- Connect variable and clause gadgets so that the graph has domatic number >= K if and only if the formula is satisfiable.
(Detailed construction follows Garey, Johnson, and Tarjan 1976b.)
Size Overhead
TBD — depends on the detailed gadget construction. Typically polynomial in n + m.
Validation Method
- Construct small 3-SAT instances with known satisfiability.
- Build the reduced graph and verify the domatic number matches the expected value.
- Cross-check with brute-force solver on both source and target.
Example
For the formula F = (x1 v x2 v x3) & (~x1 v ~x2 v x3):
This is satisfiable (e.g., x1=T, x2=T, x3=T). The reduced graph should have domatic number >= K (where K depends on the construction). An unsatisfiable formula would yield a graph with domatic number < K.
(Detailed example requires the full gadget construction from the original paper.)
Dependencies
Source
Satisfiability(already in codebase)Target
MaximumDomaticNumber(see #878)Motivation
The NP-completeness of the Domatic Number problem is established by reduction from 3-SATISFIABILITY (Garey, Johnson, and Tarjan, 1976b). This is the canonical reduction listed in Garey & Johnson A1.1 GT3 (R236). Since 3-SAT is a special case of Satisfiability, this reduction applies from the existing Satisfiability model.
Reference
Reduction Algorithm
Given a 3-CNF formula F with variables x_1, ..., x_n and clauses C_1, ..., C_m (an instance of Satisfiability):
(Detailed construction follows Garey, Johnson, and Tarjan 1976b.)
Size Overhead
TBD — depends on the detailed gadget construction. Typically polynomial in n + m.
Validation Method
Example
For the formula F = (x1 v x2 v x3) & (~x1 v ~x2 v x3):
This is satisfiable (e.g., x1=T, x2=T, x3=T). The reduced graph should have domatic number >= K (where K depends on the construction). An unsatisfiable formula would yield a graph with domatic number < K.
(Detailed example requires the full gadget construction from the original paper.)
Dependencies
Satisfiabilitymodel already exists in codebase.MaximumDomaticNumbermodel must be implemented first (see [Model] MaximumDomaticNumber #878).