Repository navigation
Conversation
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Collaborator
Author
Verification certificateVerdict: verified. Two independently written scripts and a Typst proof agree; no counterexample found. Type resolution. Source Construction script (seed 2026110301, Hypothesis derandomized): 3,827,291 checks, 0 failures.
Instances: n = 1..5 variables. Exhaustive: every single clause (n <= 5), every ordered clause pair (n <= 3), clause-shape cases (n = 4). Sampled: 300 per (n, m) with m = 2..5, planted-satisfiable instances, plus large instances beyond 64 bits. 59,972 instances (40,039 YES, 19,933 NO). Every 2^(2n) selection is enumerated. Adversary script (written from the proof alone, seed 2026110304, Hypothesis 3 strategies x 300 examples, derandomize, no database, no deadline): 4,358,569 checks, 0 failures over 109,182 instances (52,115 YES, 57,067 NO).
Cross-comparison: 169,154 shared instances; identical targets (items in index order and B), identical witness sets (all 167,354 instances with n <= 5) and identical extractions (176,555 witnesses); 0 disagreements. The Rust rule was additionally compared against both scripts on 170 instances, 0 mismatches. Mutation testing: 26 mutants of construction, checker and extraction; the adversary kills 26/26, the construction script 24/26 (the two survivors are a 64-bit-overflow mutant, which needs the large instances, and unvalidated extraction, covered by the Rust unit tests). Typst proof#set page(margin: 2cm)
#set text(size: 10.5pt)
#let thm(body) = block(inset: 8pt, stroke: 0.5pt, width: 100%)[#body]
= OneInThreeSatisfiability $arrow.r$ SubsetProduct
*Provenance.* Derived here. The nearest library rule, ExactCoverBy3Sets $arrow.r$ SubsetProduct, uses the same device (one prime per constraint, unique factorization) but has one item per set; this rule adds a private prime per variable that forces one of two items per variable, and signed occurrence counts as prime exponents. No cited source states this exact construction.
*Type resolution.* Source `OneInThreeSatisfiability`: `Solution = Vec<bool>` of length $n$, `Value = Or` (`src/models/formula/one_in_three_satisfiability.rs`); `evaluate` rejects a wrong length and otherwise returns whether every clause has exactly one true literal occurrence. Target `SubsetProduct`: `Solution = Vec<bool>` of length equal to the number of items, `Value = Or` (`src/models/misc/subset_product.rs`); sizes and target are arbitrary-precision `BigUint`, all sizes and the target positive. `Or` $arrow.r$ `Or` with the identical solution type: witness-compatible, the identity aggregate mapping applies.
*Redundancy.* `pred path OneInThreeSatisfiability SubsetProduct --limit all` reports no path, so the rule is novel (PASS). Existing outgoing edges of the source: only to ILP.
#thm[*Theorem.* Let $F$ have $n$ variables and $m$ clauses, each clause a triple of nonzero signed literals $ell in {plus.minus 1, dots, plus.minus n}$ (repeats and both signs of a variable allowed). The SubsetProduct instance below is feasible iff $F$ has an assignment making exactly one literal occurrence true in every clause, and a target witness maps to such an assignment.]
== Construction
+ Let $pi_1 < pi_2 < dots$ be the primes starting at $2$. Put $p_i = pi_i$ for $i = 1..n$ (variable primes) and $q_j = pi_(n+j)$ for $j = 1..m$ (clause primes). All $n+m$ primes are distinct.
+ For variable $i$ and clause $j$ let $nu^-_(j i)$ be the number of positions of clause $j$ holding the literal $-i$, and $nu^+_(j i)$ the number holding $+i$ (multiplicity counted).
+ For each variable $i$ create two items, in this index order (zero-based positions $2(i-1)$ and $2(i-1)+1$):
$ a_(i,0) = p_i dot product_j q_j^(nu^-_(j i)) quad ("false item"), quad a_(i,1) = p_i dot product_j q_j^(nu^+_(j i)) quad ("true item"). $
Items with equal value remain distinct indices.
+ The target is $B = (product_i p_i)(product_j q_j)$, the product of the first $n+m$ primes ($B=1$ if $n=m=0$).
== Overhead
#table(columns: 3, [Target quantity], [Formula], [Status],
[`num_elements`], [$2n$], [exact, every input including $n=0$],
[prime factors in all items, with multiplicity], [$2n + 3m$], [exact (not a registered parameter)],
[prime factors of $B$], [$n + m$], [exact],
[encoding size], [$O((n+m) log(n+m+2))$ bits], [bound])
The first count: each item holds one $p_i$ ($2n$ in total), and every clause has three literal positions, each adding one factor $q_j$ to exactly one item ($3m$ in total). The first $k = n+m$ primes are computed by trial division in time polynomial in $k$. Each has $O(log(k+2))$ bits and there are $2n+3m+n+m$ prime factors to write, giving the bit bound; individual values are not polynomially bounded numerically.
== Correctness
Let $S$ be a set of item indices, $x_i^S$ the number of selected items among ${a_(i,0), a_(i,1)}$. The product $P(S)$ of selected items has $p_i$-adic valuation $x_i^S$, because $p_i$ divides only those two items (the only primes in any item are $p_i$ of its own variable and clause primes, all distinct).
*($arrow.r.double$) Satisfiable $arrow.r$ feasible.* Let assignment $alpha$ make exactly one occurrence true in every clause. Select $a_(i,1)$ if $alpha_i$ is true and $a_(i,0)$ otherwise. Each $p_i$ then appears exactly once. For clause $j$, the exponent of $q_j$ in $P(S)$ is the sum over $i$ of $nu^(alpha_i)_(j i)$ with sign chosen by $alpha_i$, which counts the occurrences in clause $j$ that are true under $alpha$ (an occurrence of $+i$ is true iff $alpha_i$ is true, and of $-i$ iff $alpha_i$ is false). That count is one, so $q_j$ appears exactly once. By unique factorization $P(S) = B$.
*($arrow.l.double$) Feasible $arrow.r$ satisfiable.* Let $P(S) = B$. The exponent of $p_i$ in $B$ is $1$, so $x_i^S = 1$: exactly one of the two items of every variable is selected. Define $alpha_i$ true iff $a_(i,1)$ is selected. No other items exist, so $S$ consists of these choices. The exponent of $q_j$ in $P(S)$ is, as computed above, the number of true occurrences in clause $j$ under $alpha$; it equals the exponent $1$ in $B$. So every clause has exactly one true occurrence. Repeated literals contribute their full multiplicity (a clause $(x,x,x)$ has count $3$ or $0$, never $1$), opposite signs of one variable contribute to the false and the true item respectively (exactly one of them is true), and unused variables contribute only their private prime.
== Solution extraction
Given a target witness $s in {0,1}^(2n)$ with product $B$ (validated first), return source bit $i$ equal to $s_(2i+1)$ (zero-based), i.e. whether the true item of variable $i$ is selected. By the ($arrow.l.double$) paragraph this is a satisfying assignment, and $s$ is recovered as $s_(2i)=not alpha_i$, $s_(2i+1)=alpha_i$. No integer is factored. The number of target witnesses equals the number of satisfying assignments.
== Special cases
- *Repeated literal in a clause*, e.g. $(x_1,x_1,x_1)$: exponent $3$ on the true item of $x_1$, $0$ on the false item; never exactly one, so correctly unsatisfiable. $(x_1,x_1,x_2)$ gives exponent $2$ for $x_1$ true.
- *Both signs in one clause*, e.g. $(x_1, not x_1, x_2)$: both items of $x_1$ carry $q_1^1$, so they are equal in value ($10 = 10$ for $n=2$) but remain two indices; the $x_1$ occurrences contribute exactly one true literal either way.
- *Unused variables*: the two items both equal $p_i$ and stay distinct indices; both choices give valid witnesses, matching the two free assignments.
- *No clauses* ($m=0$, $n >= 1$): items $(p_1,p_1,dots)$, $B = product p_i$; feasible, with $2^n$ witnesses.
- *Empty instance* ($n=m=0$): no items, $B=1$, the empty selection has product $1$, feasible; the source empty assignment satisfies the vacuous formula.
- A clause with $n=0$ cannot exist (literals need a variable), so $m>0$ implies $n>=1$.
== Example (YES)
Clauses $(x_1,x_2,x_3)$, $(not x_1, not x_2, x_3)$, $(x_1, not x_2, not x_3)$; $n=m=3$. Variable primes $(2,3,5)$, clause primes $(7,11,13)$.
#table(columns: 3, [Variable], [False item], [True item],
[$x_1$], [$2 dot 11 = 22$], [$2 dot 7 dot 13 = 182$],
[$x_2$], [$3 dot 11 dot 13 = 429$], [$3 dot 7 = 21$],
[$x_3$], [$5 dot 13 = 65$], [$5 dot 7 dot 11 = 385$])
$B = 2 dot 3 dot 5 dot 7 dot 11 dot 13 = 30030$. Item list $(22,182,429,21,65,385)$. The selection $(1,0,0,1,1,0)$ gives $22 dot 21 dot 65 = 30030 = B$. Extraction reads positions $1,3,5$: $(0,1,0)$. Check: clause 1 has only $x_2$ true, clause 2 has only $not x_1$ true, clause 3 has only $not x_3$ true. This is the only satisfying assignment and the only target witness (exhaustive check over all $2^6$ selections).
== Example (NO)
Clauses $(x_1,x_2,x_3)$, $(not x_1,not x_2,not x_3)$; $n=3$, $m=2$. Primes $(2,3,5)$, $(7,11)$. Items $(22,14,33,21,55,35)$ with $a_(1,0)=2 dot 11$, $a_(1,1)=2 dot 7$, $a_(2,0)=3 dot 11$, $a_(2,1)=3 dot 7$, $a_(3,0)=5 dot 11$, $a_(3,1)=5 dot 7$; $B = 2310$. Source: with $t$ variables true, clause 1 has $t$ true literals and clause 2 has $3-t$; $t=1$ and $3-t=1$ cannot hold together. Target: a product equal to $B$ must pick one item per variable; then the exponents of $7$ and $11$ are $t$ and $3-t$, which are not both $1$. All $2^6$ selections give a product different from $2310$, matching the infeasible source.
Construction script (Python)#!/usr/bin/env python3
"""Constructor verification: OneInThreeSatisfiability -> SubsetProduct.
Source: n variables, m clauses of exactly three nonzero signed literals (repeats and
both signs allowed); solution = Vec<bool> of length n; Or value = every clause has
exactly one true literal occurrence.
Target: SubsetProduct, positive integer items (indexed) + positive target B;
solution = Vec<bool> of length 2n; Or value = product of selected items == B.
Construction: p_i = i-th prime (i<n), q_j = (n+j)-th prime. Items 2i (false) and 2i+1
(true): p_i * prod_j q_j^{nu-/nu+}. B = prod p * prod q. Extraction: source bit i =
target bit 2i+1.
"""
import itertools
import random
import sys
from collections import Counter
import sympy
from sympy import Symbol, simplify, Sum, factorint
from hypothesis import given, settings, strategies as st, HealthCheck
SEED = 2026110301
random.seed(SEED)
counts = Counter()
fails = Counter()
failure_log = []
def check(section, cond, msg=""):
counts[section] += 1
if not cond:
fails[section] += 1
if len(failure_log) < 20:
failure_log.append(f"[{section}] {msg}")
# ---------------------------------------------------------------- semantics
def first_primes(k):
out, c = [], 2
while len(out) < k:
if all(c % p for p in out if p * p <= c):
out.append(c)
c += 1
return out
def lit_true(lit, a):
v = a[abs(lit) - 1]
return v if lit > 0 else not v
def src_eval(n, clauses, a):
"""Source Or value (exact semantics of is_one_in_three_satisfying)."""
assert len(a) == n
return all(sum(lit_true(l, a) for l in c) == 1 for c in clauses)
def valid_source(n, clauses):
return all(len(c) == 3 and all(l != 0 and abs(l) <= n for l in c) for c in clauses)
def reduce(n, clauses):
m = len(clauses)
pr = first_primes(n + m)
p, q = pr[:n], pr[n:]
items = []
for i in range(n):
for sign in (-1, +1):
v = p[i]
for j, c in enumerate(clauses):
nu = sum(1 for l in c if l == sign * (i + 1))
v *= q[j] ** nu
items.append(v)
B = 1
for x in pr:
B *= x
return items, B
def tgt_eval(items, B, sel):
assert len(sel) == len(items)
prod = 1
for x, s in zip(items, sel):
if s:
prod *= x
return prod == B
def all_subset_products(items):
k = len(items)
prod = [1] * (1 << k)
for mask in range(1, 1 << k):
low = mask & -mask
prod[mask] = prod[mask ^ low] * items[low.bit_length() - 1]
return prod
def bits(mask, k):
return [bool((mask >> t) & 1) for t in range(k)]
def extract(sel):
return [sel[2 * i + 1] for i in range(len(sel) // 2)]
# ------------------------------------------------------------ instance sets
def all_clauses(n):
lits = [l for v in range(1, n + 1) for l in (v, -v)]
return list(itertools.product(lits, repeat=3))
def instances():
yield 0, [] # empty instance
for n in range(1, 6):
yield n, [] # unused variables only
# exhaustive: every single clause for n <= 5
for n in range(1, 6):
for c in all_clauses(n):
yield n, [c]
# exhaustive: every ordered pair of clauses for n <= 3
for n in range(1, 4):
cl = all_clauses(n)
for c1 in cl:
for c2 in cl:
yield n, [c1, c2]
# sampled: >= 300 per (n, m) for 2 <= m <= 5 (n = 4, 5) and 3 <= m <= 5 (n <= 3)
for n in range(1, 6):
cl = all_clauses(n)
for m in range(2, 6):
if n <= 3 and m == 2:
continue
for _ in range(300):
yield n, [random.choice(cl) for _ in range(m)]
# satisfiable-biased samples: plant an assignment and pick one-true clauses
for n in range(3, 6):
for m in range(1, 6):
for _ in range(150):
a = [random.random() < 0.5 for _ in range(n)]
cs = []
while len(cs) < m:
c = random.choice(all_clauses(n))
if sum(lit_true(l, a) for l in c) == 1:
cs.append(c)
yield n, cs
# ------------------------------------------------------------------ sections
def section1_symbolic():
S = "1-symbolic"
n, m, i, j = sympy.symbols("n m i j", integer=True, nonnegative=True)
# num_elements: two items per variable.
check(S, simplify(Sum(2, (i, 1, n)).doit() - 2 * n) == 0, "num_elements = 2n")
# Prime factors (with multiplicity) across items: each item has one p_i
# (2 per variable); clause exponents sum_i (nu-_ji + nu+_ji) = 3 per clause.
total = Sum(2, (i, 1, n)).doit() + Sum(3, (j, 1, m)).doit()
check(S, simplify(total - (2 * n + 3 * m)) == 0, "2n+3m")
check(S, simplify(Sum(1, (i, 1, n)).doit() + Sum(1, (j, 1, m)).doit() - (n + m)) == 0, "n+m in B")
# bit-size: log2 of sum of log2 of the (n+m)-th prime bound (p_k < k(ln k + ln ln k) for k>=6)
# concrete check of per-instance identities with sympy.factorint below
for nn, mm in [(0, 0), (1, 1), (3, 3), (5, 2), (4, 0)]:
if nn == 0 and mm > 0:
continue
cl = [tuple(random.choice([-1, 1]) * random.randint(1, nn) for _ in range(3)) for _ in range(mm)]
items, B = reduce(nn, cl)
omega = sum(sum(factorint(x).values()) for x in items)
check(S, omega == 2 * nn + 3 * mm, "sympy factorint Omega total")
check(S, sum(factorint(B).values()) == nn + mm if B > 1 else nn + mm == 0, "Omega(B)")
check(S, len(items) == 2 * nn, "len")
# the clause-exponent identity nu- + nu+ summed over variables equals 3, for all
# clause shapes (exhaustive, n=4)
for c in all_clauses(4):
tot = sum(sum(1 for l in c if abs(l) == v) for v in range(1, 5))
check(S, tot == 3, "occurrence count 3")
def section2_equivalence(insts):
S = "2-forward+backward"
n_yes = n_no = 0
for n, cl in insts:
check(S, valid_source(n, cl), "generator produced invalid source")
items, B = reduce(n, cl)
k = 2 * n
prods = all_subset_products(items)
tgt_feasible = any(prods[mask] == B for mask in range(1 << k))
# Cross-check against tgt_eval on the witnesses
src_sat = [a for a in itertools.product([False, True], repeat=n) if src_eval(n, cl, list(a))]
check(S, tgt_feasible == bool(src_sat), f"feasibility differs n={n} cl={cl}")
n_yes += bool(src_sat)
n_no += not src_sat
# forward: every satisfying assignment maps to the selection of matching items
for a in src_sat:
mask = 0
for ii, v in enumerate(a):
mask |= 1 << (2 * ii + (1 if v else 0))
check(S, prods[mask] == B, f"forward fails {n} {cl} {a}")
# backward + counting: number of target witnesses == number of satisfying assignments
wit = [mask for mask in range(1 << k) if prods[mask] == B]
check(S, len(wit) == len(src_sat), f"witness count {len(wit)} vs {len(src_sat)}")
check(S, n_yes > 1000 and n_no > 1000, f"coverage yes={n_yes} no={n_no}")
print(f" (YES instances {n_yes}, NO instances {n_no})")
def section3_extraction(insts):
S = "3-extraction"
for n, cl in insts:
items, B = reduce(n, cl)
k = 2 * n
prods = all_subset_products(items)
for mask in range(1 << k):
if prods[mask] != B:
continue
sel = bits(mask, k)
check(S, tgt_eval(items, B, sel), "witness evaluation")
for i in range(n):
check(S, sel[2 * i] != sel[2 * i + 1], f"exactly one of pair {i}")
a = extract(sel)
check(S, src_eval(n, cl, a), f"extracted not satisfying n={n} cl={cl} sel={sel}")
# extraction is injective on witnesses and re-encoding returns the witness
re = []
for v in a:
re += [not v, v]
check(S, re == sel, "re-encode")
# wrong-length / non-witness rejection model: a non-witness must not evaluate true
for mask in random.sample(range(1 << k), min(8, 1 << k)):
if prods[mask] != B:
check(S, not tgt_eval(items, B, bits(mask, k)), "non-witness accepted")
def section4_sizes(insts):
S = "4-sizes"
for n, cl in insts:
m = len(cl)
items, B = reduce(n, cl)
pr = first_primes(n + m)
check(S, len(items) == 2 * n, "num_elements = 2n")
fb = factorint(B) if B > 1 else {}
check(S, fb == {p: 1 for p in pr}, f"B is the product of the first n+m primes n={n} m={m}")
omega = 0
for idx, x in enumerate(items):
f = factorint(x)
omega += sum(f.values())
i, t = divmod(idx, 2)
check(S, f.get(pr[i], 0) == 1, "variable prime exponent 1")
for j, c in enumerate(cl):
want = sum(1 for l in c if l == (i + 1) * (1 if t else -1))
check(S, f.get(pr[n + j], 0) == want, "clause prime exponent = occurrence count")
check(S, set(f) <= {pr[i]} | set(pr[n:]), "no foreign primes")
check(S, omega == 2 * n + 3 * m, "total factor count 2n+3m")
# bit size of the encoding: O((n+m) log(n+m+2)); explicit bound
bitsz = sum(x.bit_length() for x in items) + B.bit_length()
pmax = pr[-1] if pr else 2
check(S, bitsz <= (2 * n + 3 * m + n + m + 1) * pmax.bit_length(), "bit-size bound")
def section5_structure(insts):
S = "5-structure"
for n, cl in insts:
m = len(cl)
items, B = reduce(n, cl)
pr = first_primes(n + m)
check(S, all(x >= 1 for x in items) and B >= 1, "positive")
check(S, len(set(pr)) == n + m, "distinct primes")
for i in range(n):
holders = [idx for idx, x in enumerate(items) if x % pr[i] == 0]
check(S, holders == [2 * i, 2 * i + 1], "p_i divides exactly its two items")
for j in range(m):
q = pr[n + j]
tot = 0
for i in range(n):
for t in (0, 1):
x = items[2 * i + t]
e = 0
while x % q == 0:
x //= q
e += 1
tot += e
# each literal occurrence adds one to one item: false/true items together
# carry exactly the three occurrences of the clause
check(S, tot == 3, "clause prime total exponent 3 across items")
# per variable: false and true item exponents of q_j sum to the variable's occurrences
if n > 0 and m > 0:
for i in range(n):
for j, c in enumerate(cl):
q = pr[n + j]
ef = ep = 0
x, y = items[2 * i], items[2 * i + 1]
while x % q == 0:
x //= q
ef += 1
while y % q == 0:
y //= q
ep += 1
check(S, ef + ep == sum(1 for l in c if abs(l) == i + 1), "occurrence split")
# special cases, asserted explicitly (cannot be satisfied by accident)
items, B = reduce(3, [(1, 1, 1)]) # repeated literal: x1 x1 x1
check(S, items[0:2] == [2, 2 * 7 ** 3], "triple repeat exponent 3")
items, B = reduce(2, [(1, -1, 2)]) # both signs in one clause
q = first_primes(3)[2]
check(S, items == [2 * q, 2 * q, 3 * q, 3 * q][:0] + [2 * q, 2 * q, 3, 3 * q], "both signs: equal-valued items stay indexed")
check(S, items[0] == items[1], "equal-valued false/true items for x1")
items, B = reduce(3, []) # unused variables, m = 0
check(S, items == [2, 2, 3, 3, 5, 5] and B == 30, "unused variables: equal items kept separate")
items, B = reduce(0, [])
check(S, items == [] and B == 1, "empty instance")
check(S, tgt_eval(items, B, []) is True, "empty instance feasible (empty product 1)")
def section6_yes():
S = "6-YES example"
n, cl = 3, [(1, 2, 3), (-1, -2, 3), (1, -2, -3)]
items, B = reduce(n, cl)
check(S, items == [22, 182, 429, 21, 65, 385], f"items {items}")
check(S, B == 30030, "B = 30030")
# assignment (0,1,0): x1 false, x2 true, x3 false -> items 0,3,4 (vector (1,0,0,1,1,0))
sel = [True, False, False, True, True, False]
check(S, tgt_eval(items, B, sel), "22*21*65 = 30030")
check(S, 22 * 21 * 65 == 30030, "arithmetic")
check(S, extract(sel) == [False, True, False], "extraction (0,1,0)")
check(S, src_eval(n, cl, [False, True, False]), "source satisfied")
# all satisfying assignments agree with all target witnesses
prods = all_subset_products(items)
wit = [bits(mk, 6) for mk in range(64) if prods[mk] == B]
sat = [list(a) for a in itertools.product([False, True], repeat=3) if src_eval(n, cl, list(a))]
check(S, sorted(extract(w) for w in wit) == sorted(sat), "witness set matches satisfying set")
check(S, len(sat) == 1, "unique satisfying assignment")
def section7_no():
S = "7-NO example"
n, cl = 3, [(1, 2, 3), (-1, -2, -3)]
items, B = reduce(n, cl)
check(S, items == [22, 14, 33, 21, 55, 35], f"items {items}")
check(S, B == 2310, "B = 2310")
check(S, not any(src_eval(n, cl, list(a)) for a in itertools.product([False, True], repeat=3)), "source infeasible")
prods = all_subset_products(items)
check(S, not any(prods[mk] == B for mk in range(64)), "target infeasible")
# reason: with t true variables exponents of 7 and 11 are t and 3-t
for mk in range(64):
sel = bits(mk, 6)
if all(sel[2 * i] != sel[2 * i + 1] for i in range(3)):
t = sum(sel[2 * i + 1] for i in range(3))
x = prods[mk]
e7 = e11 = 0
while x % 7 == 0:
x //= 7
e7 += 1
while x % 11 == 0:
x //= 11
e11 += 1
check(S, e7 == t and e11 == 3 - t, "exponents t and 3-t")
check(S, not (e7 == 1 and e11 == 1), "cannot both be one")
def hypothesis_section():
S = "2-hypothesis"
lit = st.integers(min_value=1, max_value=6).flatmap(lambda v: st.sampled_from([v, -v]))
# strategy 1: arbitrary instances, literals drawn freely (n=6 allowed; repeats common)
s1 = st.integers(min_value=1, max_value=6).flatmap(
lambda n: st.tuples(
st.just(n),
st.lists(
st.tuples(*[st.integers(1, n).flatmap(lambda v: st.sampled_from([v, -v]))] * 3).map(tuple),
min_size=0, max_size=5,
),
)
)
# strategy 2: planted-satisfiable instances (one true literal per clause under a hidden assignment)
@st.composite
def planted(draw):
n = draw(st.integers(1, 6))
a = draw(st.lists(st.booleans(), min_size=n, max_size=n))
m = draw(st.integers(0, 5))
cl = []
for _ in range(m):
for _try in range(200):
c = tuple(draw(st.integers(1, n)) * draw(st.sampled_from([1, -1])) for _ in range(3))
if sum(lit_true(l, a) for l in c) == 1:
cl.append(c)
break
return n, cl, a
@settings(max_examples=300, deadline=None, database=None,
suppress_health_check=list(HealthCheck), derandomize=True)
@given(s1)
def run1(inst):
n, cl = inst
items, B = reduce(n, cl)
prods = all_subset_products(items)
wit = [mk for mk in range(1 << (2 * n)) if prods[mk] == B]
sat = [a for a in itertools.product([False, True], repeat=n) if src_eval(n, cl, list(a))]
check(S, len(wit) == len(sat), "hyp1 witness count")
for mk in wit:
check(S, src_eval(n, cl, extract(bits(mk, 2 * n))), "hyp1 extraction")
@settings(max_examples=300, deadline=None, database=None,
suppress_health_check=list(HealthCheck), derandomize=True)
@given(planted())
def run2(inst):
n, cl, a = inst
# a satisfies every clause by construction when all were found
if all(sum(lit_true(l, a) for l in c) == 1 for c in cl) and len(cl) > 0:
items, B = reduce(n, cl)
sel = []
for v in a:
sel += [not v, v]
check(S, tgt_eval(items, B, sel), "hyp2 planted assignment maps to witness")
check(S, extract(sel) == list(a), "hyp2 extraction")
# flipping one variable's choice breaks the pair constraint or a clause
for i in range(n):
sel2 = list(sel)
sel2[2 * i], sel2[2 * i + 1] = sel2[2 * i + 1], sel2[2 * i]
ok = src_eval(n, cl, extract(sel2))
check(S, tgt_eval(items, B, sel2) == ok, "hyp2 flip agrees with source")
run1()
run2()
def main():
insts = list(instances())
print(f"seed {SEED}; {len(insts)} instances")
section1_symbolic()
print("section 1 done")
section2_equivalence(insts)
print("section 2 done")
section3_extraction(insts)
print("section 3 done")
section4_sizes(insts)
print("section 4 done")
section5_structure(insts)
print("section 5 done")
section6_yes()
section7_no()
hypothesis_section()
total = 0
for s in sorted(counts):
print(f" {s}: {counts[s]} checks, {fails[s]} failures")
total += counts[s]
for line in failure_log:
print("FAIL", line)
nf = sum(fails.values())
print(f"TOTAL: {total} checks, {nf} failures")
sys.exit(1 if nf else 0)
if __name__ == "__main__":
main()Adversary script (Python)#!/usr/bin/env python3
"""Independent adversary for OneInThreeSatisfiability -> SubsetProduct (issue 1201).
Written from the proof alone (the other script not consulted). Own prime
generator (sieve), own reduce / extract, own source and target checkers.
Instance format: (n, clauses) with clauses a list of 3-tuples of nonzero ints in
[-n, n] \\ {0}. Target format: (items: list[int], B: int).
Run: python3 <this script> [--quick]
Ends with "TOTAL: <checks> checks, <failures> failures".
"""
import itertools
import math
import random
import sys
import time
from collections import Counter, defaultdict
SEED = 2026110304
CHECKS = Counter()
FAILS = Counter()
FAIL_EXAMPLES = defaultdict(list)
def check(section, cond, detail=""):
CHECKS[section] += 1
if not cond:
FAILS[section] += 1
if len(FAIL_EXAMPLES[section]) < 5:
FAIL_EXAMPLES[section].append(detail() if callable(detail) else detail)
# ---------------------------------------------------------------- primitives
def sieve_primes(k):
"""First k primes via a growing sieve of Eratosthenes."""
if k == 0:
return []
limit = 16
while True:
flags = bytearray([1]) * (limit + 1)
flags[0] = flags[1] = 0
for p in range(2, int(limit ** 0.5) + 1):
if flags[p]:
flags[p * p :: p] = bytearray(len(flags[p * p :: p]))
ps = [i for i in range(limit + 1) if flags[i]]
if len(ps) >= k:
return ps[:k]
limit *= 2
def is_valid_source(n, clauses):
return n >= 0 and all(
len(c) == 3 and all(isinstance(l, int) and l != 0 and abs(l) <= n for l in c)
for c in clauses
)
def source_ok(n, clauses, assign):
"""OneInThreeSatisfiability.evaluate: length must match; exactly one true occurrence per clause."""
if len(assign) != n:
raise ValueError("wrong assignment length")
return all(count_true(c, assign) == 1 for c in clauses)
def count_true(clause, assign):
"""Number of true literal occurrences of a clause under an assignment."""
t = 0
for l in clause:
v = assign[abs(l) - 1]
t += (v if l > 0 else not v)
return t
def target_ok(items, B, sel):
"""SubsetProduct.evaluate: length must match; product of selected == B."""
if len(sel) != len(items):
raise ValueError("wrong selection length")
prod = 1
for x, s in zip(items, sel):
if s:
prod *= x
return prod == B
def reduce(n, clauses, primes=None):
"""Construction steps 1-4 of the proof."""
primes = primes or globals()["sieve_primes"]
assert is_valid_source(n, clauses)
m = len(clauses)
pr = primes(n + m)
p, q = pr[:n], pr[n:]
items = []
for i in range(1, n + 1):
f = p[i - 1]
t = p[i - 1]
for j, c in enumerate(clauses):
nu_minus = sum(1 for l in c if l == -i)
nu_plus = sum(1 for l in c if l == i)
f *= q[j] ** nu_minus
t *= q[j] ** nu_plus
items += [f, t]
B = math.prod(pr)
return items, B
def extract(items, B, sel):
"""Validate the witness, then source bit i = sel[2i+1]."""
if not target_ok(items, B, sel):
raise ValueError("not a target witness")
return [bool(sel[2 * i + 1]) for i in range(len(items) // 2)]
def raises(fn, *args):
try:
fn(*args)
except ValueError:
return True
return False
def encode(assign):
sel = []
for a in assign:
sel += [not a, bool(a)]
return sel
def subset_products(items):
"""prods[mask] = product of items[k] for bit k of mask set."""
prods = [1]
for x in items:
prods = prods + [v * x for v in prods]
return prods
def mask_to_sel(mask, k):
return [bool((mask >> b) & 1) for b in range(k)]
def all_sat(n, clauses):
return [list(a) for a in itertools.product([False, True], repeat=n) if source_ok(n, clauses, list(a))]
def factor_over(x, primes):
"""Exponent vector of x over the given primes, and the cofactor."""
if x <= 0: # not a positive integer: no valid factorization
return [0] * len(primes), x
exps = []
for p in primes:
e = 0
while x % p == 0:
x //= p
e += 1
exps.append(e)
return exps, x
# ---------------------------------------------------------------- per-instance battery
def battery(n, clauses, reduce_fn=None, extract_fn=None, tag="exh"):
"""Forward/backward equivalence, extraction, witness bijection, overhead, structure."""
reduce_fn = reduce_fn or globals()["reduce"]
extract_fn = extract_fn or globals()["extract"]
m = len(clauses)
items, B = reduce_fn(n, clauses)
k = len(items)
# --- overhead (section 4)
check("4 overhead", k == 2 * n, lambda: f"num_elements {k} != 2n for {n},{clauses}")
pr = sieve_primes(n + m)
total_mult = 0
exps_all = []
for x in items:
e, cof = factor_over(x, pr)
exps_all.append(e)
total_mult += sum(e)
check("5 structure", cof == 1 and x > 0, lambda: f"item {x} not over first n+m primes {n},{clauses}")
check("4 overhead", total_mult == 2 * n + 3 * m, lambda: f"factor count {total_mult} != 2n+3m {n},{clauses}")
eB, cofB = factor_over(B, pr)
check("4 overhead", cofB == 1 and eB == [1] * (n + m), lambda: f"B={B} not squarefree product of first n+m primes")
# encoding bit-size bound O((n+m) log(n+m+2)): sum of item bits <= (2n+3m) * bits(max prime) + k
if pr:
bitbound = (2 * n + 3 * m) * pr[-1].bit_length() + k
check("4 overhead", sum(x.bit_length() for x in items) <= bitbound, "item bits exceed bound")
check("4 overhead", B.bit_length() <= (n + m) * pr[-1].bit_length(), "B bits exceed bound")
# --- structure (section 5): exact exponents and private variable prime
for i in range(1, n + 1):
for side in (0, 1):
e = exps_all[2 * (i - 1) + side]
check("5 structure", e[i - 1] == 1 and all(e[v] == 0 for v in range(n) if v != i - 1),
lambda: f"item {2*(i-1)+side} var-prime exponents {e[:n]}")
for j, c in enumerate(clauses):
want = sum(1 for l in c if l == (i if side else -i))
check("5 structure", e[n + j] == want,
lambda: f"item ({i},{side}) q_{j} exponent {e[n+j]} != {want} in {clauses}")
# --- equivalence (section 2): enumerate every target selection
prods = subset_products(items)
tw = [mask for mask, v in enumerate(prods) if v == B]
sats = all_sat(n, clauses)
check("2 equivalence", (len(tw) > 0) == (len(sats) > 0),
lambda: f"feasibility mismatch {n},{clauses}: src {len(sats)} tgt {len(tw)}")
# forward: every satisfying assignment's encoding is a witness
for a in sats:
check("2 equivalence", target_ok(items, B, encode(a)), lambda: f"forward fails {a} {clauses}")
# backward: every witness picks one item per variable and decodes to a satisfying assignment
check("2 equivalence", len(tw) == len(sats),
lambda: f"#witnesses {len(tw)} != #sat {len(sats)} {n},{clauses}")
wset = set()
for mask in tw:
sel = mask_to_sel(mask, k)
check("2 equivalence", all(sel[2 * i] + sel[2 * i + 1] == 1 for i in range(n)),
lambda: f"witness not one-per-variable {sel}")
# --- extraction (section 3)
try:
a = extract_fn(items, B, sel)
except ValueError:
check("3 extraction", False, f"extract rejected witness {sel}")
continue
check("3 extraction", len(a) == n and source_ok(n, clauses, a),
lambda: f"extracted {a} not satisfying {clauses}")
check("3 extraction", encode(a) == sel, lambda: f"encode(extract(s)) != s for {sel}")
wset.add(tuple(sel))
check("3 extraction", wset == {tuple(encode(a)) for a in sats}, "witness set != encoded satisfying set")
# extraction rejects non-witnesses (sample a few)
rng = random.Random(hash((n, tuple(map(tuple, clauses)))) & 0xFFFF)
for _ in range(3):
mask = rng.randrange(len(prods))
if prods[mask] != B:
check("3 extraction", raises(extract_fn, items, B, mask_to_sel(mask, k)),
f"extract accepted non-witness {mask}")
check("3 extraction", raises(extract_fn, items, B, [False] * (k + 1)), "extract accepted wrong length")
return len(sats) > 0
# ---------------------------------------------------------------- instance families
def all_clauses(n):
lits = [l for v in range(1, n + 1) for l in (v, -v)]
return list(itertools.product(lits, repeat=3))
def exhaustive_instances():
yield 0, []
for n in range(1, 6):
yield n, []
for n in range(1, 6):
for c in all_clauses(n):
yield n, [c]
for n in range(1, 4):
cl = all_clauses(n)
for c1 in cl:
for c2 in cl:
yield n, [c1, c2]
cl = all_clauses(2)
for trip in itertools.combinations_with_replacement(cl, 3):
yield 2, list(trip)
def random_clause(rng, n, pool=None):
vs = pool or list(range(1, n + 1))
return tuple(rng.choice(vs) * rng.choice((1, -1)) for _ in range(3))
def planted(rng, n, m):
a = [rng.random() < 0.5 for _ in range(n)]
cls = []
while len(cls) < m:
c = random_clause(rng, n)
# generator's own truth count, so a mutated checker cannot stall instance generation
if sum((a[abs(l) - 1] if l > 0 else not a[abs(l) - 1]) for l in c) == 1:
cls.append(c)
return a, cls
def random_instances(rng, per=300):
for n in range(1, 7):
for m in range(1, 7):
for t in range(per):
if t % 3 == 0:
_, cls = planted(rng, n, m)
elif t % 3 == 1:
pool = rng.sample(range(1, n + 1), k=min(n, 2)) # heavy repetition, unused vars
cls = [random_clause(rng, n, pool) for _ in range(m)]
else:
cls = [random_clause(rng, n) for _ in range(m)]
yield n, cls
# ---------------------------------------------------------------- sections
def section1_symbolic():
import sympy as sp
n, m = sp.symbols("n m", integer=True, nonnegative=True)
i, j = sp.symbols("i j", integer=True, positive=True)
# items: 2 per variable
num_elements = sp.summation(2, (i, 1, n))
check("1 symbolic", sp.simplify(num_elements - 2 * n) == 0, "sum_i 2 != 2n")
# factor multiplicity: each item one p_i (2n), each clause 3 positions each in exactly one item
total = sp.summation(2, (i, 1, n)) + sp.summation(3, (j, 1, m))
check("1 symbolic", sp.simplify(total - (2 * n + 3 * m)) == 0, "factor count != 2n+3m")
check("1 symbolic", sp.simplify(sp.summation(1, (i, 1, n)) + sp.summation(1, (j, 1, m)) - (n + m)) == 0,
"B factor count")
# per-variable item exponent balance: nu^- + nu^+ summed over variables = 3 per clause
a, b, c = sp.symbols("a b c", integer=True, nonnegative=True)
check("1 symbolic", sp.simplify((a + b + c) - 3).subs({a: 1, b: 1, c: 1}) == 0, "3 positions")
# prime number theorem bound: pi_k <= k(ln k + ln ln k) for k >= 6 -> bits O(log k)
for kk in [6, 10, 100, 1000, 5000]:
pk = sieve_primes(kk)[-1]
check("1 symbolic", pk <= kk * (math.log(kk) + math.log(math.log(kk))), f"Rosser bound fails k={kk}")
# sympy prime() agrees with our sieve
ps = sieve_primes(300)
for idx in range(1, 301):
check("1 symbolic", sp.prime(idx) == ps[idx - 1], f"prime({idx})")
def section_large(rng):
"""Big instances: forward with planted assignment, extraction, and single-bit flips fail."""
for n, m in [(40, 60), (120, 200), (300, 500)]:
for _ in range(3):
a, cls = planted(rng, n, m)
items, B = reduce(n, cls)
check("4 overhead", len(items) == 2 * n)
check("4 overhead", B.bit_length() > 64, "expect beyond fixed width")
s = encode(a)
check("2 equivalence", target_ok(items, B, s), "planted forward fails (large)")
check("3 extraction", extract(items, B, s) == a, "large extraction")
for _ in range(20):
b = rng.randrange(2 * n)
s2 = list(s)
s2[b] = not s2[b]
check("2 equivalence", not target_ok(items, B, s2), "single flip still product B")
def section6_yes():
n = 3
cls = [(1, 2, 3), (-1, -2, 3), (1, -2, -3)]
items, B = reduce(n, cls)
check("6 YES", sieve_primes(6) == [2, 3, 5, 7, 11, 13])
check("6 YES", items == [22, 182, 429, 21, 65, 385], f"items {items}")
check("6 YES", [2 * 11, 2 * 7 * 13, 3 * 11 * 13, 3 * 7, 5 * 13, 5 * 7 * 11] == items)
check("6 YES", B == 30030 == 2 * 3 * 5 * 7 * 11 * 13, f"B {B}")
sel = [True, False, False, True, True, False]
check("6 YES", 22 * 21 * 65 == 30030 and target_ok(items, B, sel))
check("6 YES", extract(items, B, sel) == [False, True, False])
check("6 YES", all_sat(n, cls) == [[False, True, False]], "unique satisfying assignment")
prods = subset_products(items)
check("6 YES", [mk for mk, v in enumerate(prods) if v == B] == [0b011001], "unique witness")
# prose: clause 1 only x2 true; clause 2 only not x1; clause 3 only not x3
a = [False, True, False]
def truths(c):
return [(a[abs(l) - 1] if l > 0 else not a[abs(l) - 1]) for l in c]
check("6 YES", truths(cls[0]) == [False, True, False])
check("6 YES", truths(cls[1]) == [True, False, False])
check("6 YES", truths(cls[2]) == [False, False, True])
battery(n, cls)
def section7_no():
n = 3
cls = [(1, 2, 3), (-1, -2, -3)]
items, B = reduce(n, cls)
check("7 NO", items == [22, 14, 33, 21, 55, 35], f"items {items}")
check("7 NO", items == [2 * 11, 2 * 7, 3 * 11, 3 * 7, 5 * 11, 5 * 7])
check("7 NO", B == 2310)
check("7 NO", all_sat(n, cls) == [], "source should be unsat")
prods = subset_products(items)
check("7 NO", len(prods) == 64 and all(v != 2310 for v in prods), "some selection hits 2310")
# argument: t true -> clause1 count t, clause2 count 3-t
for a in itertools.product([False, True], repeat=3):
t = sum(a)
c1, c2 = count_true(cls[0], list(a)), count_true(cls[1], list(a))
check("7 NO", c1 == t and c2 == 3 - t and not (c1 == 1 and c2 == 1))
# exponents of 7, 11 in the one-per-variable selection
prod = math.prod(items[2 * i + int(a[i])] for i in range(3))
e, _ = factor_over(prod, [7, 11])
check("7 NO", e == [t, 3 - t], f"exponents {e} for t={t}")
battery(n, cls)
def section_special_cases():
S = "5 structure"
# (x1,x1,x1): exponent 3 on true item, 0 on false item; unsat
items, B = reduce(1, [(1, 1, 1)])
check(S, items == [2, 2 * 3 ** 3], f"(x1,x1,x1) items {items}")
check(S, all_sat(1, [(1, 1, 1)]) == [] and all(v != B for v in subset_products(items)))
items, B = reduce(1, [(-1, -1, -1)])
check(S, items == [2 * 3 ** 3, 2])
# (x1,x1,x2): exponent 2 for x1 true
items, B = reduce(2, [(1, 1, 2)])
e, _ = factor_over(items[1], [5])
check(S, e == [2], f"(x1,x1,x2) true item exponent {e}")
# (x1,-x1,x2) with n=2: both items of x1 equal 10
items, B = reduce(2, [(1, -1, 2)])
check(S, items[0] == items[1] == 10, f"both-sign items {items[:2]}")
sats = all_sat(2, [(1, -1, 2)])
check(S, sats == [[False, False], [True, False]], f"both-sign sats {sats}")
tw = [mk for mk, v in enumerate(subset_products(items)) if v == B]
check(S, len(tw) == 2, f"equal-valued items must stay distinct: {len(tw)} witnesses")
# unused variables: both items equal p_i
items, B = reduce(4, [(1, 2, 2)])
pr = sieve_primes(5)
check(S, items[4] == items[5] == pr[2] and items[6] == items[7] == pr[3], f"unused items {items}")
# no clauses: items (p1,p1,...), B = prod p, 2^n witnesses
for n in range(0, 7):
items, B = reduce(n, [])
pr = sieve_primes(n)
check(S, items == [p for p in pr for _ in (0, 1)] and B == math.prod(pr))
check(S, sum(v == B for v in subset_products(items)) == 2 ** n, f"m=0 witness count n={n}")
# empty instance
items, B = reduce(0, [])
check(S, items == [] and B == 1 and target_ok(items, B, []) and source_ok(0, [], []))
check(S, extract(items, B, []) == [])
# m>0 implies n>=1: no valid clause with n=0
check(S, not is_valid_source(0, [(1, 1, 1)]) and all_clauses(0) == [])
# invalid literals rejected (0 and out of range)
check(S, not is_valid_source(2, [(0, 1, 2)]) and not is_valid_source(2, [(1, 2, 3)]))
# source evaluate rejects wrong length
check(S, raises(source_ok, 2, [], [True]), "source accepted wrong length")
def hypothesis_section(n_examples=300):
from hypothesis import given, settings, strategies as st, HealthCheck
cfg = settings(max_examples=n_examples, deadline=None, database=None, derandomize=True,
suppress_health_check=list(HealthCheck))
# Strategy A: degenerate literal patterns -- repeats, both signs, few distinct variables.
@st.composite
def degenerate(draw):
n = draw(st.integers(1, 6))
used = draw(st.lists(st.integers(1, n), min_size=1, max_size=2, unique=True))
m = draw(st.integers(0, 6))
cls = []
for _ in range(m):
cls.append(tuple(draw(st.sampled_from(used)) * draw(st.sampled_from([1, -1])) for _ in range(3)))
return n, cls
# Strategy B: planted satisfiable at the 'exactly one' boundary, plus a perturbation that may
# turn one clause into a 0- or 2-true clause (boundary between YES and NO).
@st.composite
def boundary(draw):
n = draw(st.integers(1, 6))
a = draw(st.lists(st.booleans(), min_size=n, max_size=n))
m = draw(st.integers(1, 6))
cls = []
for _ in range(m):
trues = draw(st.integers(0, 3)) # number of true occurrences the clause should get
lits = []
for pos in range(3):
v = draw(st.integers(1, n))
want_true = pos < trues
sign = 1 if a[v - 1] == want_true else -1
lits.append(sign * v)
perm = draw(st.permutations(lits))
cls.append(tuple(perm))
return n, cls
# Strategy C: n up to 6 with unused trailing variables and possibly duplicate clauses.
@st.composite
def dup_clauses(draw):
n = draw(st.integers(1, 6))
base = draw(st.lists(st.tuples(*[st.integers(1, n).flatmap(
lambda v: st.sampled_from([v, -v]))] * 3), min_size=1, max_size=3))
reps = draw(st.lists(st.sampled_from(base), min_size=0, max_size=3))
return n, base + reps
counts = Counter()
for name, strat in [("A", degenerate()), ("B", boundary()), ("C", dup_clauses())]:
@cfg
@given(strat)
def run(inst):
n, cls = inst
counts[name] += 1
CHECKS["H hypothesis"] += 1
battery(n, cls, tag="hyp" + name)
run()
return counts
def safe_battery(n, cls, **kw):
try:
return battery(n, cls, **kw)
except Exception as e:
check("2 equivalence", False, f"battery crashed on {n},{cls}: {type(e).__name__}: {e}")
return False
def main():
quick = "--quick" in sys.argv
t0 = time.time()
rng = random.Random(SEED)
section1_symbolic()
n_inst = yes = 0
for n, cls in exhaustive_instances():
n_inst += 1
yes += safe_battery(n, cls)
n_exh = n_inst
for n, cls in random_instances(rng, per=60 if quick else 300):
n_inst += 1
yes += safe_battery(n, cls, tag="rand")
hc = {}
for name, fn in [("2 equivalence", lambda: section_large(rng)), ("5 structure", section_special_cases),
("6 YES", section6_yes), ("7 NO", section7_no),
("H hypothesis", lambda: hc.update(hypothesis_section(50 if quick else 300)))]:
try:
fn()
except Exception as e: # a crash is a failure of that section, not of the whole run
check(name, False, f"{fn} crashed: {type(e).__name__}: {e}")
print(f"instances: {n_inst} ({n_exh} exhaustive, {n_inst - n_exh} random), YES {yes}, NO {n_inst - yes}")
print(f"hypothesis examples per strategy: {dict(hc)}")
for sec in sorted(CHECKS):
print(f" {sec:16s} {CHECKS[sec]:>9d} checks {FAILS[sec]:>6d} failures")
for ex in FAIL_EXAMPLES[sec]:
print(f" e.g. {ex}")
print(f"seed {SEED}, {time.time() - t0:.1f} s")
total, fails = sum(CHECKS.values()), sum(FAILS.values())
print(f"TOTAL: {total} checks, {fails} failures")
return 1 if fails else 0
if __name__ == "__main__":
sys.exit(main()) |
Collaborator
Author
Agentic Review ReportSubject: rule The change adds two new files:
It edits five more:
Verdict: approve. There are no open findings. All five findings from the previous round are fixed. Structural and semantic
Quality
Feature test
FindingsNone open. |
1 similar comment
Collaborator
Author
Agentic Review ReportSubject: rule The change adds two new files:
It edits five more:
Verdict: approve. There are no open findings. All five findings from the previous round are fixed. Structural and semantic
Quality
Feature test
FindingsNone open. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1236 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151806 +248
========================================
+ Hits 147308 147557 +249
+ Misses 4250 4249 -1 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #1201
Adds the reduction
OneInThreeSatisfiability→SubsetProduct: one private prime per variable, one prime per clause, two items per variable (false/true) whose clause-prime exponents count the literal occurrences, and the target is the product of the first n + m primes.num_elements = 2 * num_vars; the identity aggregate mapping applies (Or → Or).assigned_primes/product_biguintandSubsetProduct::try_newmadepub(crate)for reuse, bodies unchangedoneinthreesatisfiability_ilp.rs: qualifiedtarget_constructioncall, needed once the source has a secondReduceToimpl🤖 Generated with Claude Code