[Rule] 3-Satisfiability to Cyclic Ordering

[isPANN]

Source: 3-Satisfiability (3SAT)
Target: Cyclic Ordering

Motivation: Establishes NP-completeness of CYCLIC ORDERING by encoding a 3SAT instance into cyclic order constraints on a finite set. The reduction encodes variable assignments as the relative cyclic position of "true" and "false" marker elements, and clause satisfaction as cyclic ordering triples that force at least one literal per clause to adopt the correct orientation. This connects propositional logic to a fundamental combinatorial ordering problem.
Reference: Garey & Johnson, Computers and Intractability, A1.2 MS2; Galil and Megiddo 1977

GJ Source Entry

[MS2] CYCLIC ORDERING
INSTANCE: Finite set A, collection C of ordered triples (a, b, c) of distinct elements from A.
QUESTION: Is there a one-to-one function f: A → {1, 2, ..., |A|} such that for each (a, b, c) ∈ C either f(a) < f(b) < f(c), or f(b) < f(c) < f(a), or f(c) < f(a) < f(b)?
Reference: [Galil and Megiddo, 1977]. Transformation from 3-SATISFIABILITY.

Reduction Algorithm

Summary:
Given a 3SAT instance with variables x_1, ..., x_n and clauses C_1, ..., C_m, construct a Cyclic Ordering instance as follows:

1. Elements: Create the following elements in set A:

   • A special reference element r
   • For each variable x_i: two elements t_i (true) and f_i (false)
   • Additional clause gadget elements as needed for each clause

2. Variable encoding: For each variable x_i, add the cyclic ordering triple (r, t_i, f_i). This forces either:

   • r < t_i < f_i (cyclically), encoding x_i = TRUE, or
   • r < f_i < t_i (cyclically), encoding x_i = FALSE

   The relative cyclic order of t_i and f_i with respect to r determines the truth value of x_i.

3. Clause encoding: For each clause C_j = (l_1 ∨ l_2 ∨ l_3), introduce clause gadget elements and triples that are satisfiable in cyclic order if and only if at least one literal l_k is true. The exact gadget construction uses auxiliary elements to connect the literal orientations to the clause satisfaction requirement. For a positive literal x_i in a clause, the gadget references t_i; for a negative literal ¬x_i, it references f_i.

4. Correctness: A valid cyclic ordering f exists if and only if there is a satisfying assignment for the 3SAT instance. The variable triples fix the truth assignment, and the clause gadgets ensure at least one literal per clause is satisfied.

5. Solution extraction: From a valid cyclic ordering f, determine x_i = TRUE if t_i appears before f_i in cyclic order relative to r, and x_i = FALSE otherwise.

Key invariant: The cyclic position of t_i relative to f_i (with respect to reference r) encodes a Boolean variable, and the clause gadgets enforce that at least one literal per clause is correctly oriented.

Time complexity of reduction: O(n + m) elements and O(n + m) triples (polynomial).

Size Overhead

Symbols:

• n = num_variables of source 3SAT instance
• m = num_clauses of source 3SAT instance

Target metric (code name)	Polynomial (using symbols above)
num_elements	O(num_variables + num_clauses)
num_triples	O(num_variables + num_clauses)

Derivation: 1 reference element + 2n variable elements + O(m) clause gadget elements. The number of triples is n (variable triples) + O(m) (clause gadget triples). The exact constants depend on the specific gadget construction from Galil and Megiddo.

Validation Method

• Closed-loop test: construct a 3SAT instance, reduce to Cyclic Ordering, solve target by brute-force permutation enumeration, verify the cyclic ordering corresponds to a satisfying assignment.
• Test with a known satisfiable 3SAT instance: (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ x2 ∨ ¬x3). Verify the reduction produces a YES instance.
• Test with a known unsatisfiable instance: the single clause (x1) ∧ (¬x1) — 2SAT but trivially unsatisfiable. Verify the reduction produces a NO instance.
• Verify that the cyclic ordering triples correctly distinguish between true and false literal orientations.

Example

Source instance (3SAT):
Variables: x_1, x_2
Clauses: C_1 = (x_1 ∨ x_2 ∨ x_2), C_2 = (¬x_1 ∨ ¬x_2 ∨ x_1)
Satisfying assignment: x_1 = TRUE, x_2 = TRUE (C_1: TRUE, C_2: x_1 is TRUE so TRUE).

Constructed target instance (Cyclic Ordering):

• Elements: A = {r, t_1, f_1, t_2, f_2, ...} (plus clause gadget elements)
• Variable triples: (r, t_1, f_1), (r, t_2, f_2)
• Clause triples: gadget-specific triples encoding C_1 and C_2.

Solution mapping:

• With x_1 = TRUE: in the cyclic ordering, t_1 appears before f_1 relative to r.
• With x_2 = TRUE: t_2 appears before f_2 relative to r.
• A valid cyclic ordering f exists that satisfies all triples, confirming the 3SAT instance is satisfiable.

Note: The full clause gadget construction is detailed in Galil and Megiddo (1977) and involves auxiliary elements that make the example verbose. The essential structure is that variable triples fix orientations and clause triples enforce disjunction.

References

• [Galil and Megiddo, 1977]: Z. Galil and N. Megiddo (1977). "Cyclic ordering is NP-complete." Theoretical Computer Science 5(2), pp. 179-182.
• [Garey and Johnson, 1979]: M. R. Garey and D. S. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, pp. 225 (MS2).

[zazabap]

verify-reduction: OPEN — construction ambiguity in Galil & Megiddo 1977 scan.

The 10th triple in Δ⁰ (the last entry) is ambiguous in the scanned PDF — nml vs lmn changes the cyclic direction. Testing both orientations:

• (N,M,L): passes 36/36 small instances (1-2 clauses) but blocks all-TRUE case for single clause
• (L,M,N): allows solutions for unsatisfiable instances (incorrect)

The smallest unsatisfiable 3SAT with n=3 requires all 8 clauses (49 elements), making brute-force CO verification infeasible (49! permutations).

Needs: clean digital copy of the original paper, or a textbook reproducing the exact construction.

[GiggleLiu]

Implemented in PR #1010.