[Rule] 3-SATISFIABILITY to ACYCLIC PARTITION

[isPANN]

---

name: Rule
about: Propose a new reduction rule
title: "[Rule] 3SAT to ACYCLIC PARTITION"
labels: rule
assignees: ''
canonical_source_name: '3-SATISFIABILITY'
canonical_target_name: 'ACYCLIC PARTITION'
source_in_codebase: true
target_in_codebase: false

Source: 3SAT
Target: ACYCLIC PARTITION
Motivation: Establishes NP-completeness of ACYCLIC PARTITION via polynomial-time reduction from 3SAT. The reduction encodes truth assignments as partition choices in a directed graph, using the acyclicity constraint to force consistency and clause satisfaction. This shows that partitioning a directed graph into bounded-weight acyclic groups is intractable even with just 2 groups and unit weights.

Reference: Garey & Johnson, Computers and Intractability, ND15, p.210

GJ Source Entry

[ND15] ACYCLIC PARTITION
INSTANCE: Directed graph G=(V,A), positive integer K.
QUESTION: Can V be partitioned into K disjoint sets V_1,...,V_K such that the subgraph of G induced by each V_i is acyclic?
Reference: [Garey and Johnson, 1979]. Transformation from 3SAT.
Comment: NP-complete even for K=2.

Reduction Algorithm

Summary:
Given a KSatisfiability instance with n variables U = {u_1, ..., u_n} and m clauses C = {c_1, ..., c_m}, construct an AcyclicPartition instance (G = (V, A), K = 2) as follows:

1. Variable gadgets: For each variable u_i, create a directed cycle of length 3 on vertices {v_i, v_i', v_i''}. The arcs are (v_i -> v_i'), (v_i' -> v_i''), (v_i'' -> v_i). In any partition of V into two sets where each induced subgraph is acyclic, at least one arc of this 3-cycle must cross between the two sets -- meaning at least one vertex from each 3-cycle must be in a different partition set. This encodes the binary truth assignment: if v_i is in V_1, interpret u_i = True; if v_i is in V_2, interpret u_i = False.

2. Clause gadgets: For each clause c_j = (l_1 OR l_2 OR l_3) where each l_k is a literal (u_i or NOT u_i), create a directed 3-cycle on fresh clause vertices {a_j, b_j, c_j_vertex}. The arcs are (a_j -> b_j), (b_j -> c_j_vertex), (c_j_vertex -> a_j).

3. Connection arcs (literal to clause): For each literal l_k in clause c_j, add a pair of arcs connecting the variable gadget vertex corresponding to l_k to the clause gadget. Specifically:

   • If l_k = u_i (positive literal): add arcs (v_i -> a_j) and (a_j -> v_i) creating a 2-cycle that forces v_i and a_j into different partition sets, or alternatively add directed paths that propagate the partition assignment.
   • If l_k = NOT u_i (negated literal): the connection is made to the complementary vertex in the variable gadget.

   The connection structure ensures that if all three literals of a clause are false (i.e., all corresponding variable vertices are on the same side as the clause gadget), the clause gadget together with the connections forms a directed cycle entirely within one partition set, violating the acyclicity constraint.

4. Partition parameter: K = 2.

5. Solution extraction: Given a valid 2-partition (V_1, V_2) where both induced subgraphs are acyclic, read off the truth assignment from which partition set each variable vertex v_i belongs to. The acyclicity constraint on the clause gadgets guarantees that each clause has at least one satisfied literal.

Note: The GJ entry references this as a transformation from 3SAT (or equivalently X3C in some printings). The key insight is that directed cycles of length 3 within each partition set are forbidden, so the partition must "break" every 3-cycle by placing at least one vertex on each side. The clause gadgets are designed so that a clause is satisfied if and only if its 3-cycle can be broken by the partition implied by the truth assignment.

Size Overhead

Symbols:

• n = num_vars of source 3SAT instance (number of variables)
• m = num_clauses of source 3SAT instance (number of clauses)

Target metric (code name)	Polynomial (using symbols above)
num_vertices	3 * num_vars + 3 * num_clauses
num_arcs	3 * num_vars + 3 * num_clauses + 6 * num_clauses

Derivation:

• Vertices: 3 per variable gadget (3-cycle) + 3 per clause gadget (3-cycle) = 3n + 3m
• Arcs: 3 per variable cycle + 3 per clause cycle + 2 connection arcs per literal (3 literals per clause, so 6 per clause) = 3n + 3m + 6m = 3n + 9m

Validation Method

• Closed-loop test: reduce a KSatisfiability instance to AcyclicPartition, solve target with BruteForce (enumerate all 2-partitions, check acyclicity of each induced subgraph), extract truth assignment from partition, verify it satisfies all clauses
• Test with both satisfiable and unsatisfiable 3SAT instances to verify bidirectional correctness
• Verify that for K=2, the constructed graph has a valid acyclic 2-partition iff the 3SAT instance is satisfiable
• Check vertex and arc counts match the overhead formulas

Example

Source instance (KSatisfiability):
3 variables: u_1, u_2, u_3 (n = 3)
2 clauses (m = 2):

• c_1 = (u_1 OR u_2 OR NOT u_3)
• c_2 = (NOT u_1 OR u_2 OR u_3)

Constructed target instance (AcyclicPartition):

Vertices (3n + 3m = 9 + 6 = 15 total):

• Variable gadget for u_1: {v_1, v_1', v_1''} with cycle (v_1 -> v_1' -> v_1'' -> v_1)
• Variable gadget for u_2: {v_2, v_2', v_2''} with cycle (v_2 -> v_2' -> v_2'' -> v_2)
• Variable gadget for u_3: {v_3, v_3', v_3''} with cycle (v_3 -> v_3' -> v_3'' -> v_3)
• Clause gadget for c_1: {a_1, b_1, d_1} with cycle (a_1 -> b_1 -> d_1 -> a_1)
• Clause gadget for c_2: {a_2, b_2, d_2} with cycle (a_2 -> b_2 -> d_2 -> a_2)

Connection arcs (linking literals to clause gadgets):

• c_1 literal u_1 (positive): arcs connecting v_1 to clause-1 gadget
• c_1 literal u_2 (positive): arcs connecting v_2 to clause-1 gadget
• c_1 literal NOT u_3 (negative): arcs connecting v_3' to clause-1 gadget
• c_2 literal NOT u_1 (negative): arcs connecting v_1' to clause-2 gadget
• c_2 literal u_2 (positive): arcs connecting v_2 to clause-2 gadget
• c_2 literal u_3 (positive): arcs connecting v_3 to clause-2 gadget

Partition parameter: K = 2

Solution mapping:

• Satisfying assignment: u_1 = True, u_2 = True, u_3 = True
• Partition V_1 (True side): {v_1, v_2, v_3} plus clause vertices as needed
• Partition V_2 (False side): {v_1', v_1'', v_2', v_2'', v_3', v_3''} plus remaining clause vertices
• Each variable 3-cycle is split across V_1 and V_2, so no complete cycle in either induced subgraph
• Each clause has at least one true literal, so clause gadget cycles are also properly split
• Both induced subgraphs are acyclic

References

• [Garey and Johnson, 1979]: [Garey19xx] M. R. Garey and D. S. Johnson (1979). "Unpublished results".

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	⚠️ Warn	Target problem "AcyclicPartition" does not exist in the codebase; cannot assess path or overhead comparison
Non-trivial	⚠️ Warn	Gadget construction described, but connection arcs are vague and underspecified
Correctness	⚠️ Warn	GJ reference (ND15, p.210) is plausible but could not be independently verified; reduction algorithm itself has correctness concerns
Well-written	❌ Fail	Multiple sections are incomplete or inconsistent; algorithm is not implementable as written

Overall: 0 passed, 3 warnings, 1 failed

---

Usefulness

The target problem "AcyclicPartition" does not exist in the codebase (pred show AcyclicPartition fails). This means:

• No existing path from KSatisfiability to AcyclicPartition exists (novel direction — good).
• However, implementing this rule first requires a [Model] issue for AcyclicPartition. Without the target model, this rule cannot be implemented.

The motivation is reasonable: establishing NP-completeness of Acyclic Partition via 3SAT is a classic complexity-theoretic result. The motivation field is substantive and explains why the reduction matters.

Verdict: Warning — novel reduction direction, but blocked on missing target model.

---

Non-trivial

The reduction describes gadget construction (variable 3-cycles, clause 3-cycles, connection arcs), which would constitute a genuine structural transformation if fully specified. This is not a simple variable substitution or subtype coercion.

However, the connection arcs (Step 3) are critically underspecified:

• The description says "add arcs (v_i -> a_j) and (a_j -> v_i) creating a 2-cycle that forces v_i and a_j into different partition sets, or alternatively add directed paths that propagate the partition assignment." The phrase "or alternatively" indicates the author is unsure of the actual construction.
• The mechanism for how clause satisfaction is enforced is described only in vague terms ("the clause gadget together with the connections forms a directed cycle entirely within one partition set, violating the acyclicity constraint") without specifying precisely which arcs form this cycle.

Verdict: Warning — the gadget idea is non-trivial, but the construction is too vague to fully assess.

---

Correctness

Reference verification:

• Garey & Johnson, 1979 (ND15, p.210): This is a plausible reference. The GJ book's appendix does list problems in the ND (Network Design) section, and the problem statement in the "GJ Source Entry" section is consistent with the GJ format. However, I could not independently verify the specific ND15 designation or page number through web searches. The book itself (garey1979) is already in the project bibliography (docs/paper/references.bib), so the citation is valid.
• The reference states "Transformation from 3SAT" which is consistent with the proposed reduction direction.
• The reference field cites [Garey and Johnson, 1979] as "Unpublished results" — this is suspicious. The GJ book itself is not unpublished; perhaps the reduction proof was unpublished at the time of the book's writing (GJ often listed results as "unpublished" when the proof appeared only in the appendix without a separate publication). This should be clarified.

Algorithm correctness concerns:

1. The connection arc construction (Step 3) is ambiguous. A 2-cycle (v_i -> a_j, a_j -> v_i) does force v_i and a_j into different partition sets (since a 2-cycle is not acyclic), but the issue then needs to explain how this propagation interacts with the clause gadget to enforce clause satisfaction. The current explanation is hand-wavy.
2. The overhead table has an internal inconsistency: the formula says num_arcs = 3 * num_vars + 3 * num_clauses + 6 * num_clauses but the derivation says this equals 3n + 9m, while the table formula says 3 * num_vars + 3 * num_clauses + 6 * num_clauses = 3n + 9m. The table formula should be 3 * num_vars + 9 * num_clauses for consistency.

Verdict: Warning — reference is plausible but not independently verified; algorithm has correctness concerns due to vague connection structure.

---

Well-written

4a: Information Completeness — All template sections are present, but several have substantive issues.

4b: Algorithm Completeness — Fail. The reduction algorithm is NOT a complete, step-by-step procedure:

• Step 3 (Connection arcs) uses "or alternatively" phrasing, indicating two different possible constructions without committing to one. A programmer cannot implement this.
• The connection mechanism for negative literals says "the connection is made to the complementary vertex in the variable gadget" without specifying which complementary vertex or what arcs to add.
• The "Note" paragraph acknowledges uncertainty about the source problem ("or equivalently X3C in some printings").
• The solution extraction (Step 5) says "read off the truth assignment from which partition set each variable vertex v_i belongs to" but doesn't specify which partition set corresponds to True vs False.

4c: Symbol and Notation Consistency — Issues found:

• The overhead table uses num_arcs as a target metric code name, but since AcyclicPartition doesn't exist in the codebase, this cannot be verified against actual getter methods.
• The overhead table formula 3 * num_vars + 3 * num_clauses + 6 * num_clauses doesn't simplify to the claimed value — it should be written as 3 * num_vars + 9 * num_clauses to match the derivation.

4d: Example Quality — The example is partially worked but incomplete:

• Connection arcs are described as "arcs connecting v_1 to clause-1 gadget" without specifying the actual arcs (which endpoints, which direction).
• The solution mapping assigns vertices to partitions but doesn't verify step-by-step that each induced subgraph is actually acyclic.
• The example does not show the full target instance (all arcs are not enumerated).

Verdict: Fail — the algorithm is not implementable as written; connection arcs are underspecified; example is incomplete.

---

Recommendations

1. A [Model] issue for AcyclicPartition is a prerequisite. This rule cannot be implemented without the target problem model. File a [Model] issue first with the formal definition, variable semantics, schema, and complexity bounds.
2. Specify the exact connection arc construction. The reduction algorithm must commit to a single, precise gadget. For each literal in each clause, specify exactly which arcs are added, between which vertices, with which directions. The "or alternatively" must be resolved.
3. Prove the correctness argument explicitly. Show that (a) if the 3SAT instance is satisfiable, the partition breaks all cycles, and (b) if the partition is acyclic, the corresponding truth assignment satisfies all clauses. Both directions need step-by-step reasoning.
4. Fix the overhead table. Use 3 * num_vars + 9 * num_clauses for num_arcs to match the derivation.
5. Complete the example. Enumerate all arcs in the target instance and verify the acyclicity of both induced subgraphs for the given partition.
6. Clarify the reference. The "Unpublished results" citation for Garey and Johnson 1979 is confusing — this is a published book. If the reduction proof itself was unpublished (only appearing in the appendix), state that clearly.

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No existing path from KSatisfiability to AcyclicPartition; novel reduction direction
Non-trivial	⚠️ Warn	Gadget construction described, but connection arcs are ambiguous ("or alternatively")
Correctness	❌ Fail	Critical mismatch between the GJ ND15 problem and the codebase AcyclicPartition model; reference "Unpublished results" is nonsensical
Well-written	❌ Fail	Algorithm is not implementable; connection arcs underspecified; example incomplete; overhead targets wrong model

Overall: 1 passed, 1 warning, 2 failed

Re-check (previous check from 2026-03-11). Changes: Usefulness upgraded from Warn to Pass (AcyclicPartition now exists in codebase). Correctness downgraded from Warn to Fail (model mismatch identified). Well-written remains Fail.

---

Usefulness

Both KSatisfiability and AcyclicPartition exist in the codebase. No reduction path currently exists between them (pred path KSatisfiability AcyclicPartition returns no path). AcyclicPartition currently has zero incoming reduction edges (reduces_from: []), so any valid reduction into it would be valuable for graph connectivity.

The motivation is substantive and explains why the reduction matters (establishing NP-completeness of Acyclic Partition via 3SAT).

Verdict: Pass.

---

Non-trivial

The reduction describes variable 3-cycles, clause 3-cycles, and connection arcs — a genuine gadget construction, not a trivial relabeling or subtype coercion. However, Step 3 (connection arcs) uses "or alternatively" phrasing, indicating the author has not committed to a single construction. This prevents full assessment of whether the gadget actually works.

Verdict: Warn — the gadget idea is non-trivial, but the construction is too vague to fully confirm.

---

Correctness

Critical problem: The issue targets the wrong problem definition.

The GJ ND15 problem described in the issue is:

"Can V be partitioned into K disjoint sets V_1,...,V_K such that the subgraph of G induced by each V_i is acyclic?"

The codebase AcyclicPartition model (src/models/graph/acyclic_partition.rs) is a different problem:

• It requires the quotient graph (the graph where each partition group is contracted to a single node) to be a DAG
• It does not require each induced subgraph within a partition group to be acyclic
• It includes vertex weights, arc costs, a per-group weight bound, and an inter-partition cost bound
• The number of groups is not a fixed parameter K; vertices can be assigned to any of up to num_vertices labels

These are fundamentally different optimization/feasibility problems. A reduction that constructs an instance where "each partition's induced subgraph must be acyclic" will not produce a valid AcyclicPartition instance as defined in the codebase. The codebase model's acyclicity constraint is on the quotient graph, not on the induced subgraphs.

Reference verification:

The GJ reference (ND15, p.210) is plausible — Garey & Johnson (1979) is in the project bibliography (garey1979). However, the specific ND15 designation could not be independently verified through web searches. The References section cites [Garey and Johnson, 1979] as "Unpublished results" — this is incorrect. The GJ book is a published book (W. H. Freeman, 1979, ISBN 0-7167-1045-5). The GJ appendix often marks individual reduction proofs as "unpublished" when no separate paper exists, but the citation format used in the issue is confusing and misleading.

Algorithm correctness concerns (even ignoring the model mismatch):

1. The connection arc construction (Step 3) is ambiguous — a 2-cycle forces vertices into different partition sets, but the mechanism for enforcing clause satisfaction is hand-wavy.
2. The "Note" paragraph acknowledges uncertainty ("or equivalently X3C in some printings"), undermining confidence in the source material.

Verdict: Fail — the reduction targets a different problem than the codebase AcyclicPartition model.

---

Well-written

4a: Information Completeness — All template sections are present, but several have substantive errors.

4b: Algorithm Completeness — Fail.

• Step 3 uses "or alternatively" phrasing — two possible constructions without committing to one. Not implementable.
• Negative literal connections say "the connection is made to the complementary vertex" without specifying which vertex or which arcs.
• Solution extraction (Step 5) does not specify which partition set corresponds to True vs False.

4c: Symbol and Notation Consistency — Fail.

• The overhead table uses num_arcs as a target metric, which matches the codebase size fields. However, the issue's reduction does not construct vertex_weights, arc_costs, weight_bound, or cost_bound — all required fields of the actual AcyclicPartition model. The issue treats AcyclicPartition as if it only has a graph and K parameter.
• The overhead formula 3 * num_vars + 3 * num_clauses + 6 * num_clauses should be simplified to 3 * num_vars + 9 * num_clauses to match the derivation.

4d: Example Quality — Fail.

• Connection arcs are described as "arcs connecting v_1 to clause-1 gadget" without specifying actual endpoints or directions.
• The target instance is not fully constructed — all arcs are not enumerated.
• The solution mapping does not verify step-by-step that each induced subgraph (or quotient graph) is acyclic.
• The example does not construct the required AcyclicPartition fields (vertex_weights, arc_costs, weight_bound, cost_bound).

Verdict: Fail — the algorithm is not implementable; the overhead table and example target the wrong model schema.

---

Recommendations

1. Resolve the model mismatch first. The codebase AcyclicPartition requires an acyclic quotient graph with weight and cost bounds — not "each induced subgraph is acyclic with K groups." Either:
   • (a) Redesign the reduction to target the actual codebase AcyclicPartition model (constructing appropriate vertex_weights, arc_costs, weight_bound, cost_bound), or
   • (b) File a separate [Model] issue for the GJ ND15 problem as a distinct problem (e.g., "AcyclicSubgraphPartition" or "AcyclicInducedPartition") since it has different semantics.
2. Specify the exact connection arc construction. Commit to a single, precise gadget with explicit arc endpoints and directions.
3. Fix the reference citation. Replace "Unpublished results" with the correct citation: Garey, M. R. and Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman.
4. Complete the example. Enumerate all arcs, construct all required target fields, and verify the solution step by step.
5. Fix the overhead table. Include formulas for all target model fields (vertex_weights, arc_costs, weight_bound, cost_bound) — not just num_vertices and num_arcs.