[Rule] 3SAT to PATH CONSTRAINED NETWORK FLOW

[isPANN]

Source: 3SAT
Target: PATH CONSTRAINED NETWORK FLOW
Motivation: Establishes NP-completeness of PATH CONSTRAINED NETWORK FLOW via polynomial-time reduction from 3SAT. This result is notable because standard (unconstrained) network flow is polynomial, but restricting flow to travel along specified paths makes the problem NP-complete, even when all capacities equal 1.

Reference: Garey & Johnson, Computers and Intractability, ND34, p.215

GJ Source Entry

[ND34] PATH CONSTRAINED NETWORK FLOW
INSTANCE: Directed graph G=(V,A), specified vertices s and t, a capacity c(a)∈Z^+ for each a∈A, a collection P of directed paths in G, and a requirement R∈Z^+.
QUESTION: Is there a function g: P->Z_0^+ such that if f: A->Z_0^+ is the flow function defined by f(a)=Sum_{p∈P(a)} g(p), where P(a)⊆P is the set of all paths in P containing the arc a, then f is such that
(1) f(a)<=c(a) for all a∈A,
(2) for each v∈V-{s,t}, flow is conserved at v, and
(3) the net flow into t is at least R?
Reference: [Promel, 1978]. Transformation from 3SAT.
Comment: Remains NP-complete even if all c(a)=1. The corresponding problem with non-integral flows is equivalent to LINEAR PROGRAMMING, but the question of whether the best rational flow fails to exceed the best integral flow is NP-complete.

Reduction Algorithm

Summary:
Given a 3SAT instance with n variables x_1, ..., x_n and m clauses C_1, ..., C_m, construct a PATH CONSTRAINED NETWORK FLOW instance as follows:

1. Variable gadgets: For each variable x_i, create a "variable arc" e_i in the graph. Create two paths: p_{x_i} (representing x_i = true) and p_{~x_i} (representing x_i = false). Both paths traverse arc e_i, ensuring that at most one of them can carry flow (since arc e_i has capacity 1).

2. Clause gadgets: For each clause C_j (containing three literals l_{j,1}, l_{j,2}, l_{j,3}), create a "clause arc" e_{n+j}. Also create three arcs c_{j,1}, c_{j,2}, c_{j,3}, one for each literal position in the clause. Create three paths p~_{j,1}, p~_{j,2}, p~_{j,3} where p~_{j,k} traverses both arc e_{n+j} and arc c_{j,k}.

3. Linking literals to variables: Arc c_{j,k} is also traversed by the variable path p_{x_i} (or p_{~x_i}) if literal l_{j,k} is x_i (or x_i, respectively). This creates a conflict: if variable x_i is set to true (p_{x_i} carries flow), then the clause path p_{j,k} corresponding to literal ~x_i cannot carry flow through the shared arc.

4. Capacities: Set all arc capacities to 1.

5. Requirement: Set R such that we need flow from all variable gadgets (n units for variable selection) plus at least one satisfied literal per clause (m units from clause satisfaction), giving R = n + m.

6. Correctness (forward): A satisfying assignment selects one path per variable (n units of flow). For each clause, at least one literal is true, so the corresponding clause path can carry flow without conflicting with the variable paths. Total flow >= n + m = R.

7. Correctness (reverse): If a feasible flow achieving R = n + m exists, the variable arcs force exactly one truth value per variable (binary choice), and the clause arcs force each clause to have at least one satisfied literal.

Key invariant: Shared arcs between variable paths and clause paths enforce consistency between variable assignments and clause satisfaction. Unit capacities enforce binary choices.

Time complexity of reduction: O(n + m) for graph construction (polynomial in the 3SAT formula size).

Size Overhead

Symbols:

• n = number of variables in 3SAT instance
• m = number of clauses in 3SAT instance

Target metric (code name)	Polynomial (using symbols above)
num_vertices	O(n + m)
num_arcs	n + m + 3 * m = n + 4 * m
num_paths	2 * n + 3 * m
requirement (R)	n + m

Derivation: The graph has O(n + m) vertices. There are n variable arcs, m clause arcs, and 3m literal arcs, for n + 4m arcs total. The path collection has 2n variable paths and 3m clause-literal paths. All capacities are 1.

Validation Method

• Closed-loop test: reduce a 3SAT instance to PathConstrainedNetworkFlow, solve target with BruteForce (enumerate path flow assignments), extract solution, verify on source
• Test with known YES instance: a satisfiable 3SAT formula
• Test with known NO instance: an unsatisfiable 3SAT formula (e.g., a small unsatisfiable core)
• Compare with known results from literature

Example

Source instance (3SAT):
Variables: x_1, x_2, x_3, x_4
Clauses (m = 4):

• C_1 = (x_1 v x_2 v ~x_3)
• C_2 = (~x_1 v x_3 v x_4)
• C_3 = (x_2 v ~x_3 v ~x_4)
• C_4 = (~x_1 v ~x_2 v x_4)

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

• C_1: x_1=T -> satisfied
• C_2: x_4=T -> satisfied
• C_3: ~x_3=T -> satisfied
• C_4: x_4=T -> satisfied

Constructed target instance (PathConstrainedNetworkFlow):

• Variable arcs: e_1, e_2, e_3, e_4 (capacity 1 each)
• Clause arcs: e_5, e_6, e_7, e_8 (capacity 1 each)
• Literal arcs: c_{1,1}, c_{1,2}, c_{1,3}, c_{2,1}, c_{2,2}, c_{2,3}, c_{3,1}, c_{3,2}, c_{3,3}, c_{4,1}, c_{4,2}, c_{4,3} (capacity 1 each)
• Variable paths (8 total): p_{x_1}, p_{~x_1}, p_{x_2}, p_{~x_2}, p_{x_3}, p_{~x_3}, p_{x_4}, p_{~x_4}
• Clause paths (12 total): 3 per clause
• R = 4 + 4 = 8

Solution mapping:

• Assignment x_1=T, x_2=T, x_3=F, x_4=T:
  • Select paths p_{x_1}, p_{x_2}, p_{~x_3}, p_{x_4} (flow = 1 each, 4 units)
  • For C_1: x_1 satisfies it, select clause path p~_{1,1} (1 unit)
  • For C_2: x_4 satisfies it, select clause path p~_{2,3} (1 unit)
  • For C_3: x_3 satisfies it, select clause path p_{3,2} (1 unit)
  • For C_4: x_4 satisfies it, select clause path p~_{4,3} (1 unit)
  • Total flow into t = 4 + 4 = 8 = R

References

• [Promel, 1978]: [Promel1978] H. J. Pr{"o}mel (1978). "".

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No existing reduction path from KSatisfiability to PathConstrainedNetworkFlow
Non-trivial	✅ Pass	Gadget construction with variable arcs, clause arcs, and capacity-enforced binary choices
Correctness	⚠️ Warn	Reference [Promel, 1978] cannot be independently verified; reduction algorithm is AI-generated and underspecified
Well-written	❌ Fail	Overhead table uses non-existent size fields; algorithm lacks precise graph topology; reference has empty title

Overall: 2 passed, 1 warning, 1 failed

---

Usefulness

pred path KSatisfiability PathConstrainedNetworkFlow returns no existing path. This reduction would be a novel edge in the reduction graph, connecting Boolean satisfiability to a network flow variant. The motivation is substantive: it highlights that restricting flow to prescribed paths makes an otherwise polynomial problem NP-complete.

Verdict: Pass

Non-trivial

The reduction involves genuine structural transformation: variable gadgets (arcs with unit capacity enforcing binary choice), clause gadgets (arcs requiring at least one satisfied literal to carry flow), and linking arcs that create conflicts between variable assignments and clause satisfaction paths. This is not a relabeling or subtype coercion.

Verdict: Pass

Correctness

Reference verification:

1. Garey & Johnson, ND34, p.215: The issue quotes a GJ source entry for ND34 "PATH CONSTRAINED NETWORK FLOW" that references "[Promel, 1978]. Transformation from 3SAT." This is consistent with GJ's format. However, the original Promel 1978 paper cannot be found in any online database (arxiv, Semantic Scholar, Google Scholar). It appears to be an unpublished manuscript or personal communication cited only by GJ. This is not uncommon for GJ entries from the 1970s, but it means the detailed reduction construction cannot be verified against the original source.

2. References section: The BibTeX-style entry at the bottom is H. J. Pr{\"o}mel (1978). "" — the paper title is empty. This is incomplete and unhelpful for anyone trying to trace the reference.

3. Reduction algorithm: All substantive sections are marked with ⚠️ Unverified: AI-generated warnings. The algorithm sketch is plausible at a high level (variable arcs enforce binary choice, clause arcs require satisfaction), but the actual graph topology is not specified:

   • How many vertices are there and what are they?
   • How are arcs arranged to form valid s-t paths?
   • How does each variable path traverse from source s to sink t while passing through its variable arc?
   • How do clause paths traverse both a clause arc and a literal arc while remaining valid s-t paths?

   Without this detail, the construction cannot be verified for correctness.

Verdict: Warn — the GJ citation is plausible but the original paper is unverifiable, and the algorithm is too high-level to confirm correctness.

Well-written

4a. Information Completeness:

Section	Status
Source	✅ "3SAT" (resolves to KSatisfiability)
Target	✅ "PATH CONSTRAINED NETWORK FLOW" (resolves to PathConstrainedNetworkFlow)
Motivation	✅ Clear and substantive
Reference	❌ Paper title is empty in the References section
Reduction Algorithm	⚠️ Present but underspecified (see below)
Size Overhead	❌ Uses wrong metric names (see below)
Validation Method	✅ Reasonable closed-loop test plan
Example	⚠️ Partially worked (see below)

4b. Algorithm Completeness:

The reduction algorithm provides a high-level sketch but is not a complete, step-by-step procedure a programmer could implement:

• The graph construction is described in terms of "arcs" but never specifies the vertices or the full graph topology (which vertex connects to which via which arc).
• It says "create two paths: p_{x_i} and p_{~x_i}. Both paths traverse arc e_i" but does not describe the other arcs/vertices these paths traverse to form valid s-t paths.
• The linking mechanism ("Arc c_{j,k} is also traversed by the variable path") is described at a conceptual level but the actual path construction is not spelled out.

Verdict: Fail — the algorithm is a sketch, not an implementable procedure.

4c. Symbol and Notation Consistency:

• The overhead table uses num_vertices, num_arcs, num_paths, and requirement as "Target metric (code name)" fields.
• The actual size_fields for PathConstrainedNetworkFlow are only num_arcs and num_paths.
• num_vertices and requirement are not valid size fields on the target problem.
• The num_vertices overhead is given as O(n + m) — an asymptotic bound, not an exact expression as required for the overhead system.

Verdict: Fail — overhead table references non-existent size fields.

4d. Example Quality:

• The source instance (4 variables, 4 clauses) is reasonably sized with multiple feasible assignments — good.
• The target instance construction lists arcs and paths but does not show the actual graph (vertices, adjacency). Without seeing the graph, the example cannot be verified by hand.
• The solution mapping is shown but is based on the underspecified construction, so its correctness cannot be confirmed.

Verdict: Fail — example does not fully work through the target instance construction.

---

Recommendations

• The Promel 1978 reference appears to be an unpublished manuscript. Consider citing the Garey & Johnson entry directly as the primary reference (since that is what is actually available), and note that the original Promel paper is not publicly accessible.
• The reduction algorithm needs a complete, explicit graph construction: define all vertices, all arcs with their endpoints, and show how each path is a valid s-t walk. A diagram would help significantly.
• Fix the overhead table to use only num_arcs and num_paths (the actual size fields). Remove num_vertices and requirement rows, or check whether these getter methods actually exist on the target type.
• The example should include the full target graph (as an adjacency list or edge list) so that the construction can be verified by hand.
• The dissertation by Maren Martens, "Path-Constrained Network Flows" (TU Dortmund, 2007), may contain a detailed treatment of this reduction and could serve as a more accessible reference.