[Rule] KSatisfiability to SubsetSum

[zazabap]

Source: KSatisfiability (3-SAT)
Target: SubsetSum
Motivation: Classical Karp reduction bridging Boolean satisfiability (formula domain) to number theory (algebraic domain). The canonical proof that SubsetSum is NP-complete. Uses a base-10 digit encoding where each digit position is independent (no carries).
Reference: Karp, 1972; Sipser, Introduction to the Theory of Computation, 2012, Theorem 7.56; CLRS, 4th ed., 2022, §34.5.5

Reduction Algorithm

Notation:

• Source: 3-CNF formula $\phi$ with $n$ variables $x_1, \ldots, x_n$ and $m$ clauses $C_1, \ldots, C_m$
• Target: SubsetSum instance with set $S$ of $2n + 2m$ integers and target $T$, each integer having $(n + m)$ decimal digits

Step 1 — Variable integers ($2n$ integers):

For each variable $x_i$, create two integers using $(n+m)$-digit base-10 representation:

$$y_i: \quad d_i = 1, \quad d_{n+j} = 1 \text{ if } x_i \in C_j$$ $$z_i: \quad d_i = 1, \quad d_{n+j} = 1 \text{ if } \overline{x_i} \in C_j$$

where $d_k$ denotes the $k$-th digit (1-indexed, most significant first).

Step 2 — Slack integers ($2m$ integers):

For each clause $C_j$, create two slack integers:

$$g_j: \quad d_{n+j} = 1 \quad \text{(all other digits 0)}$$ $$h_j: \quad d_{n+j} = 2 \quad \text{(all other digits 0)}$$

Step 3 — Target:

$$T: \quad d_i = 1 ;\forall, i \in [1, n], \quad d_{n+j} = 4 ;\forall, j \in [1, m]$$

Why no carries: Each variable digit sums to exactly 1 (we pick $y_i$ or $z_i$). Each clause digit sums to at most $3$ (from literals) $+ 2$ (from $h_j$) $= 5 < 10$, so digits are independent.

Why it works: Selecting $y_i$ ($z_i$) corresponds to setting $x_i = T$ ($x_i = F$). Variable digits force exactly one of $y_i, z_i$ per variable. Clause digits count how many selected literals satisfy each clause; the slacks $g_j, h_j$ pad to exactly 4, which is possible iff at least 1 literal satisfies the clause (contribution 1–3, padded with slack 1–3).

Solution extraction: For each $i$: if $y_i$ is in the subset, set $x_i = 1$; if $z_i$ is in the subset, set $x_i = 0$.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_elements	$2n + 2m$
max_digits	$n + m$

Validation Method

Closed-loop testing: solve 3-SAT by brute-force ($2^n$ enumeration), solve the reduced SubsetSum by brute-force ($2^{2n+2m}$ enumeration), and verify that the formula is satisfiable iff the target sum is achievable. Test with: satisfiable instance, unsatisfiable instance, single-clause, single-variable.

Example

Source instance: 3-SAT formula $(x_1 \lor x_2 \lor x_3) \land (\overline{x_1} \lor \overline{x_2} \lor x_3)$, $n = 3$, $m = 2$.

Constructed integers (5-digit base-10):

Integer	$d_1$	$d_2$	$d_3$	$d_4$ (C₁)	$d_5$ (C₂)	Decimal
$y_1$	1	0	0	1	0	10010
$z_1$	1	0	0	0	1	10001
$y_2$	0	1	0	1	0	1010
$z_2$	0	1	0	0	1	1001
$y_3$	0	0	1	1	1	111
$z_3$	0	0	1	0	0	100
$g_1$	0	0	0	1	0	10
$h_1$	0	0	0	2	0	20
$g_2$	0	0	0	0	1	1
$h_2$	0	0	0	0	2	2

Target: $T = 11144$

Verification: Assignment $x_1 = T, x_2 = T, x_3 = T$ (satisfying):

• Select $y_1 + y_2 + y_3 = 10010 + 1010 + 111 = 11131$
• Clause digits: $C_1 = 3, C_2 = 1$. Need $+1$ for $C_1$, $+3$ for $C_2$
• Add $g_1 + h_2 + g_2 = 10 + 2 + 1 = 13$
• Total: $11131 + 13 = 11144 = T$ ✓

Assignment $x_1 = F, x_2 = F, x_3 = F$ (unsatisfying — clause 1 has 0 true literals):

• Select $z_1 + z_2 + z_3 = 10001 + 1001 + 100 = 11102$
• Clause digits: $C_1 = 0, C_2 = 2$. Need $+4$ for $C_1$ — but max slack is $g_1 + h_1 = 3$. Cannot reach 4. ✗

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	No path from KSatisfiability to SubsetSum
Non-trivial	✅ Pass	Base-10 digit encoding with gadget construction
Correctness	⚠️ Warn	Karp 1972 attribution is imprecise
Well-written	⚠️ Warn	Target model SubsetSum not yet in codebase

Overall: 2 passed, 0 failed, 2 warnings

---

Usefulness

SubsetSum does not exist in the codebase. This canonical reduction (3-SAT → SubsetSum) bridges boolean satisfiability to number theory. Requires a [Model] issue for SubsetSum first (distinct from existing Knapsack — SubsetSum is a satisfaction problem).

Non-trivial

Base-10 digit encoding where each digit position represents a variable or clause. Constructs 2n variable integers + 2m slack integers with a "no carries" invariant ensuring digit-level independence. Genuine gadget construction.

Correctness — WARN

Reference	Status	Notes
Karp (1972)	⚠️ Imprecise	Karp's reduction tree goes SAT → 3-SAT → Exact Cover → Knapsack. The direct 3-SAT → SubsetSum digit encoding is a later textbook construction, not from Karp 1972.
Sipser (2012), Theorem 7.56	✅ Verified	Primary source for this specific digit-encoding construction
CLRS 4th ed. (2022), Section 34.5.5	✅ Verified	Same construction with 2(n+m) integers, target digit value 4

The algorithm is mathematically correct: digit-level independence (max sum < 10) ensures no carries, slack pairs (g_j=1, h_j=2) correctly pad satisfied literal count to exactly 4. Example independently verified.

Recommendation: Clarify attribution: "Karp (1972) established NP-completeness of Knapsack via Exact Cover; the direct 3-SAT → SubsetSum construction follows Sipser (2012, Thm 7.56) and CLRS (2022, Sec 34.5.5)."

Well-written

All sections present. Algorithm is detailed and implementable. Example (3 vars, 2 clauses) is fully worked with both satisfying and unsatisfying assignment verification.

Minor issues:

• Mixed notation (1/0 vs T/F) for boolean values
• Overhead metrics num_elements, max_digits cannot be verified until SubsetSum model exists

Recommendations

1. File a [Model] issue for SubsetSum as prerequisite
2. Clarify Karp 1972 attribution
3. Standardize boolean notation (1/0 or T/F, not both)

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Target problem SubsetSum does not exist in the codebase; no existing path from KSatisfiability
Non-trivial	✅ Pass	Gadget construction with base-10 digit encoding, slack variables, and carry-free arithmetic
Correctness	✅ Pass	All three references verified; claims are consistent with the literature
Well-written	✅ Pass	Complete algorithm, consistent notation, fully worked example

Overall: 4 passed, 0 failed, 0 warnings

---

Usefulness

SubsetSum is not yet implemented in the reduction graph (pred show SubsetSum fails). There is also no existing path from KSatisfiability to the related Knapsack problem. This reduction is the canonical proof that Subset Sum is NP-complete and would bridge the formula domain (Boolean satisfiability) to the algebraic/number-theoretic domain. Pass — novel reduction to a new problem.

Note: implementing this rule requires first adding a SubsetSum model to the codebase.

Non-trivial

The reduction constructs 2n + 2m integers using an (n+m)-digit base-10 encoding scheme. Each variable produces two integers (positive/negative literal), each clause produces two slack integers, and the target value enforces both variable-selection constraints (exactly one of yi/zi per variable) and clause-satisfaction constraints (at least one true literal per clause). This is a genuine structural transformation involving gadget construction and penalty-term encoding — not a relabeling or type coercion. Pass.

Correctness

Karp, 1972 — "Reducibility among Combinatorial Problems" is present in the project bibliography (references.bib, key karp1972). The paper does include Knapsack/Subset Sum among its 21 NP-complete problems, though the original Karp reduction tree routes through Exact Cover rather than directly from 3-SAT. The issue correctly cites this as foundational context rather than the specific construction used. Verified.

Sipser, 2012 — "Introduction to the Theory of Computation" (3rd edition) is a standard textbook. Theorem 7.56 covers the SUBSET-SUM NP-completeness proof via reduction from 3-SAT using the digit-encoding technique described in the issue. Verified.

CLRS, 4th ed., 2022 — "Introduction to Algorithms" Section 34.5.5 covers the 3-SAT to Subset Sum reduction. The construction in the issue (base-10 digits, target digit value 4, slack pairs with values 1 and 2) matches the standard CLRS presentation. Verified.

The mathematical claims are consistent across all three sources and match the project's knowledge base (references.md confirms 3-SAT → Knapsack in Karp's tree, and Subset Sum as a canonical NP-complete problem).

Well-written

Information completeness: All required sections are present and substantive — Source, Target, Motivation, Reference, Reduction Algorithm, Size Overhead, Validation Method, and Example.

Algorithm completeness: The three-step algorithm is detailed and implementable: Step 1 defines variable integers with explicit digit assignments, Step 2 defines slack integers, Step 3 defines the target. Solution extraction is clearly stated. The no-carries argument is provided to justify correctness.

Notation consistency: All symbols are defined before use (n, m, di, yi, zi, gj, hj, T). The notation is consistent across all sections. The overhead table uses num_elements and max_digits — these cannot be validated against pred show since SubsetSum is not yet implemented, but the names are reasonable for the target problem's schema.

Example quality: The example uses n=3 variables and m=2 clauses, producing 10 integers — non-trivial enough to exercise the reduction meaningfully while remaining hand-verifiable. Both a satisfying and unsatisfying assignment are checked, with arithmetic shown step by step. The digit table is clear and correct. Pass.