[Rule] 3SAT to NON-LIVENESS OF FREE CHOICE PETRI NETS

[isPANN]

Source: 3SAT (KSatisfiability with K=3)
Target: NON-LIVENESS OF FREE CHOICE PETRI NETS (NonLivenessFreePetriNet)

Motivation: Establishes NP-completeness of determining whether a free-choice Petri net can reach a deadlock state. This is a fundamental result in concurrency theory, showing that even the well-structured class of free-choice nets has intractable liveness analysis. The reduction from 3SAT encodes clause satisfaction as token flow through a Petri net, where a satisfying assignment corresponds to a live execution and an unsatisfiable formula forces a deadlock. NP membership (the harder direction) was established independently by Hack (1972).
Reference: Garey & Johnson, Computers and Intractability, A12 MS3; Jones, Landweber, Lien 1977

GJ Source Entry

[MS3] NON-LIVENESS OF FREE CHOICE PETRI NETS
INSTANCE: Petri net P = (S, T, F, M_0) satisfying the free-choice property.
QUESTION: Is P not live?

Reference: [Jones, Landweber, and Lien, 1977]. Transformation from 3-SATISFIABILITY.
Comment: The proof that this problem belongs to NP is nontrivial [Hack, 1972].

Reduction Algorithm

Summary:
Given a 3SAT instance phi with variables x_1, ..., x_n and clauses C_1, ..., C_m, construct a free-choice Petri net P = (S, T, F, M_0) as follows:

1. Variable gadgets: For each variable x_i, create two places p_i (representing x_i = true) and p_i' (representing x_i = false), and two transitions: t_i^+ that consumes from a "choice place" c_i and produces a token in p_i, and t_i^- that consumes from c_i and produces a token in p_i'. The choice place c_i gets one token in M_0. This ensures exactly one truth value is selected per variable, and the free-choice property holds because c_i is the sole input to both t_i^+ and t_i^-.

2. Clause gadgets: For each clause C_j = (l_1 OR l_2 OR l_3), create a "clause place" q_j that needs at least one token to enable a transition t_j^check. For each literal l_k in C_j, add an arc from the corresponding literal place (p_i if positive, p_i' if negative) to q_j via an intermediate transition. The free-choice property is maintained by ensuring each place feeds into at most one transition, or all transitions sharing an input place have identical input sets.

3. Deadlock encoding: The clause-checking transition t_j^check can only fire if clause C_j is satisfied (at least one literal place has a token routed to q_j). If all clauses are satisfiable, the net can continue firing (is live). If some clause is unsatisfied, the corresponding clause transition is permanently dead, making the net not live.

4. Initial marking M_0: Place one token in each choice place c_i. All other places start empty.

Correctness:

• (=>) If phi is unsatisfiable, then for every truth assignment (token routing choice), at least one clause has no satisfied literal, so its clause transition is dead. The net is not live. Answer: YES.
• (<=) If phi is satisfiable, the token routing corresponding to the satisfying assignment enables all clause transitions. The net can be shown to be live. Answer: NO.

Note: The actual construction by Jones, Landweber, and Lien (1977) is more intricate to ensure the free-choice property holds globally. The above is a simplified sketch.

Size Overhead

Symbols:

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

Target metric (code name)	Polynomial (using symbols above)
num_places	O(n + m)
num_transitions	O(n + m)

Derivation:

• Variable gadgets: 2 literal places + 1 choice place per variable = 3n places, 2 transitions per variable = 2n transitions.
• Clause gadgets: O(1) places and transitions per clause = O(m).
• Intermediate routing places/transitions for free-choice compliance: O(m) additional.
• Total: O(n + m) places, O(n + m) transitions.

Validation Method

• Closed-loop test: reduce a KSatisfiability instance to NonLivenessFreePetriNet, solve target with BruteForce (explore reachability graph for dead transitions), verify that the answer matches the satisfiability of the original formula.
• Test with a satisfiable 3SAT instance (e.g., (x1 OR x2 OR x3)): net should be live, answer NO.
• Test with an unsatisfiable 3SAT instance (e.g., (x) AND (NOT x) padded to 3 literals): net should not be live, answer YES.
• Verify the free-choice property holds in all constructed nets.

Example

Source instance (KSatisfiability):
2 variables {x1, x2}, 2 clauses:

• C1 = (x1 OR x2 OR x2) -- x1 or x2
• C2 = (NOT x1 OR NOT x2 OR NOT x2) -- not x1 or not x2

This is satisfiable (e.g., x1 = true, x2 = false satisfies both).

Constructed target instance (NonLivenessFreePetriNet):
Places: {c1, c2, p1, p1', p2, p2', q1, q2} (8 places)
Transitions:

• t1+: c1 -> p1 (assign x1 = true)
• t1-: c1 -> p1' (assign x1 = false)
• t2+: c2 -> p2 (assign x2 = true)
• t2-: c2 -> p2' (assign x2 = false)
• t_c1: checks clause 1 (enabled if p1 or p2 has token routed to q1)
• t_c2: checks clause 2 (enabled if p1' or p2' has token routed to q2)

Initial marking: M_0(c1) = 1, M_0(c2) = 1, all others = 0.

Since phi is satisfiable, the net is live. Answer: NO (the net IS live, so it is NOT the case that it is not live).

If we change to phi = (x1) AND (NOT x1) (unsatisfiable, padded to 3 literals), the net would not be live. Answer: YES.

References

• [Jones, Landweber, and Lien, 1977]: N.D. Jones, L.H. Landweber, Y.E. Lien (1977). "Complexity of Some Problems in Petri Nets." Theoretical Computer Science, 4(3), pp. 277-299.
• [Hack, 1972]: M. Hack (1972). "Analysis of Production Schemata by Petri Nets." MIT Project MAC TR-94.