[Rule] OneInThreeSatisfiability to SubsetProduct

Source

OneInThreeSatisfiability, with no variant parameters. The input has n Boolean variables and m clauses, each containing exactly three signed literal occurrences. Repetitions and both signs of a variable are permitted by the existing model. A solution makes exactly one occurrence true in every clause. Source solutions are Vec<bool> and the value is Or.

Target

SubsetProduct, with no variant parameters. Given an indexed list of positive integers and a positive target B, choose a subset of indices whose values multiply to B. Equal item values remain distinct indexed choices. Both source and target have Boolean-vector solutions and Or values; completed feasibility maps identically. Products use the existing arbitrary-precision positive integer representation.

Motivation

A direct arithmetic encoding separates two obligations: one truth choice per variable, and exactly one true occurrence per clause. It handles negation and repeated occurrences directly, without composing an intermediate model or solver.

The source model was introduced in #861, which already discusses its direct ILP route; that route is not claimed here. The existing ExactCoverBy3Sets→SubsetProduct rule, #858, also uses prime products. Its implementation has one item per triple. The proposed rule adds variable-consistency pairs and signed occurrence multiplicities. No dedicated proposal for the present endpoints was found in the all-state issues/PR snapshot captured on 2026-10-13.

This is evidence about the project's catalog, not a claim of global novelty. The shared prime technique is a material risk to separate nontriviality credit; maintainers should assess that question explicitly.

Reference

The direct reduction below is proved by unique factorization and does not depend on an unread reduction theorem. The source model cites Thomas J. Schaefer, The Complexity of Satisfiability Problems, STOC 1978, 216–226, DOI 10.1145/800133.804350. The publisher metadata was identified, but the full text was not obtained in this audit; it is background, not asserted as the source of this exact transformation. The related project rule #858 is credited above.

Reduction Algorithm

Take the first n+m primes, starting with 2. Assign distinct primes p_i to variables and q_j to clauses. Let ν⁻_{ji} and ν⁺_{ji} count the negative and positive occurrences of variable i in clause j.

1. For each variable, create two indexed items, in false/true order:

   a_(i,0) = p_i · ∏_j q_j^(ν⁻_(ji))
   a_(i,1) = p_i · ∏_j q_j^(ν⁺_(ji))
   

2. Set B = (∏_i p_i)(∏_j q_j).

3. After validating a target witness, return the selection bit of each true item: source bit i is target bit 2i+1 with zero-based item positions.

Forward proof. Select exactly the item matching each variable's truth value. Every variable prime occurs once. A clause prime occurs in the product once per true literal occurrence in that clause, hence exactly once. The product is B.

Backward proof. Suppose an indexed subset has product B. The prime p_i occurs in exactly its two variable items, once in each. Its exponent in B is one, so exactly one of those items was selected. These choices define an assignment. The exponent of q_j in the selected product is exactly the number of true literal occurrences in clause j; it must be one. Thus every clause is satisfied. This argument also covers duplicate literals, opposite signs in one clause, and unused variables.

Empty and repeated cases. With no variables and clauses the empty item list and B=1 are feasible. Without clauses, any assignment selects one of each private-prime pair. Equal-valued false/true items for an unused variable must stay separate indices. Literal multiplicity is retained as a prime exponent, not deduplicated.

Polynomial construction and arithmetic. The largest of the first k=n+m primes has O(log(k+2)) bits. A sieve or deterministic trial division generates them in time polynomial in k; the implementation uses arbitrary-precision candidates and trial divisors. The sum of factor multiplicities across all items is 2n+3m, and B has n+m factors. Ordinary exact multiplication therefore suffices for polynomial construction and output encoding. This is a bit-size claim, not a claim that item values are polynomially bounded numerically. Allocation counts 2n, n+m, and signed-literal/index conversions are checked.

The size convention includes the n declared variable coordinates. A succinct binary declaration of arbitrarily many unused variables would still require an explicit n-coordinate source witness and 2n indexed items; polynomial size in log n alone is not claimed.

Size Overhead

Only num_elements is a registered target parameter. Extraction scans the item choices and never factors an integer.

Validation Method

Local engineering checkpoint. Production code 650a8023 passed fmt,
complete clippy, 6,980 ordinary tests and 149 doctests in a separate retry.
The original Cargo command was interrupted by RAM exhaustion in doctest
compilation, not recorded as exit zero. Test-only HEAD a4b8cba0 changes no
production code and passed fresh fmt (4.566 s), clippy (45.973 s), and all
eight focused rule-05 tests. CLI round trips/default solve, four exporters,
full manual and topology passed. 89 new rule tests were measured below
five seconds: 88 earlier tests (maximum 4.7597 s including startup) plus
the allocation regression (0.017 s). Final new-production coverage PASS:
1,223/1,233 instrumented added lines, 99.189%; every rule exceeds 95%.
The audit excludes 814 added lines with no DA record explicitly; ten
instrumented lines remain uncovered. The focused instrumented extension
passed 8/8 tests. Human scientific review and maintainer approval remain
pending.

All mathematical counts below are local evidence. Proof sources, constructor,
independent adversarial and cross-check scripts are prepared locally and can
accompany a later implementation PR; they are not public certificate URLs.

The proof above covers all accepted mathematical instances. Finite tests supplement it as counterexample searches and implementation audits.

• Constructor audit: 11,382 instance executions, 291,900 assertions, seed 2026101303; all seven required sections passed. Includes signed and repeated literals, empty cases, source assignments, target subset enumeration, extraction, symbolic size checks, and products beyond fixed-width integer limits.
• Fresh-context adversary: 48,443 instance executions, 3,559,750 assertions, seeds 2026101309 and 2026101310, including two Hypothesis strategies of 300 examples each (database=None, deadline=None); zero failures. Its constructor, checker and decoder were written independently from the proof.
• Cross-comparison: 90 exactly identical targets, 24,552 subset-feasibility comparisons and 314 extractions; zero disagreements.
• Rust: 6 focused tests passed, 0 failed, 0.06 seconds; formatting passed. Branch contrib/one-in-three-subset-product, local commit 23b5f7cd. The existing source→ILP implementation only needed a qualified trait reference after adding a second target.

Assertion counts are not numbers of independent statistical samples. Durable local evidence: verification/algebra_oneinthree_constructor_report.json, corresponding constructor/proof/targets, adversary/adv_oneinthree_subsetproduct*, and verification/cross_algebra_round2_report.json, under research/coauthorship-2026-10-13/. These paths are local, not public artifact links.

Example

YES. Use clauses (x₁,x₂,x₃), (¬x₁,¬x₂,x₃), (x₁,¬x₂,¬x₃). Assignment (0,1,0) gives one true occurrence in each. Variable primes are (2,3,5) and clause primes (7,11,13).

The target is B=2·3·5·7·11·13=30030. Choose item vector (1,0,0,1,1,0): 22·21·65=30030. Extraction gives (0,1,0).

NO. Use (x₁,x₂,x₃) and (¬x₁,¬x₂,¬x₃). If t variables are true, these clauses simultaneously require t=1 and 3−t=1, impossible. Items are (22,14,33,21,55,35) and B=2310. A target product must choose one item per variable. Its exponents of 7 and 11 are then t and 3−t, which cannot both be one, so the target is also infeasible.

BibTeX

@inproceedings{Schaefer1978Satisfiability,
  author = {Schaefer, Thomas J.},
  title = {The Complexity of Satisfiability Problems},
  booktitle = {Proceedings of the Tenth Annual ACM Symposium on Theory of Computing},
  year = {1978},
  pages = {216--226},
  doi = {10.1145/800133.804350}
}

Attribution and submission status

Responsible human contributor: Thiago Costa (@ThiagoCAltoe). Codex AI agents assisted discovery, drafting, implementation and automated adversarial checking. Human scientific review is pending. This draft does not claim maintainer acceptance, reserved priority or earned coauthorship. Maintainers decide whether the direct signed-occurrence construction counts separately from the existing prime-product rule.