[Model] OneInThreeSatisfiability

[isPANN]

Motivation

ONE-IN-THREE 3SAT (P256) from Garey & Johnson, A9 LO4. Given a 3-CNF formula, determine whether there is a truth assignment such that each clause has exactly one true literal. NP-complete even without negated literals (Schaefer, 1978). A key problem in Schaefer's dichotomy theorem framework for generalized satisfiability, and widely used as a source for reductions to graph coloring, partition, and geometric problems.

Associated rules:

• [Rule] 3SAT to ONE-IN-THREE 3SAT #862: 3SAT → OneInThreeSatisfiability (classical NP-completeness proof from G&J)

Definition

Name: OneInThreeSatisfiability
Reference: Garey & Johnson, Computers and Intractability, A9 LO4

Mathematical definition:

INSTANCE: Set U of variables, collection C of clauses over U such that each clause c ∈ C has |c| = 3.
QUESTION: Is there a truth assignment for U such that each clause in C has exactly one true literal?

**Canonical name:** One-in-Three 3-Satisfiability (also known as 1-in-3 SAT, Positive 1-in-3 SAT when no negated literals)

Variables

• Count: n = |U| (one variable per Boolean variable)
• Per-variable domain: binary {0, 1} (false/true)
• Meaning: x_i = 1 if variable u_i is assigned true. A clause is satisfied iff exactly one of its three literals evaluates to true.

Schema (data type)

Type name: OneInThreeSatisfiability
Variants: none (clause size is always 3)

Field	Type	Description
num_vars	usize	Number of Boolean variables
clauses	Vec<[Literal; 3]>	Clauses each with exactly 3 literals

Notes:

• This is a feasibility (decision) problem: Value = Or.
• Structurally identical to KSatisfiability<K3>, but the evaluation criterion differs — each clause requires exactly one true literal instead of at least one.
• Key getter methods: num_vars(), num_clauses() (= clauses.len()).
• The Literal type encodes a variable index and its polarity (positive or negated).

Complexity

• Decision complexity: NP-complete (Schaefer, 1978; transformation from 3SAT). Remains NP-complete even if no clause contains a negated literal (Positive 1-in-3 SAT).
• Best known exact algorithm: Any 3-SAT exact algorithm can solve 1-in-3 SAT by modifying the acceptance criterion. The best known 3-SAT algorithm runs in O*(1.307^n) (Scheder & Steinberger, 2017). No dedicated 1-in-3 SAT algorithm with a provably better worst-case bound has been established in the literature.
• Concrete complexity expression: "1.307^num_vars" (for declare_variants!; conservative upper bound via 3-SAT reduction)
• References:
  • T.J. Schaefer (1978). "The Complexity of Satisfiability Problems." STOC 1978, pp. 216-226.
  • D. Scheder, J.P. Steinberger (2017). "PPSZ for General k-SAT — Making Hertli's Analysis Simpler and 3-SAT Faster." CCC 2017.

Specialization

• This is a special case of: Generalized Satisfiability (Schaefer's framework — the one-in-three constraint is a specific relation R)
• Known special cases: Positive One-in-Three 3SAT (no negated literals — still NP-complete)
• Restriction: Each clause has exactly 3 literals and exactly one must be true (vs. at-least-one for standard SAT, or not-all-equal for NAE-SAT)
• Relationship to NAE-SAT: If σ satisfies a One-in-Three instance, then both σ and ¬σ satisfy the corresponding NAE-SAT instance (one true and two false in each clause means not-all-equal holds)

Extra Remark

Full book text:

INSTANCE: Set U of variables, collection C of clauses over U such that each clause c∈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∈C contains a negated literal.

How to solve

• It can be solved by (existing) bruteforce. (Enumerate all 2^n truth assignments; check if each clause has exactly one true literal.)
• It can be solved by reducing to integer programming. (Binary variable per Boolean variable; for each clause with literals l_1, l_2, l_3, add constraint l_1 + l_2 + l_3 = 1 where negated literals use 1 − x_i. Companion rule issue to be filed separately.)
• Other:

Example Instance

Input:
n = 6 variables: x_1, x_2, x_3, x_4, x_5, x_6
m = 4 clauses (each requires exactly one true literal):

• C_1 = R(x_1, x_2, x_3)
• C_2 = R(x_4, x_5, x_6)
• C_3 = R(x_1, x_5, x_3)
• C_4 = R(x_2, x_4, x_6)

Satisfying assignment: x_1=T, x_2=F, x_3=F, x_4=F, x_5=F, x_6=T

• C_1: T, F, F → exactly 1 true ✓
• C_2: F, F, T → exactly 1 true ✓
• C_3: T, F, F → exactly 1 true ✓
• C_4: F, F, T → exactly 1 true ✓

Answer: YES — 5 out of 64 assignments satisfy all clauses.

Non-trivial structure: A greedy approach setting x_1=T and x_4=T would fail C_4 (needing x_2=F and x_6=F, but then C_2 has x_4=T, x_5=?, x_6=F requiring x_5=F, which gives C_3: x_1=T, x_5=F, x_3=? requiring x_3=F, so C_1: T,F,F ✓ — actually this also works with (1,0,0,1,0,0)). The 5 valid assignments are: (1,0,0,1,0,0), (0,0,1,1,0,0), (0,1,0,0,1,0), (1,0,0,0,0,1), (0,0,1,0,0,1).

Negative modification: Add clause C_5 = R(x_1, x_4, x_5). This forces exactly one of x_1, x_4, x_5 to be true. Of the 5 satisfying assignments above, only (0,1,0,0,1,0) satisfies C_5 (x_1=F, x_4=F, x_5=T → exactly 1). Now change C_5 to R(x_1, x_2, x_4). This requires exactly one of x_1, x_2, x_4 true. Checking: (1,0,0,1,0,0) has x_1=T, x_2=F, x_4=T → 2 true ✗. (0,0,1,1,0,0): x_1=F, x_2=F, x_4=T → 1 true ✓. (0,1,0,0,1,0): x_1=F, x_2=T, x_4=F → 1 true ✓. (1,0,0,0,0,1): x_1=T → 1 true ✓. (0,0,1,0,0,1): 0 true ✗. Down to 3. Adding C_6 = R(x_3, x_4, x_5): (0,0,1,1,0,0) has x_3=T, x_4=T → 2 ✗. (0,1,0,0,1,0) has x_3=F, x_4=F, x_5=T → 1 ✓. (1,0,0,0,0,1) has 0 ✗. Down to 1: (0,1,0,0,1,0). Adding C_7 = R(x_1, x_6, x_5): (0,1,0,0,1,0) has x_5=T → 1 ✓. Still satisfiable. Adding C_8 = R(x_2, x_5, x_6): (0,1,0,0,1,0) has x_2=T, x_5=T → 2 ✗. Answer: NO — no assignment satisfies all 8 clauses.

Python validation script

# Positive example (4 clauses)
def one_in_three(x, clause):
    return sum(x[i] for i in clause) == 1

solutions = []
for bits in range(64):
    x = {i+1: (bits >> i) & 1 for i in range(6)}
    clauses = [[1,2,3], [4,5,6], [1,5,3], [2,4,6]]
    if all(one_in_three(x, c) for c in clauses):
        solutions.append(tuple(x[i] for i in range(1,7)))
assert len(solutions) == 5
assert (1,0,0,0,0,1) in solutions
print(f"Positive: {len(solutions)}/64 satisfying")

# Negative: add clauses until unsatisfiable
extra = [[1,2,4], [3,4,5], [1,6,5], [2,5,6]]
all_clauses = [[1,2,3], [4,5,6], [1,5,3], [2,4,6]] + extra
neg_count = 0
for bits in range(64):
    x = {i+1: (bits >> i) & 1 for i in range(6)}
    if all(one_in_three(x, c) for c in all_clauses):
        neg_count += 1
assert neg_count == 0
print(f"Negative (8 clauses): {neg_count}/64 satisfying (correct)")

[isPANN]

Issue Quality Check — Model

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but no companion [Rule] OneInThreeKSatisfiability to ILP issue linked despite claiming ILP solvability
Non-trivial	✅ Pass	Distinct feasibility constraint (exactly-one) from existing KSatisfiability (at-least-one) and NAESatisfiability (not-all-equal)
Correctness	❌ Fail	Complexity bound O(1.0984^n) cites Wahlström (2007) but this paper is from 2005, covers general SAT with low occurrences, and the bound is not established for 1-in-3 SAT specifically
Well-written	❌ Fail	Multiple issues: failed example attempts left in body, missing Expected Outcome section, confusing naming, no ILP companion issue linked

Overall: 1 passed, 1 warning, 2 failed

---

Usefulness

The problem does not yet exist in the reduction graph (pred show OneInThreeKSatisfiability returns not found). Two planned reductions are mentioned (3SAT → OneInThree, OneInThree → Generalized Satisfiability), which is good.

However, the "How to solve" section checks "It can be solved by reducing to integer programming" but does not link a companion [Rule] OneInThreeKSatisfiability to ILP issue. Per the check-issue policy, claiming ILP solvability requires linking a direct [Rule] companion issue.

Non-trivial

This is a genuinely distinct problem from existing models:

• KSatisfiability requires at least one true literal per clause.
• NAESatisfiability requires not all literals to have the same value.
• OneInThree requires exactly one true literal per clause — a strictly different feasibility constraint.

The relationship to NAE-SAT (noted in the Specialization section) is also correct: a 1-in-3 solution implies NAE-SAT satisfaction but not vice versa.

Correctness

Schaefer (1978) reference: Correct. Schaefer's paper establishes NP-completeness of One-in-Three 3SAT, and the claim that it remains NP-complete without negated literals is accurate.

Wahlström complexity claim: Incorrect on multiple counts.

1. The paper is from 2005 (SAT 2005, LNCS vol. 3569), not 2007.
2. The paper title is "Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable" — it addresses general SAT with restricted variable occurrences, not 1-in-3 SAT specifically.
3. The claimed bound of O(1.0984^n) for 1-in-3 SAT is not verified in this paper. The paper's results are parameterized by the maximum number of occurrences per variable, not by problem type.
4. No independent source confirms O(1.0984^n) as the best exact algorithm for 1-in-3 SAT.

The only dedicated exact algorithm paper found for 1-in-3 SAT is Bonnet & Paschos (2013, arXiv:1307.5776) claiming O*(1.260^n), but it was withdrawn by the authors noting "better results already known." The actual best bound for 1-in-3 SAT needs proper literature research.

Recommendation: The complexity section should cite a verified algorithm specifically for 1-in-3 SAT, or use the general SAT bound of O(1.307^n) for 3-SAT (since any 3-SAT algorithm can solve 1-in-3 SAT by modifying the acceptance criterion, though this is not tight).

Well-written

Failed items:

1. Messy example section: The body contains two failed solution attempts with crossed-out checks (C₃: 0 true ✗, C₄: 2 true ✗) before arriving at a revised instance. Failed attempts should be removed — the issue body should present only the final, correct example.

2. Missing Expected Outcome section: The issue template requires an explicit "Expected Outcome" section. For a satisfaction problem, this means stating the satisfying assignment and explaining why it is valid. The solution is embedded in the example text but not in a dedicated section.

3. Confusing naming: The proposed name OneInThreeKSatisfiability implies a K-parameterized family (like KSatisfiability<K3>), but the definition restricts to exactly k=3. If this is meant to generalize to "One-in-K K-SAT", the definition should say so. If it is only for k=3, the name should be OneInThreeSatisfiability (without the K).

4. No ILP companion issue linked: The "How to solve" section claims ILP solvability but does not link a [Rule] OneInThreeKSatisfiability to ILP issue in a "Reduction Rule Crossref" section.

5. Complexity expression missing: The Complexity section provides a prose description but not a concrete complexity expression in terms of problem parameters (e.g., 1.0984^num_variables). The template requires this.

Final example verification: The final 4-clause instance over 6 variables is correct and has 5 satisfying assignments out of 64 total, which provides adequate complexity for round-trip testing. The "non-obvious structure" note is a nice touch.

Recommendations

• Remove the failed example attempts and present only the final correct instance cleanly.
• Research and cite a verified complexity bound specifically for 1-in-3 SAT (or explicitly fall back to the 3-SAT bound with justification).
• Clarify whether the "K" in the name is meant to generalize beyond k=3; if not, drop it.
• Create and link a companion [Rule] OneInThreeKSatisfiability to ILP issue.
• Add a dedicated "Expected Outcome" section.

[isPANN]

Fix-issue changelog

• Title/Name: Renamed OneInThreeKSatisfiability → OneInThreeSatisfiability (K was confusing since problem is fixed at k=3).
• Complexity: Removed incorrect Wahlström (2007) O(1.0984^n) claim — that paper covers general SAT with low occurrences, not 1-in-3 SAT. Replaced with conservative 3-SAT bound O*(1.307^n) (Scheder & Steinberger 2017).
• Example: Removed two failed solution attempts (C3: 0 true ✗, C4: 2 true ✗). Kept only the clean 4-clause instance with verified solution. Added negative example (8 clauses, 0/64 satisfying).
• Motivation: Rewrote with concrete context about Schaefer's dichotomy theorem.
• Associated rules: Linked rule [Rule] 3SAT to ONE-IN-THREE 3SAT #862 (3SAT → OneInThreeSatisfiability).
• ILP: Added companion rule note with ILP formulation description (l1+l2+l3=1 per clause).
• Added Python validation script verifying both positive (5/64) and negative (0/64) cases.

Applied by /fix-issue.