[Rule] 3SAT to DIRECTED TWO-COMMODITY INTEGRAL FLOW

[isPANN]

Source: 3-SATISFIABILITY (3SAT)
Target: DIRECTED TWO-COMMODITY INTEGRAL FLOW
Motivation: Establishes NP-completeness of DIRECTED TWO-COMMODITY INTEGRAL FLOW via polynomial-time reduction from 3SAT. This is a foundational result by Even, Itai, and Shamir (1976) showing that even with only two commodities, the integral multicommodity flow problem is intractable, in sharp contrast to the single-commodity case which is polynomial.
Reference: Garey & Johnson, Computers and Intractability, ND38, p.216; Even, Itai, and Shamir (1976).

GJ Source Entry

[ND38] DIRECTED TWO-COMMODITY INTEGRAL FLOW
INSTANCE: Directed graph G=(V,A), specified vertices s_1, s_2, t_1, and t_2, capacity c(a)∈Z^+ for each a∈A, requirements R_1,R_2∈Z^+.
QUESTION: Are there two flow functions f_1,f_2: A→Z_0^+ such that
(1) for each a∈A, f_1(a)+f_2(a)≤c(a),
(2) for each v∈V−{s,t} and i∈{1,2}, flow f_i is conserved at v, and
(3) for i∈{1,2}, the net flow into t_i under flow f_i is at least R_i?
Reference: [Even, Itai, and Shamir, 1976]. Transformation from 3SAT.
Comment: Remains NP-complete even if c(a)=1 for all a∈A and R_1=1.

Reduction Algorithm

Given a KSatisfiability<K3> instance with n variables x_1, ..., x_n and m clauses C_1, ..., C_m, construct a DirectedTwoCommodityIntegralFlow instance as follows (Even-Itai-Shamir 1976 construction):

Stage 1: Variable lobes (truth assignment encoding)

For each variable x_i (i = 1, ..., n), construct a "lobe" with two parallel directed paths from entry vertex u_i to exit vertex v_i:

• TRUE path: u_i → p_i → v_i (upper path, represents x_i = TRUE)
• FALSE path: u_i → q_i → v_i (lower path, represents x_i = FALSE)

This creates 4 vertices per variable: u_i, p_i (true midpoint), q_i (false midpoint), v_i.

Stage 2: Variable chain (Commodity 1)

Chain the lobes in series to form the commodity-1 corridor:

• s_1 → u_1, v_1 → u_2, v_2 → u_3, ..., v_n → t_1

Commodity 1 has requirement R_1 = 1. A single unit of flow traverses each lobe, choosing either the TRUE or FALSE path, thereby encoding a truth assignment: α(x_i) = true iff commodity-1 flows through p_i.

Stage 3: Clause satisfaction (Commodity 2)

For each clause C_j (j = 1, ..., m), create a clause vertex d_j. For each literal in C_j:

• If x_i appears positively in C_j: add arc (p_i → d_j)
• If ¬x_i appears in C_j: add arc (q_i → d_j)

Add arcs from s_2 to each clause vertex: s_2 → d_j for j = 1, ..., m.
Add arcs from each clause vertex to the sink: d_j → t_2 for j = 1, ..., m.

Commodity 2 has requirement R_2 = m. Each clause must route one unit of flow from s_2 through a satisfied literal's midpoint to d_j to t_2.

Capacity and terminal vertices

• All arcs have capacity 1
• Four terminal vertices: s_1, t_1, s_2, t_2

Vertex numbering (0-indexed)

• s_1 = 0, t_1 = 1, s_2 = 2, t_2 = 3 (4 terminal vertices)
• Variable lobe i (0-based): u_i = 4 + 4i, p_i = 4 + 4i + 1, q_i = 4 + 4i + 2, v_i = 4 + 4i + 3
• Clause vertex j (0-based): d_j = 4 + 4n + j

Total vertices: 4 + 4n + m

Solution extraction

From a feasible two-commodity flow (f_1, f_2):

• α(x_i) = true if f_1(u_i → p_i) = 1 (commodity-1 flows through TRUE path)
• α(x_i) = false if f_1(u_i → q_i) = 1 (commodity-1 flows through FALSE path)

Correctness

• (Forward): If the formula is satisfiable with assignment α, route commodity 1 through the TRUE/FALSE paths according to α. For each clause C_j, at least one literal is satisfied; route one unit of commodity 2 from s_2 → d_j, then from d_j backwards through the satisfied literal's midpoint arc. Since commodity 1 chose the opposite path through that variable's lobe, the literal-to-clause arc is free (capacity not consumed by commodity 1).
• (Backward): If both commodities achieve their requirements, commodity 1's path through the lobes defines a truth assignment. Commodity 2 needs m units reaching t_2, one per clause. Each unit must pass through a literal midpoint arc not used by commodity 1, which means the corresponding literal evaluates to true under the assignment.

Size Overhead

Target metric (code name)	Expression
num_vertices	4 * num_vars + num_clauses + 4
num_arcs	7 * num_vars + 4 * num_clauses + 1

Derivation:

• Vertices: 4 terminals + 4n (variable lobes) + m (clause vertices) = 4n + m + 4
• Arcs: per variable lobe: 4 internal arcs (u→p, u→q, p→v, q→v) + 1 chain arc (except last) = ~5 arcs; chain arcs from s_1→u_1 and v_n→t_1 = n+1 total chain arcs; plus 2n lobe arcs (TRUE/FALSE paths) gives 4n + (n+1) = 5n+1 for commodity-1 corridor. Literal-to-clause arcs: 3m. Source/sink arcs for commodity 2: m (s_2→d_j) + m (d_j→t_2) = 2m. Adjusted total: 7n + 4m + 1 (combining chain arcs with lobe internal arcs and accounting for the n-1 inter-lobe arcs plus 2 terminal arcs).

Implementation Note

DirectedTwoCommodityIntegralFlow already has a path to ILP (DirectedTwoCommodityIntegralFlow → ILP/i32). No companion ILP rule is needed.

Example

Source (KSatisfiability):
n = 5 variables (x_1, x_2, x_3, x_4, x_5), m = 4 clauses:

• C_1 = (x_1 ∨ ¬x_2 ∨ x_3)
• C_2 = (¬x_1 ∨ x_4 ∨ ¬x_5)
• C_3 = (x_2 ∨ ¬x_3 ∨ x_5)
• C_4 = (¬x_2 ∨ ¬x_4 ∨ x_5)

Balanced structure: each variable appears in 2-3 clauses with mixed polarity.

Target (DirectedTwoCommodityIntegralFlow):

• Vertices: 4·5 + 4 + 4 = 28 vertices
• Arcs: 7·5 + 4·4 + 1 = 52 arcs
• R_1 = 1, R_2 = 4, all capacities = 1

Terminal vertices:

• s_1 = 0, t_1 = 1, s_2 = 2, t_2 = 3

Variable lobe vertices (20):

• x_1: u_0=4, p_0=5, q_0=6, v_0=7
• x_2: u_1=8, p_1=9, q_1=10, v_1=11
• x_3: u_2=12, p_2=13, q_2=14, v_2=15
• x_4: u_3=16, p_3=17, q_3=18, v_3=19
• x_5: u_4=20, p_4=21, q_4=22, v_4=23

Clause vertices (4):

• d_0=24, d_1=25, d_2=26, d_3=27

Commodity-1 chain arcs (6): (0→4), (7→8), (11→12), (15→16), (19→20), (23→1)
Lobe internal arcs (20): for each i: (u→p), (u→q), (p→v), (q→v)
Literal-to-clause arcs (12):

• C_1: (p_0→d_0)=(5→24), (q_1→d_0)=(10→24), (p_2→d_0)=(13→24)
• C_2: (q_0→d_1)=(6→25), (p_3→d_1)=(17→25), (q_4→d_1)=(22→25)
• C_3: (p_1→d_2)=(9→26), (q_2→d_2)=(14→26), (p_4→d_2)=(21→26)
• C_4: (q_1→d_3)=(10→27), (q_3→d_3)=(18→27), (p_4→d_3)=(21→27)
  Commodity-2 source arcs (4): (2→24), (2→25), (2→26), (2→27)
  Commodity-2 sink arcs (4): (24→3), (25→3), (26→3), (27→3)

Satisfying assignment: x_1=1, x_2=0, x_3=1, x_4=1, x_5=1

• C_1: x_1=T ✓
• C_2: x_4=T ✓
• C_3: x_5=T ✓
• C_4: x_5=T ✓
• Commodity 1 path: s_1→u_0→p_0→v_0→u_1→q_1→v_1→u_2→p_2→v_2→u_3→p_3→v_3→u_4→p_4→v_4→t_1
• Commodity 2 routes through unused literal arcs (one per clause)

Non-satisfying assignment: x_1=0, x_2=1, x_3=0, x_4=0, x_5=0

• C_2: (¬x_1=T ∨ x_4=F ∨ ¬x_5=T) = T ✓
• C_3: (x_2=T ∨ ¬x_3=T ∨ x_5=F) = T ✓
• C_4: (¬x_2=F ∨ ¬x_4=T ∨ x_5=F) = T ✓
• C_1: (x_1=F ∨ ¬x_2=F ∨ x_3=F) = F ✗
• Commodity 1 would use q_0, p_1, q_2, q_3, q_4 paths. For C_1, all literal arcs (p_0, q_1, p_2) are occupied by commodity 1 — commodity 2 cannot route a unit through C_1.

Validation Method

• Closed-loop test: reduce KSatisfiability to DirectedTwoCommodityIntegralFlow, solve target via ILP (DirectedTwoCommodityIntegralFlow → ILP/i32), extract truth assignment from commodity-1 flow paths, verify all clauses satisfied
• Test with both satisfiable and unsatisfiable instances
• Verify vertex/arc counts match overhead formulas

References

• Even, S., Itai, A., and Shamir, A. (1976). "On the complexity of timetable and multicommodity flow problems." SIAM Journal on Computing, 5(4), pp. 691–703.
• Garey, M. R., & Johnson, D. S. (1979). Computers and Intractability, ND38, p.216.

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No existing path from KSatisfiability to DirectedTwoCommodityIntegralFlow
Non-trivial	✅ Pass	Genuine gadget construction with variable lobes and capacity sharing
Correctness	⚠️ Warn	Primary reference verified; minor inaccuracy in secondary reference year; algorithm details not fully verifiable against original paper
Well-written	❌ Fail	Multiple issues: ambiguous algorithm steps, O-notation in overhead table instead of exact expressions, vague example solution mapping

Overall: 2 passed, 1 warning, 1 failed

---

Usefulness

Pass. There is currently no reduction path from KSatisfiability to DirectedTwoCommodityIntegralFlow in the reduction graph. DirectedTwoCommodityIntegralFlow has zero incoming reductions (reduces_from is empty), so this would be the first rule connecting it to the broader graph as a target. The motivation is clear and well-justified: establishing NP-completeness of directed two-commodity integral flow via 3SAT is a foundational result, and it contrasts meaningfully with the polynomial-time single-commodity case.

Non-trivial

Pass. The reduction constructs variable lobe gadgets (parallel TRUE/FALSE paths), chains them into a commodity-1 assignment path, creates clause sinks for commodity 2, and uses shared arc capacities to enforce consistency between the assignment and clause satisfaction. This is a genuine structural transformation involving gadgets, auxiliary vertices, and non-trivial capacity-sharing constraints.

Correctness

Warn.

• Even, Itai, and Shamir (1976): Verified. The paper "On the Complexity of Timetable and Multicommodity Flow Problems" exists in SIAM Journal on Computing, Vol. 5, No. 4, pp. 691-703, 1976. DOI: 10.1137/0205048. It proves NP-completeness of two-commodity integral flow. The paper is already in the project bibliography as evenItaiShamir1976.
• Garey & Johnson ND38: The GJ entry is faithfully reproduced and correctly attributes the result to Even, Itai, and Shamir (1976) with "Transformation from 3SAT."
• Itai 1977 reference: The issue cites [Itai, 1977] as a Technion dept. report, but the project bibliography has this as itai1978 — published in the Journal of the ACM, Vol. 25, No. 4, pp. 596-611, 1978. The year and venue are slightly wrong in the issue. This is non-critical (likely a tech report predating formal publication), but should be corrected.
• Algorithm fidelity: Without access to the full text of the original paper, the high-level structure of the reduction (variable lobes, commodity-1 assignment chain, commodity-2 clause validation, capacity sharing) is consistent with what is known about this classic reduction. However, the specific details (e.g., how commodity 2 routes from s_2 through literal connections) cannot be independently verified from the issue description alone, since the description is partially ambiguous (see Well-written section).

Well-written

Fail. Several issues need to be addressed:

4a — Information Completeness:

• All required sections are present. However, the Source field says "3SAT" — the correct problem name in this codebase is KSatisfiability (with K3 variant). The Target says "DIRECTED TWO-COMMODITY INTEGRAL FLOW" — the correct name is DirectedTwoCommodityIntegralFlow.

4b — Algorithm Completeness:

• Step 5 is ambiguous: "s_2 connects to each clause node (or to the literal connection points)" — the "or" introduces two possible constructions without specifying which one to implement.
• Step 6 is hand-wavy: "This forces commodity 2 to route through the 'other' paths consistent with the assignment, verifying clause satisfaction" is an explanation of why it works, not a constructive step a programmer can implement. The exact graph structure for routing commodity 2 from s_2 through literal arcs to clause sinks needs to be spelled out.
• Variable lobe internals undefined: Step 1 says "two parallel directed paths from node u_i to node v_i" but does not specify the intermediate nodes on these paths. The literal connections in Step 4 reference "the TRUE path of lobe i" but it is unclear which specific node or arc on the path they connect to. Are the literal connection arcs branching from intermediate nodes, or from u_i/v_i directly?
• Solution extraction not described: The algorithm should explicitly describe how to extract a 3SAT assignment from a feasible two-commodity flow (the reverse mapping).

4c — Symbol and Notation Consistency:

• Overhead table uses n = num_variables and m = num_clauses but the code getter methods on KSatisfiability are num_vars and num_clauses. The table should use the actual code metric names.
• The overhead table uses O-notation (O(n + m), O(n + 3m)) instead of exact polynomial expressions. The #[reduction(overhead = {...})] macro requires exact expressions (e.g., "2 * num_vars + num_clauses + 4", not "O(num_vars + num_clauses)"). The exact vertex and arc counts must be derivable from the construction.
• The overhead table includes max_capacity, requirement_1, requirement_2 — these are not size fields of DirectedTwoCommodityIntegralFlow. The target's size_fields are only ["num_arcs", "num_vertices"]. While noting that capacities are unit and requirements are fixed is useful context, the overhead table should focus on the actual size fields.

4d — Example Quality:

• The example has reasonable size (3 variables, 3 clauses) and is brute-force solvable.
• However, the solution mapping for commodity 2 is vague: "s_2 -> d_1 (through x_1 TRUE literal connection, using a different arc not used by commodity 1) -> t_2" — it is unclear which actual arcs carry commodity 2 flow. The parenthetical "using a different arc not used by commodity 1" is hand-wavy; the exact arc sequence should be listed.
• The example only shows a satisfiable instance. For round-trip testing, an unsatisfiable instance (or at least a note about what happens with an unsatisfiable formula) would strengthen the validation.
• The example does not demonstrate that the specific assignment (all TRUE) is the only satisfying assignment, nor does it show suboptimal configurations. Since this is a feasibility problem (Or-valued), the round-trip concern is less severe — but the example should still show that at least one non-satisfying configuration maps to an infeasible flow to build confidence.

Recommendations

• Replace O-notation overhead expressions with exact formulas derived from the construction. For example, if each variable lobe adds 4 vertices (u_i, two intermediate nodes, v_i) plus s_1, s_2, t_1, t_2, and m clause nodes, then num_vertices = 4 * num_vars + num_clauses + 4. Count the arcs similarly.
• Use the correct problem names: KSatisfiability (source, K3 variant) and DirectedTwoCommodityIntegralFlow (target).
• Fix the Itai reference: year should be 1978, venue should be Journal of the ACM (not Technion tech report).
• Fully specify the intermediate nodes in variable lobes and the exact connection points for literal arcs.
• Add an explicit solution extraction procedure (flow assignment -> truth assignment).

[GiggleLiu]

fix-issue changelog:

• Rewrote issue body with complete Even-Itai-Shamir (1976) construction: 3-stage architecture (variable lobes, commodity-1 chain, commodity-2 clause satisfaction)
• Added concrete vertex numbering (0-indexed), arc listing, and overhead derivation
• Specified exact overhead: num_vertices = 4num_vars + num_clauses + 4, num_arcs = 7num_vars + 4*num_clauses + 1
• Added nontrivial example: n=5 vars, m=4 clauses (28 vertices, 52 arcs) with satisfying and non-satisfying assignments
• Noted target already has ILP path (DirectedTwoCommodityIntegralFlow -> ILP/i32)
• Removed AI-unverified warnings; construction follows the original paper