[Rule] 3-SATISFIABILITY to MULTIPLE CHOICE BRANCHING

[isPANN]

---

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

Source: 3SAT
Target: MULTIPLE CHOICE BRANCHING

Motivation: Establishes NP-completeness of MULTIPLE CHOICE BRANCHING via polynomial-time reduction from 3SAT. This reduction encodes Boolean satisfiability as an arc-selection problem on a directed graph, where variable assignments correspond to choosing arcs from partition groups, clause satisfaction is enforced by the branching (acyclicity + in-degree) constraints, and the weight threshold ensures enough clauses are satisfied. The reduction is notable because removing the partition constraint makes the problem polynomial (maximum weight branching via matroid intersection), showing that the multiple-choice constraint is the source of intractability.
Reference: Garey & Johnson, Computers and Intractability, ND11, p.208

GJ Source Entry

[ND11] MULTIPLE CHOICE BRANCHING
INSTANCE: Directed graph G=(V,A), a weight w(a)∈Z^+ for each arc a∈A, a partition of A into disjoint sets A_1,A_2,...,A_m, and a positive integer K.
QUESTION: Is there a subset A'⊆A with ∑_{a∈A'} w(a)≥K such that no two arcs in A' enter the same vertex, A' contains no cycles, and A' contains at most one arc from each of the A_i, 1≤i≤m?
Reference: [Garey and Johnson, ——]. Transformation from 3SAT.
Comment: Remains NP-complete even if G is strongly connected and all weights are equal. If all A_i have |A_i|=1, the problem becomes simply that of finding a "maximum weight branching," a 2-matroid intersection problem that can be solved in polynomial time (e.g., see [Tarjan, 1977]). (In a strongly connected graph, a maximum weight branching can be viewed as a maximum weight directed spanning tree.) Similarly, if the graph is symmetric, the problem becomes equivalent to the "multiple choice spanning tree" problem, another 2-matroid intersection problem that can be solved in polynomial time [Suurballe, 1975].

Reduction Algorithm

Summary:
Given a 3SAT instance with variables x_1, ..., x_n and clauses C_1, ..., C_p (each clause having exactly 3 literals), construct a MULTIPLE CHOICE BRANCHING instance as follows:

1. Variable gadgets: For each variable x_i, create a pair of arcs representing the true and false assignments. These two arcs form a partition group A_i (|A_i| = 2). The "at most one arc from each A_i" constraint forces exactly one truth assignment per variable.

2. Clause gadgets: For each clause C_j = (l_1 OR l_2 OR l_3), create a vertex v_j (clause vertex). For each literal l_k in C_j, add an arc from the corresponding variable gadget vertex to v_j. The in-degree constraint ("no two arcs enter the same vertex") interacts with the variable arc choices.

3. Graph structure: Create a directed graph where:

   • There is a root vertex r.
   • For each variable x_i, there are vertices representing the positive and negative literal states, with arcs from the root to these vertices.
   • Clause vertices receive arcs from literal vertices corresponding to their literals.
   • Additional arcs connect the structure to ensure the branching (acyclicity) property encodes the dependency structure.

4. Weights: Assign weights to arcs such that selecting arcs corresponding to a satisfying assignment yields total weight >= K. Arcs entering clause vertices have weight 1, and K is set to p (the number of clauses), so all clauses must be "reached" by the branching.

5. Partition groups: A_1 through A_n correspond to variable choices (true/false arcs). Additional partition groups may encode auxiliary structural constraints.

Key invariant: The branching structure (acyclic, in-degree at most 1) enforces that the selected arcs form a forest of in-arborescences. Combined with the partition constraint (one arc per variable group), this forces a consistent truth assignment. The weight threshold K = p ensures every clause vertex is reached by at least one literal arc, corresponding to clause satisfaction.

Size Overhead

Symbols:

• n = number of variables in the 3SAT instance
• p = number of clauses (= num_clauses)

Target metric (code name)	Polynomial (using symbols above)
num_vertices	O(n + p) (variable, literal, and clause vertices plus root)
num_arcs	O(n + 3*p) (2 arcs per variable gadget + 3 arcs per clause for literals)
num_partition_groups (m)	n (one group per variable, plus possibly auxiliary groups)
threshold (K)	p (number of clauses)

Derivation: Each variable contributes O(1) vertices and 2 arcs (for true/false). Each clause contributes 1 vertex and 3 incoming arcs (one per literal). The total is linear in the formula size.

Validation Method

• Closed-loop test: reduce a small 3SAT instance to MULTIPLE CHOICE BRANCHING, solve the target with BruteForce (enumerate branching subsets respecting partition constraints), extract the variable assignments from the selected partition group arcs, verify the extracted assignment satisfies all clauses of the original 3SAT formula.
• Negative test: use an unsatisfiable 3SAT formula (e.g., all 8 clauses on 3 variables forming a contradiction), verify the target MCB instance has no branching meeting the weight threshold.
• Structural checks: verify that the constructed graph has the correct number of vertices, arcs, and partition groups; verify arc weights sum correctly.

Example

Source instance (3SAT / KSatisfiability with k=3):
Variables: x_1, x_2, x_3, x_4
Clauses (6 clauses):

• C_1 = (x_1 OR x_2 OR NOT x_3)
• C_2 = (NOT x_1 OR x_3 OR x_4)
• C_3 = (x_2 OR NOT x_3 OR NOT x_4)
• C_4 = (NOT x_1 OR NOT x_2 OR x_4)
• C_5 = (x_1 OR x_3 OR NOT x_4)
• C_6 = (NOT x_2 OR x_3 OR x_4)

Satisfying assignment: x_1 = T, x_2 = T, x_3 = T, x_4 = T

• C_1: x_1=T -> satisfied
• C_2: x_3=T -> satisfied
• C_3: NOT x_4=F, but x_2=T -> satisfied
• C_4: x_4=T -> satisfied
• C_5: x_1=T -> satisfied
• C_6: x_3=T -> satisfied

Constructed target instance (MultipleChoiceBranching):
Directed graph with vertices: root r, literal vertices {p1, n1, p2, n2, p3, n3, p4, n4}, clause vertices {c1, c2, c3, c4, c5, c6}.
Total: 1 + 8 + 6 = 15 vertices.

Arcs (with partition groups):

• Group A_1 (variable x_1): {r -> p1 (w=1), r -> n1 (w=1)} -- choose true or false for x_1
• Group A_2 (variable x_2): {r -> p2 (w=1), r -> n2 (w=1)}
• Group A_3 (variable x_3): {r -> p3 (w=1), r -> n3 (w=1)}
• Group A_4 (variable x_4): {r -> p4 (w=1), r -> n4 (w=1)}

Clause arcs (each in its own singleton group or ungrouped):

• p1 -> c1 (w=1), p2 -> c1 (w=1), n3 -> c1 (w=1) [for C_1]
• n1 -> c2 (w=1), p3 -> c2 (w=1), p4 -> c2 (w=1) [for C_2]
• p2 -> c3 (w=1), n3 -> c3 (w=1), n4 -> c3 (w=1) [for C_3]
• n1 -> c4 (w=1), n2 -> c4 (w=1), p4 -> c4 (w=1) [for C_4]
• p1 -> c5 (w=1), p3 -> c5 (w=1), n4 -> c5 (w=1) [for C_5]
• n2 -> c6 (w=1), p3 -> c6 (w=1), p4 -> c6 (w=1) [for C_6]

K = 6 + 4 = 10 (must select enough arcs to cover all clauses plus variable assignments).

Solution mapping:

• Select variable arcs: r->p1 (x_1=T), r->p2 (x_2=T), r->p3 (x_3=T), r->p4 (x_4=T) from groups A_1 through A_4.
• Select clause arcs (one entering each clause vertex, respecting in-degree 1):
  • p1 -> c1 (C_1 satisfied by x_1)
  • p3 -> c2 (C_2 satisfied by x_3)
  • p2 -> c3 (C_3 satisfied by x_2)
  • p4 -> c4 (C_4 satisfied by x_4)
  • p1 -> c5 (C_5 satisfied by x_1) -- but p1 already used for c1! In-degree constraint on c5 is OK (different vertex), but we need p1 to have out-arcs to both c1 and c5; as long as no two arcs ENTER the same vertex, this is fine. c1 entered by one arc, c5 entered by one arc.
  • p3 -> c6 (C_6 satisfied by x_3)
• Total selected arcs: 4 (variable) + 6 (clause) = 10 = K
• Branching check: root r has outgoing arcs to p1, p2, p3, p4; then p1->c1, p1->c5; p2->c3; p3->c2, p3->c6; p4->c4. This forms a forest rooted at r. No cycles. Each clause vertex has in-degree 1.
• Answer: YES

References

• [Garey and Johnson, ——]: (not found in bibliography)
• [Tarjan, 1977]: [Tarjan1977] Robert E. Tarjan (1977). "Finding optimum branchings". Networks 7, pp. 25–35.
• [Suurballe, 1975]: [Suurballe1975] James W. Suurballe (1975). "Minimal spanning trees subject to disjoint arc set constraints".

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Target problem not in codebase; no existing path from KSatisfiability to MultipleChoiceBranching
Non-trivial	⚠️ Warn	Gadget construction described, but algorithm is too vague to confirm structural transformation
Correctness	⚠️ Warn	Garey & Johnson ND11 reference is plausible but cannot be independently verified; Suurballe 1975 reference not found
Well-written	❌ Fail	Algorithm is a high-level sketch, not an implementable procedure; overhead uses O-notation instead of exact expressions; example has structural concerns

Overall: 1 passed, 2 warnings, 1 failed

---

Usefulness

Pass. The target problem "MULTIPLE CHOICE BRANCHING" does not exist in the codebase (pred show fails for it, and it does not appear in pred list). There is no existing reduction path from KSatisfiability (3SAT) to this target. This would be a novel reduction adding a new node to the reduction graph.

Note: Since the target model does not exist in the codebase (target_in_codebase: false as stated in the issue metadata), implementing this rule also requires implementing the MultipleChoiceBranching model first.

---

Non-trivial

Warn. The described reduction involves variable gadgets (partition groups encoding true/false assignments), clause gadgets (clause vertices with incoming literal arcs), and structural constraints (branching = acyclic + in-degree-1) to enforce satisfiability. This is characteristic of a genuine structural transformation, not a trivial relabeling or subtype coercion.

However, the algorithm description is marked with "AI-generated summary" warnings and contains vague language like "Additional arcs connect the structure to ensure the branching property encodes the dependency structure" (Step 3) and "Additional partition groups may encode auxiliary structural constraints" (Step 5). These hedges make it impossible to confirm that the construction is fully non-trivial versus partially hand-waved. Upgrading to Pass requires a precise, complete algorithm.

---

Correctness

Warn. Reference verification results:

• Garey & Johnson, ND11, p.208: The book "Computers and Intractability" (1979) is a well-known reference already in the project bibliography (garey1979 in references.bib). The ND (Network Design) category and page 208 are consistent with the book's appendix structure. The problem description (directed graph, arc weights, partition of arcs, branching constraints) is consistent with the style and content of Garey & Johnson's problem catalog. However, the specific ND11 entry could not be independently verified online since the book's appendix is not freely available. The issue itself quotes the GJ entry verbatim, which appears authentic in style.

• Tarjan, 1977: Verified. "Finding optimum branchings" by Robert E. Tarjan was published in Networks, Volume 7, pages 25-35, 1977. This paper presents an O(m log n) algorithm for maximum weight branching, confirming the comment that without partition constraints the problem is polynomial.

• Suurballe, 1975: Not found as cited. The issue cites Suurballe (1975) for "Minimal spanning trees subject to disjoint arc set constraints." However, Suurballe's known 1974 publication is "Disjoint paths in a network" in Networks 4:125-145. A 1975 publication with the cited title could not be located through web search or Semantic Scholar. This may be an obscure technical report or the year/title may be slightly off.

• "[Garey and Johnson, ——]": The GJ source entry references "[Garey and Johnson, ——]" for the reduction from 3SAT. The dashes suggest an unpublished/internal result. This is consistent with GJ's style for self-referential proofs, but it means the reduction construction itself is not from a published, verifiable source — it is attributed to the book authors without a separate paper.

The reduction algorithm's correctness cannot be fully verified because the algorithm itself is incomplete (see Well-written section).

---

Well-written

Fail. Multiple issues found:

4a: Information Completeness

All template sections are present, but nearly every section carries an "AI-generated / unverified" warning, which is a red flag for quality.

4b: Algorithm Completeness — FAIL

The reduction algorithm is a high-level sketch, not an implementable step-by-step procedure:

1. Step 3 is vague: "Additional arcs connect the structure to ensure the branching (acyclicity) property encodes the dependency structure" — this is a hand-wave, not a construction. A programmer cannot implement this without knowing exactly which arcs to add.

2. Step 5 is vague: "Additional partition groups may encode auxiliary structural constraints" — the word "may" is unacceptable in a reduction algorithm. Either there are additional partition groups or there are not. If there are, they must be specified exactly.

3. No solution extraction procedure: The algorithm describes how to construct the target instance but does not give an explicit, step-by-step procedure for extracting a satisfying assignment from a valid branching. The "Key invariant" paragraph gives intuition but not a procedure.

4. Missing vertex/arc definitions: The algorithm says "vertices representing the positive and negative literal states" but does not define them precisely. How many vertices per variable? The text seems to suggest 2 literal vertices per variable plus arcs from root, but this is not stated unambiguously.

4c: Symbol and Notation Consistency — FAIL

• The overhead table uses O(n + p) and O(n + 3*p) — O-notation is not acceptable for overhead expressions. The codebase requires exact symbolic expressions (e.g., "n + p + 1", "2 * n + 3 * p"), not asymptotic bounds. These need to be exact polynomial expressions using variable names that match getter methods on the target problem.
• The target problem does not exist, so the code metric names (num_vertices, num_arcs, num_partition_groups, threshold) cannot be validated against size_fields. This is expected given target_in_codebase: false, but the overhead expressions still need to be exact.
• The symbol n is defined as "number of variables" and p as "number of clauses", but the expressions mix these with unquantified constants ("+1" for root, etc.) while hiding them inside O-notation.

4d: Example Quality — WARN

The example is non-trivial (4 variables, 6 clauses) and provides a fully worked construction showing source instance, target graph, and solution mapping. However:

• The threshold K is stated as 6 + 4 = 10, but the algorithm says K = p (number of clauses = 6). This is a contradiction — the example invents a different K formula (p + n) without justification.
• The example notes that p1 is used as a source for arcs to both c1 and c5, commenting "this is fine" because they enter different vertices. While the in-degree constraint is satisfied for the clause vertices, this needs more careful analysis: in the branching, the arcs selected must form a forest. Having p1 -> c1 and p1 -> c5 both selected means p1 has out-degree 2 in the selected arc set, which is allowed in a branching (branchings constrain in-degree, not out-degree). This is correct but should be stated more clearly.

---

Recommendations

1. The reduction algorithm must be completely rewritten with explicit, numbered steps that a programmer could implement directly. Each vertex, arc, weight, and partition group must be defined precisely. No "may" or "additional structure" hand-waves.
2. Replace O-notation in the overhead table with exact expressions (e.g., n + p + 1 for vertices, 2 * n + 3 * p for arcs).
3. Resolve the K threshold contradiction: either K = p (as stated in the algorithm) or K = n + p (as used in the example). Justify the choice.
4. Add explicit solution extraction: given a valid branching A' with weight >= K, describe exactly how to read off the variable assignments (likely: for each group A_i, if arc r->p_i is selected then x_i = true, else x_i = false).
5. Verify the Suurballe reference: the 1975 citation could not be found. Provide a DOI or correct the year/title.
6. Consider whether this rule requires the target model to be implemented first. Since MultipleChoiceBranching is not in the codebase, a [Model] issue for it should precede or accompany this rule issue.

[zazabap]

Issue Quality Check — Rule

Re-check (previous check posted 2026-03-11; 2 warnings, 1 failure). MultipleChoiceBranching model now exists in the codebase.

Check	Result	Details
Usefulness	✅ Pass	No existing path from KSatisfiability to MultipleChoiceBranching; novel edge in reduction graph
Non-trivial	⚠️ Warn	Gadget construction described, but algorithm is too vague to confirm full structural transformation
Correctness	⚠️ Warn	Garey & Johnson ND11 reference plausible but reduction itself is an unpublished "[Garey and Johnson, ——]" self-citation; Suurballe 1975 not found
Well-written	❌ Fail	Algorithm is a high-level sketch, not implementable; overhead uses O-notation instead of exact expressions; K threshold contradictory; missing solution extraction

Overall: 1 passed, 2 warnings, 1 failed

---

Usefulness

Pass. The target problem MultipleChoiceBranching now exists in the codebase (previously it did not), with size getters num_vertices, num_arcs, and num_partition_groups. However, it currently has zero incoming and zero outgoing reductions (reduces_from: [], reduces_to: []). There is no existing path from KSatisfiability to MultipleChoiceBranching:

pred path KSatisfiability MultipleChoiceBranching
→ Error: No reduction path

This would be a novel reduction, adding a first connection to an otherwise orphaned node. This is clearly useful.

The Motivation section is substantive — it explains that removing the partition constraint makes the problem polynomial (via matroid intersection), showing the partition constraint is the source of intractability. This is a well-motivated reduction.

---

Non-trivial

Warn. The described reduction involves variable gadgets (partition groups encoding true/false assignments), clause gadgets (clause vertices with incoming literal arcs), and structural constraints (branching = acyclic + in-degree ≤ 1) to enforce satisfiability. This is characteristic of a genuine structural transformation, not a trivial relabeling.

However, the algorithm contains vague language that prevents full confirmation:

• Step 3: "Additional arcs connect the structure to ensure the branching property encodes the dependency structure" — hand-wave, not a construction.
• Step 5: "Additional partition groups may encode auxiliary structural constraints" — the word "may" is unacceptable.

Until the algorithm is made precise, the non-triviality of the specific construction cannot be fully confirmed, even though the type of reduction (3SAT to a network design problem) is inherently non-trivial.

---

Correctness

Warn. Reference verification results:

• Garey & Johnson, Computers and Intractability, ND11, p.208: The book garey1979 is in the project bibliography. The ND (Network Design) category and the problem description (directed graph, arc weights, partition of arcs, branching constraints, weight threshold) are consistent with GJ's appendix style. However, the GJ source entry itself cites the reduction as "[Garey and Johnson, ——]" — meaning this is an unpublished, self-referential proof. There is no separate published paper describing this reduction. The OWU NP-Completeness Project (npcomplete.owu.edu) tags this problem as "uncited reduction" and "No G&J reference," corroborating that no independent published proof exists. This means the reduction algorithm in this issue is necessarily reconstructed, not taken from a verified published source.

• Tarjan, 1977: Verified. "Finding optimum branchings" by Robert E. Tarjan, Networks 7(1), pp. 25–35, 1977. Confirmed via Wiley Online Library. The claim that maximum weight branching (without partition constraints) is polynomial is correct.

• Suurballe, 1975: Not found as cited. The issue cites Suurballe (1975) for "Minimal spanning trees subject to disjoint arc set constraints." Suurballe's known publications are "Disjoint paths in a network" (Networks 4:125–145, 1974) and a 1984 paper with Tarjan. No 1975 publication with the cited title was found via web search or Semantic Scholar. This may be an obscure technical report, or the year/title may be incorrect.

• Reduction correctness: Since the algorithm is a high-level sketch (see Well-written section), correctness of the specific construction cannot be verified. The claim that 3SAT reduces to Multiple Choice Branching is consistent with GJ, but the specific construction in this issue is unverified.

---

Well-written

Fail. Multiple issues found:

4a: Information Completeness

All template sections are present, but nearly every section carries an "⚠️ Unverified: AI-generated" warning. The content reads as LLM-generated without human verification.

4b: Algorithm Completeness — FAIL

The reduction algorithm is a high-level sketch, not an implementable procedure:

1. Step 3 is vague: "Additional arcs connect the structure to ensure the branching (acyclicity) property encodes the dependency structure" — a programmer cannot implement this.
2. Step 5 is vague: "Additional partition groups may encode auxiliary structural constraints" — either they exist or they do not.
3. No solution extraction procedure: The algorithm describes forward construction but gives no explicit steps for extracting a satisfying assignment from a valid branching.
4. Missing precise vertex/arc definitions: The text says "vertices representing the positive and negative literal states" without fully specifying the graph topology.

4c: Symbol and Notation Consistency — FAIL

• The overhead table uses O-notation (O(n + p), O(n + 3*p)). The codebase requires exact expressions matching getter methods (e.g., "num_vars + num_clauses + 1" for num_vertices). The target model has getters num_vertices, num_arcs, num_partition_groups.
• The symbol n = "number of variables" and p = "number of clauses" need to map to source getter names (num_vars, num_clauses).
• Constants hidden inside O-notation (+1 for root vertex, etc.) must be made explicit.

4d: Example Quality — WARN

The example (4 variables, 6 clauses) is non-trivial and shows a fully worked construction. However:

• K threshold contradiction: The algorithm states K = p (= 6), but the example uses K = 6 + 4 = 10 (= p + n). These are inconsistent — one must be wrong.
• Branching validity: The example selects arcs p1→c1 and p1→c5 from the same source vertex. While this is valid in a branching (in-degree constraint, not out-degree), the analysis should be clearer about why this forms a valid in-arborescence.
• The example has enough structure for round-trip testing (multiple feasible assignments exist for this formula), which is good.

---

Recommendations

1. Rewrite the reduction algorithm completely with explicit, numbered steps. Every vertex, arc, weight, and partition group must be defined precisely. No "may" or "additional structure" hand-waves.
2. Replace O-notation in the overhead table with exact expressions using source getter names: e.g., num_vertices = "num_vars * 2 + num_clauses + 1", num_arcs = "num_vars * 2 + 3 * num_clauses", num_partition_groups = "num_vars".
3. Resolve the K threshold contradiction: clarify whether K = p or K = n + p, and make algorithm and example consistent.
4. Add explicit solution extraction: given a valid branching A' with weight ≥ K, describe exactly how to extract variable assignments.
5. Fix the Suurballe reference: provide a DOI or correct the year/title (Suurballe 1974 in Networks 4 is the verified publication).
6. Acknowledge the unpublished nature of the reduction: since GJ cite "[Garey and Johnson, ——]", note that this is a reconstruction, not a transcription of a published proof.