[Rule] 3SAT to ONE-IN-THREE 3SAT

[isPANN]

Source: 3SAT
Target: ONE-IN-THREE 3SAT

Motivation: Establishes NP-completeness of One-in-Three 3SAT via polynomial-time reduction from 3SAT. One-in-Three 3SAT is a fundamental problem in Schaefer's dichotomy theorem and serves as a common starting point for reductions to graph problems (e.g., graph coloring, independent set on special structures) due to its rigid "exactly one true" constraint.

Reference: Garey & Johnson, Computers and Intractability, Appendix A9.1, p.259

GJ Source Entry

[LO4] ONE-IN-THREE 3SAT
INSTANCE: Set U of variables, collection C of clauses over U such that each clause c E C has |c| = 3.
QUESTION: Is there a truth assignment for U such that each clause in C has exactly one true literal?
Reference: [Schaefer, 1978b]. Transformation from 3SAT.
Comment: Remains NP-complete even if no c E C contains a negated literal.

Reduction Algorithm

Reference: [Schaefer, 1978b]. Transformation from 3SAT.

Summary:
Given a 3SAT instance with n variables and m clauses, construct a One-in-Three 3SAT instance as follows:

For each 3SAT clause Cⱼ = (l₁ ∨ l₂ ∨ l₃), introduce 6 fresh auxiliary variables aⱼ, bⱼ, cⱼ, dⱼ, eⱼ, fⱼ and create 5 one-in-three clauses using the predicate R(u,v,w) meaning "exactly one of u, v, w is true":

1. R(l₁, aⱼ, dⱼ)
2. R(l₂, bⱼ, dⱼ)
3. R(aⱼ, bⱼ, eⱼ)
4. R(cⱼ, dⱼ, fⱼ)
5. R(l₃, cⱼ, ⊥)

where ⊥ is a designated variable forced to be false (shared across all clauses — add one global variable z₀ and one clause R(z₀, z₀, z₀) to force z₀ = false, or equivalently use a constant false slot).

Correctness: The 5 R-clauses are simultaneously satisfiable (by some setting of aⱼ, bⱼ, cⱼ, dⱼ, eⱼ, fⱼ) if and only if at least one of l₁, l₂, l₃ is true. This is because:

• If all three literals are false, R(l₁, aⱼ, dⱼ) forces exactly one of aⱼ, dⱼ to be true, and the chain of constraints propagates a contradiction.
• If at least one literal is true, a consistent assignment to the auxiliaries can be found.

Solution extraction: Restrict the satisfying assignment to the original n variables.

Handling negated literals: If literal lᵢ = ¬xₖ, we need to represent negation. One approach: introduce a "complement" variable x̄ₖ for each variable xₖ, and add a clause R(xₖ, x̄ₖ, z_aux) with a fresh auxiliary to enforce xₖ ⊕ x̄ₖ = 1 (exactly one true). Then use x̄ₖ wherever ¬xₖ appears.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_vars	n + 6m + 1 (n original variables + 6 auxiliaries per clause + 1 false-forcing variable)
num_clauses	5m + 1 (5 clauses per original clause + 1 false-forcing clause)

If negated literals require complement variables (see above), add up to n complement variables and n enforcement clauses:
| num_vars (with negation) | 2n + 6m + 1 |
| num_clauses (with negation) | 5m + n + 1 |

Validation Method

• Closed-loop test: reduce a 3SAT instance, solve the One-in-Three 3SAT target with BruteForce, extract solution, verify each original clause is satisfied
• Verify the one-in-three property: each target clause has exactly one true literal
• Test with both satisfiable and unsatisfiable 3SAT instances
• Test edge case: clauses with negated literals

Example

Source instance (3SAT):
Variables: x₁, x₂, x₃, x₄
Clauses:

• C₁ = (x₁ ∨ x₂ ∨ x₃)
• C₂ = (¬x₁ ∨ x₃ ∨ x₄)
• C₃ = (x₂ ∨ ¬x₃ ∨ ¬x₄)

This instance is satisfiable, e.g., x₁=T, x₂=T, x₃=F, x₄=T.

Constructed target instance (One-in-Three 3SAT):

Global false-forcing variable: z₀, with clause R(z₀, z₀, z₀) forcing z₀ = F.

For C₁ = (x₁ ∨ x₂ ∨ x₃), auxiliary variables a₁, b₁, c₁, d₁, e₁, f₁:

1. R(x₁, a₁, d₁)
2. R(x₂, b₁, d₁)
3. R(a₁, b₁, e₁)
4. R(c₁, d₁, f₁)
5. R(x₃, c₁, z₀)

For C₂ = (¬x₁ ∨ x₃ ∨ x₄), we need x̄₁ as complement of x₁. Auxiliary variables a₂, b₂, c₂, d₂, e₂, f₂:
6. R(x̄₁, a₂, d₂)
7. R(x₃, b₂, d₂)
8. R(a₂, b₂, e₂)
9. R(c₂, d₂, f₂)
10. R(x₄, c₂, z₀)

For C₃ = (x₂ ∨ ¬x₃ ∨ ¬x₄), we need x̄₃, x̄₄. Auxiliary variables a₃, b₃, c₃, d₃, e₃, f₃:
11. R(x₂, a₃, d₃)
12. R(x̄₃, b₃, d₃)
13. R(a₃, b₃, e₃)
14. R(c₃, d₃, f₃)
15. R(x̄₄, c₃, z₀)

Plus complement-enforcement clauses (with fresh auxiliaries p₁, p₃, p₄):
16. R(x₁, x̄₁, p₁)
17. R(x₃, x̄₃, p₃)
18. R(x₄, x̄₄, p₄)

Totals: 4 + 3 + 18 + 1 + 3 = 29 variables, 18 + 1 = 19 clauses (including the z₀-forcing clause).

Solution mapping:

• Source assignment: x₁=T, x₂=T, x₃=F, x₄=T
• Complements: x̄₁=F, x̄₃=T, x̄₄=F
• Each of the 5-clause gadgets is satisfiable (at least one literal in the original clause is true)
• Extracted source solution: restrict to x₁, x₂, x₃, x₄ → verifies all original clauses

References

• [Schaefer, 1978b]: [Schaefer1978b] T. J. Schaefer (1978). "The complexity of satisfiability problems". In: Proceedings of the 10th Annual ACM Symposium on Theory of Computing, pp. 216–226. Association for Computing Machinery.

[GiggleLiu]

Implemented in PR #1010.