[Rule] 3SAT to KClique

[isPANN]

---

name: Rule
about: Propose a new reduction rule
title: "[Rule] 3SAT to KClique"
labels: rule
assignees: ''
canonical_source_name: '3-Satisfiability (3SAT)'
canonical_target_name: 'KClique'
source_in_codebase: true
target_in_codebase: false

Source: KSatisfiability (K3)
Target: KClique
Motivation: Establishes NP-completeness of CLIQUE via polynomial-time reduction from 3SAT. This is one of Karp's 21 NP-complete problems (1972) and one of the most widely taught reductions in computational complexity. The construction elegantly encodes satisfiability constraints into graph structure, demonstrating that finding large complete subgraphs is computationally as hard as solving Boolean satisfiability.

Reference: Garey & Johnson, Computers and Intractability, A1.2 GT19

GJ Source Entry

[GT19] CLIQUE
INSTANCE: Graph G = (V,E), positive integer K <= |V|.
QUESTION: Does G contain a clique of size K or more, i.e., a subset V' <= V with |V'| >= K such that every two vertices in V' are joined by an edge in E?

Reference: [Karp, 1972]. Transformation from VERTEX COVER (see Chapter 3).
Comment: Solvable in polynomial time for graphs obeying any fixed degree bound d, for planar graphs, for edge graphs, for chordal graphs [Gavril, 1972], for comparability graphs [Even, Pnueli, and Lempel, 1972], for circle graphs [Gavril, 1973], and for circular arc graphs (given their representation as families of arcs) [Gavril, 1974a]. The variant in which, for a given r, 0 < r < 1, we are asked whether G contains a clique of size r|V| or more is NP-complete for any fixed value of r.

Reduction Algorithm

Summary:
Given a 3SAT instance φ with num_clauses clauses C_1, C_2, ..., C_{num_clauses}, each clause C_i = (l_{i,1} ∨ l_{i,2} ∨ l_{i,3}) containing exactly 3 literals over num_vars Boolean variables, construct a KClique instance (G, num_clauses) as follows:

1. Vertex construction: For each clause C_i and each literal l_{i,j} in that clause, create a vertex v_{i,j}. This yields exactly 3·num_clauses vertices, organized into num_clauses groups (triples) of 3, one triple per clause.

2. Edge construction: Connect two vertices v_{i,a} and v_{j,b} with an edge if and only if:

   • They belong to different clauses (i ≠ j), AND
   • Their literals are not contradictory (l_{i,a} is not the negation of l_{j,b}).
     In other words, edges are absent only between vertices in the same triple and between vertices labeled with complementary literals (x and ¬x).

3. Clique size parameter: Set K = num_clauses.

4. Solution extraction: Given a clique C of size num_clauses in G, construct a satisfying assignment by setting each literal corresponding to a vertex in C to TRUE. This is consistent because no two vertices in the clique have contradictory labels (such pairs have no edge, so cannot both be in a clique). Each clause is satisfied because the clique contains exactly one vertex from each triple.

Correctness:

• (Forward) If φ is satisfiable, pick one true literal per clause. The corresponding num_clauses vertices form a clique: they are from different triples (so edges exist between them) and their labels are consistent with a single assignment (so no contradictory pairs).
• (Backward) If G has a num_clauses-clique, no two vertices can come from the same triple (no intra-triple edges), so exactly one vertex per clause is selected. The labels on these vertices define a consistent truth assignment that satisfies all num_clauses clauses.

Note: Both KSatisfiability and KClique are satisfaction problems (Metric = bool), so no sat/opt type bridge is needed. The reduction maps satisfying assignments bijectively to k-cliques.

Source: Karp (1972), "Reducibility among combinatorial problems"; Sipser, Introduction to the Theory of Computation, Theorem 7.32; Garey & Johnson Chapter 3.

Size Overhead

Symbols:

• num_clauses: number of clauses in the 3SAT formula
• num_vars: number of variables in the 3SAT formula

Target metric (code name)	Formula
num_vertices	3 * num_clauses
num_edges	9 * num_clauses * (num_clauses - 1) / 2 (upper bound)
k	num_clauses

Derivation: There are 3·num_clauses vertices (3 per clause). Cross-triple vertex pairs total 9 · C(num_clauses, 2) = 9·num_clauses·(num_clauses − 1)/2. From these we subtract pairs with contradictory labels (x_i and ¬x_i across different triples). The exact number of contradictory pairs is instance-dependent, so the overhead uses the upper bound (zero contradictory pairs removed). In the worst case (all distinct variables per clause), this bound is tight.

Validation Method

• Closed-loop test: construct a 3SAT instance, reduce to KClique (G, k), solve the KClique instance with BruteForce, extract the satisfying assignment from the clique vertices, verify it satisfies the original 3SAT formula.
• Forward test: generate a known-satisfiable 3SAT instance, verify the constructed graph contains a k-clique.
• Backward test: generate a known-unsatisfiable 3SAT instance, verify no k-clique exists in G.
• Size verification: check that the graph has exactly 3·num_clauses vertices and that no intra-triple edges or contradictory-literal edges exist.

Example

Source instance (3SAT):
Variables: x_1, x_2, x_3 (num_vars = 3)
Clauses (num_clauses = 3):

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

Constructed target instance (KClique):
Vertices (3·num_clauses = 9):

• Triple 1 (C_1): v_{1,1}=x_1, v_{1,2}=¬x_2, v_{1,3}=x_3
• Triple 2 (C_2): v_{2,1}=¬x_1, v_{2,2}=x_2, v_{2,3}=¬x_3
• Triple 3 (C_3): v_{3,1}=x_1, v_{3,2}=x_2, v_{3,3}=x_3

Edges (connect cross-triple non-contradictory pairs):

• v_{1,1}(x_1) — v_{2,2}(x_2): YES
• v_{1,1}(x_1) — v_{2,3}(¬x_3): YES
• v_{1,1}(x_1) — v_{2,1}(¬x_1): NO (contradictory)
• v_{1,1}(x_1) — v_{3,1}(x_1): YES
• v_{1,1}(x_1) — v_{3,2}(x_2): YES
• v_{1,1}(x_1) — v_{3,3}(x_3): YES
• v_{1,2}(¬x_2) — v_{2,1}(¬x_1): YES
• v_{1,2}(¬x_2) — v_{2,2}(x_2): NO (contradictory)
• v_{1,2}(¬x_2) — v_{2,3}(¬x_3): YES
• v_{1,2}(¬x_2) — v_{3,1}(x_1): YES
• v_{1,2}(¬x_2) — v_{3,2}(x_2): NO (contradictory)
• v_{1,2}(¬x_2) — v_{3,3}(x_3): YES
• v_{1,3}(x_3) — v_{2,1}(¬x_1): YES
• v_{1,3}(x_3) — v_{2,2}(x_2): YES
• v_{1,3}(x_3) — v_{2,3}(¬x_3): NO (contradictory)
• v_{1,3}(x_3) — v_{3,1}(x_1): YES
• v_{1,3}(x_3) — v_{3,2}(x_2): YES
• v_{1,3}(x_3) — v_{3,3}(x_3): YES
• v_{2,1}(¬x_1) — v_{3,1}(x_1): NO (contradictory)
• v_{2,1}(¬x_1) — v_{3,2}(x_2): YES
• v_{2,1}(¬x_1) — v_{3,3}(x_3): YES
• v_{2,2}(x_2) — v_{3,1}(x_1): YES
• v_{2,2}(x_2) — v_{3,2}(x_2): YES
• v_{2,2}(x_2) — v_{3,3}(x_3): YES
• v_{2,3}(¬x_3) — v_{3,1}(x_1): YES
• v_{2,3}(¬x_3) — v_{3,2}(x_2): YES
• v_{2,3}(¬x_3) — v_{3,3}(x_3): NO (contradictory)

Contradictory pairs (6 total): v_{1,1}–v_{2,1}, v_{1,2}–v_{2,2}, v_{1,2}–v_{3,2}, v_{1,3}–v_{2,3}, v_{2,1}–v_{3,1}, v_{2,3}–v_{3,3}.

Total edges: 27 cross-triple pairs − 6 contradictory = 21 edges.

Clique size: K = 3

Solution mapping:

• 3-clique in G: {v_{1,1}(x_1), v_{2,2}(x_2), v_{3,3}(x_3)}
  • Check edges: v_{1,1}–v_{2,2} (YES), v_{1,1}–v_{3,3} (YES), v_{2,2}–v_{3,3} (YES). Valid clique.
• Extracted assignment: x_1 = TRUE, x_2 = TRUE, x_3 = TRUE
• Verification against 3SAT:
  • C_1 = (T ∨ F ∨ T) = TRUE
  • C_2 = (F ∨ T ∨ F) = TRUE
  • C_3 = (T ∨ T ∨ T) = TRUE
• All clauses satisfied. ✓

Alternative clique: {v_{1,2}(¬x_2), v_{2,1}(¬x_1), v_{3,3}(x_3)} is also a valid 3-clique (all three pairs have edges). Extracted assignment: x_1 = FALSE, x_2 = FALSE, x_3 = TRUE. Verification: C_1 = (F ∨ T ∨ T) = T, C_2 = (T ∨ F ∨ F) = T, C_3 = (F ∨ F ∨ T) = T. ✓

The formula has 5 satisfying assignments out of 8 total, and the graph has 12 distinct 3-cliques.

References

• [Karp, 1972]: [Karp1972] Richard M. Karp (1972). "Reducibility among combinatorial problems". In: Complexity of Computer Computations. Plenum Press.
• [Gavril, 1972]: [Gavril1972] F. Gavril (1972). "Algorithms for minimum coloring, maximum clique, minimum covering by cliques, and maximum independent set of a chordal graph". SIAM Journal on Computing 1, pp. 180-187.
• [Even, Pnueli, and Lempel, 1972]: [Even1972] S. Even and A. Pnueli and A. Lempel (1972). "Permutation graphs and transitive graphs". Journal of the Association for Computing Machinery 19, pp. 400-410.
• [Gavril, 1973]: [Gavril1973] F. Gavril (1973). "Algorithms for a maximum clique and a maximum independent set of a circle graph". Networks 3, pp. 261-273.
• [Gavril, 1974a]: [Gavril1974a] F. Gavril (1974). "Algorithms on circular-arc graphs". Networks 4, pp. 357-369.

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No existing path from KSatisfiability to MaximumClique
Non-trivial	✅ Pass	Gadget construction encoding clause structure into graph edges
Correctness	⚠️ Warn	Example edge count is wrong (claims 22, actual is 21); references verified
Well-written	❌ Fail	Overhead num_edges uses undefined variable num_complementary_pairs; example arithmetic error

Overall: 2 passed, 1 warning, 1 failed

---

Usefulness

Pass. There is currently no reduction path from KSatisfiability to MaximumClique in the codebase. This is one of Karp's original 21 reductions (confirmed in references.md as "3-SAT → Clique (clause-variable gadget)") and would add a novel edge to the reduction graph connecting formula-based problems to graph substructure problems.

Non-trivial

Pass. The reduction constructs a genuinely new graph from the clause structure: 3 vertices per clause, edges between non-contradictory cross-clause literal pairs. This is a classic gadget construction involving structural transformation, not a variable relabeling or type coercion.

Correctness

Warn. The core references check out:

• Karp (1972) — Confirmed. Already in docs/paper/references.bib as karp1972. The paper does include the SAT-to-CLIQUE reduction. Note: Karp's original is SAT→CLIQUE; the 3SAT specialization is the standard textbook presentation.
• Garey & Johnson (1979) — Confirmed. Already in bibliography as garey1979. GT19 is the correct GJ number for CLIQUE.
• Sipser, Theorem 7.32 — Standard textbook; the 3SAT→CLIQUE reduction is well-known to appear in Chapter 7. Could not independently verify the exact theorem number, but the content is correct.

However, the example contains an arithmetic error:

The issue lists 5 contradictory cross-triple pairs, but actually there are 6:

1. v_{1,1}(x₁) — v_{2,1}(¬x₁)
2. v_{1,2}(¬x₂) — v_{2,2}(x₂)
3. v_{1,2}(¬x₂) — v_{3,2}(x₂)
4. v_{1,3}(x₃) — v_{2,3}(¬x₃)
5. v_{2,1}(¬x₁) — v_{3,1}(x₁)
6. v_{2,3}(¬x₃) — v_{3,3}(x₃)

Correct edge count: 27 − 6 = 21 edges, not 22 as claimed. (Counting the YES entries in the issue's own edge listing confirms 21.)

Well-written

Fail. Several issues:

4a — Overhead table problems

1. Undefined variable in overhead formula. The num_edges formula references num_complementary_pairs, which is not a getter method on KSatisfiability. Available getters are: num_vars, num_clauses, num_literals. The overhead system requires all variable names to correspond to actual getter methods on the source type — num_complementary_pairs would cause a compile error.

2. No clean closed-form for num_edges. The issue acknowledges that the exact edge count depends on the specific formula ("contradictory_cross_pairs depends on the specific formula"). For the overhead system, an upper-bound expression using only source getters is needed. A valid upper bound would be: num_edges <= 9 * num_clauses * (num_clauses - 1) / 2. However, this is loose. Consider whether num_edges can be omitted from overhead (since MaximumClique's size_fields only lists num_vertices).

4b — Symbol inconsistency

The "Symbols" section defines k = number of clauses and n = number of variables, but the overhead table uses code-level getter names (num_clauses, num_complementary_pairs) without connecting them to the symbols k and n used in the derivation section. These should be consistent.

4c — Example arithmetic error

As noted in Correctness above, the edge count is wrong: 21, not 22. The issue first says 18, then "corrects" to 22, but both are wrong.

4d — Satisfaction-to-optimization mapping not addressed

KSatisfiability<K3> is a satisfaction problem (Metric = bool) while MaximumClique is an optimization problem (Metric = SolutionSize<W>). The reduction algorithm describes the classic decision-version reduction (k-clique exists iff formula is satisfiable), but does not address how solution extraction works in the optimization setting. Specifically: after finding the maximum clique (which may be larger than k for satisfiable instances, or smaller for unsatisfiable ones), how exactly is the satisfying assignment extracted? This should be clarified — the clique of size k within the maximum clique must be selected, or alternatively the reduction should note that the maximum clique size equals k iff the formula is satisfiable.

Recommendations

• Remove num_edges from the overhead table entirely, since MaximumClique's primary size field is num_vertices and the edge count cannot be expressed cleanly with source getters alone. Or provide a valid upper bound: num_edges = "9 * num_clauses * (num_clauses - 1) / 2".
• Fix the example edge count from 22 to 21 (6 contradictory pairs, not 5).
• Add a paragraph to the reduction algorithm explaining how the satisfaction/optimization type mismatch is handled in solution extraction.
• Unify notation: use getter names (num_clauses, num_vars) consistently throughout, or define the mapping (k = num_clauses, n = num_vars) once and use it consistently.

[isPANN]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Not redundant; direct edge adds educational value and simpler extraction
Non-trivial	✅ Pass	Classic gadget construction encoding clause structure into graph edges
Correctness	⚠️ Warn	Core reduction correct; example edge count arithmetic error (21, not 22)
Well-written	❌ Fail	Overhead uses undefined getter; example arithmetic wrong; sat/opt gap

Overall: 2 passed, 0 failed, 1 warning, 1 failed

---

Usefulness

Pass. A 4-step composite path exists (KSatisfiability → Satisfiability → MIS/One → MIS/i32 → MaximumClique) with overhead O(num_literals) vertices and O(num_literals²) edges. However, the redundancy check finds the proposed rule is Not Redundant:

• The direct rule produces O(num_clauses) vertices — comparable to the composite path (since num_literals = 3 * num_clauses for 3SAT), but with single-step solution extraction instead of 4 intermediate back-mappings.
• This is one of Karp's original 21 NP-complete reductions (1972) — high educational and documentation value.
• Motivation is substantive and well-justified.

Non-trivial

Pass. The reduction constructs a genuinely new graph from clause structure: 3 vertices per clause, edges between non-contradictory cross-clause literal pairs. This is a classic gadget construction involving structural transformation — not a variable relabeling, subtype coercion, or identity mapping.

Correctness

Warn. The core reduction algorithm is correct and well-established in the literature.

References verified:

Reference	Status	Notes
Karp (1972)	✅ In bib as karp1972	CLIQUE is #3 in Karp's list; note: Karp's original route is via Vertex Cover, not direct 3SAT→CLIQUE
Garey & Johnson (1979)	✅ In bib as garey1979	GT19 is correct GJ number for CLIQUE
Sipser, Theorem 7.32	✅ In bib as sipser2012	3SAT→CLIQUE construction appears in 3rd edition Thm 7.32
Gavril (1972)	✅ Not in bib	Real paper, SIAM J. Computing 1:180-187. GJ comment section reference.
Even, Pnueli, Lempel (1972)	✅ Not in bib	Real paper, JACM 19:400-410. GJ comment section reference.
Gavril (1973)	✅ Not in bib	Real paper, Networks 3:261-273. GJ comment section reference.
Gavril (1974a)	✅ Not in bib	Real paper, Networks 4:357-369. GJ comment section reference.

Example arithmetic error: The issue claims 5 contradictory pairs and 22 edges. The correct count is 6 contradictory pairs and 21 edges (27 cross-triple pairs − 6 contradictory = 21). Python brute-force verification confirms 21 edges, 12 valid 3-cliques, and the formula has 5 satisfying assignments out of 8. The contradictory pair missed in the count is v_{2,3}(¬x₃) — v_{3,3}(x₃), which IS listed as "NO" in the edge enumeration but was not counted in the final tally.

No better constructions found. The described construction is canonical — 3k vertices and O(k²) edges is essentially tight for this reduction.

Well-written

Fail. Several issues:

4a — Overhead table: undefined variable

The num_edges formula references num_complementary_pairs, which is not a getter method on KSatisfiability. Available getters: num_vars, num_clauses, num_literals. This would cause a compile error in the #[reduction(overhead = {...})] macro. The issue acknowledges the edge count depends on the specific formula, but the overhead system requires expressions using only source getters.

Fix options:

1. Provide an upper bound: num_edges = "9 * num_clauses * (num_clauses - 1) / 2" (all cross-triple pairs, worst case)
2. Drop num_edges from overhead entirely — MaximumClique's primary size field is num_vertices, and the edge count is instance-dependent

4b — Example arithmetic error

The edge count goes from "18" to a "corrected" "22", but both are wrong. The correct count is 21 (6 contradictory pairs, not 5). The issue's own edge-by-edge enumeration lists exactly 6 "NO" entries but counts only 5 in the summary.

4c — Symbol inconsistency

The "Symbols" section defines k = number of clauses and n = number of variables, but the overhead table uses code-level getter names (num_clauses, num_complementary_pairs) without connecting them to the mathematical symbols.

4d — Satisfaction-to-optimization type mismatch not addressed

KSatisfiability<K3> is a satisfaction problem (Metric = bool) while MaximumClique is an optimization problem (Metric = SolutionSize<W>). The reduction describes the classic decision-version (k-clique ↔ satisfiable), but does not address:

• How solution extraction works in the optimization framing
• The maximum clique may be larger than k for satisfiable instances
• For unsatisfiable instances, the maximum clique is smaller than k

This needs a paragraph explaining how the sat↔opt bridge works in the codebase context.

4e — Example quality

The example IS fully worked (all vertices and edges enumerated — good). Search space is 2⁹ = 512 configurations — appropriate size. The example has 12 valid 3-cliques and multiple suboptimal feasible solutions — good diversity.

Recommendations

1. Replace num_edges overhead with upper bound "9 * num_clauses * (num_clauses - 1) / 2" or drop it entirely
2. Fix example edge count: 6 contradictory pairs → 21 edges
3. Add paragraph on sat/opt type mismatch and solution extraction in the optimization context
4. Unify notation: define num_clauses = k, num_vars = n mapping once and use consistently

[isPANN]

Fix-issue changelog

• Target changed from MaximumClique to KClique (decision version, sat→sat — eliminates type mismatch)
• target_in_codebase set to false (KClique not yet implemented)
• Fixed example edge count: 22 → 21 (6 contradictory pairs, not 5)
• Replaced undefined num_complementary_pairs in overhead with upper bound 9 * num_clauses * (num_clauses - 1) / 2
• Added k = num_clauses to overhead table
• Unified notation: num_clauses/num_vars used consistently throughout
• Added sat/sat framing note (no type bridge needed)
• Added alternative clique example and summary statistics (12 cliques, 5/8 satisfying assignments)
• Removed confused "18...corrected to 22" paragraph

Applied by /fix-issue.