[Rule] SubsetProduct to CircuitSAT

Source

SubsetProduct: positive arbitrary-precision integers a_1,...,a_n and a positive
target B. A configuration x in {0,1}^n is feasible exactly when the product of
the items with x_i=1 equals B. The empty product is 1. Empty item lists, repeated
items, and items equal to 1 are allowed. Positions remain independently
selectable even when their values are equal.

The source has Value=Or and Solution=Vec<bool>. Its registered parameter is
num_elements; it has no registered parameter for integer magnitude.

Target

CircuitSAT: a conjunction of Boolean assignment equations with named variables.
An equation equates its output bit to a Boolean expression. Repeated output names
impose simultaneous equations; they are not sequential overwrites. A witness
gives a bit for every name in the target's stored variable order.

The target has Value=Or and Solution=Vec<bool>. Its four size parameters are
num_variables, num_assignments, num_assignment_outputs, and
num_expression_nodes. Completed Or values map identically in this rule.

Motivation

This direct rule compiles positive integer subset multiplication to exact Boolean
arithmetic without factoring the input integers. The existing Factoring to
CircuitSAT rule is related: it constructs a multiplier for two unknown factors.
The proposed rule instead cascades multiplication by known constants and uses
one selector per item, including arbitrary-precision inputs.

At inspected base 875b6e86d5a87e5f66c2f6743be9d22abe917a09, the captured
pred path query returned no path from SubsetProduct to CircuitSAT. The
captured project issue/PR history contained no located claim for this pair.
Those observations are bounded by the captured project state. This proposal
does not claim worldwide originality or a new multiplication technique.

Reference

C. S. Wallace, A Suggestion for a Fast Multiplier, IEEE Transactions on
Electronic Computers EC-13(1):14-17, February 1964.
DOI: 10.1109/PGEC.1964.263830.
The primary full text
was read at pp. 14-15, especially “Lines of Approach”, “Addition”, and
“Generation of Summands”. These discuss multiplication through binary
summands and addition hardware. This is background for the arithmetic
technique; the paper is not being cited as the source of this exact selector
cascade or of the reduction proof below. Our construction uses ripple additions,
not Wallace's parallel adder tree.

Reduction Algorithm

Let ell(a)=floor(log_2(a))+1 for positive a, D=sum_i ell(a_i),
H=sum_i popcount(a_i), and W=max(1+D,ell(B)). All words have W little-endian
bits. Indices for stages, set-bit positions, bit columns, and gate kinds are
included in fresh names, so output names never collide accidentally.

1. Introduce n free selector bits x_i and W constant assignments forcing P_0=1.

2. For each i=1,...,n, compute T_i=P_(i-1)*a_i. Start accumulator A at the
   all-zero constant word. For each set-bit position j in a_i, in increasing
   order, add the word P_(i-1) shifted left by j to A. A shifted reference below
   bit zero is constant false. Each addition begins with carry false.

3. For every column with bits u,v and incoming carry c, emit these five fresh
   assignment outputs in order:

   h = u XOR v
   s = h XOR c
   f = u AND v
   g = h AND c
   d = f OR g
   

   Use s as the sum bit and d as the next carry. The last column's d remains
   constrained, although it is not propagated to a further column. After each
   addition, the new accumulator consists of the s outputs.

4. Introduce each P_i bit with one multiplexer assignment:

   P_(i,b) = (x_i AND T_(i,b)) OR ((NOT x_i) AND P_(i-1,b)).
   

5. Append W constant equations requiring P_n=B. These reuse P_n's output names.
   For n=0 they reuse the names of P_0, so the target is feasible exactly when
   B=1. Store each selector's coordinate in CircuitSAT::variable_names().

6. To extract, evaluate the entire target witness exactly once. Reject a
   malformed or unsatisfied assignment using a typed extraction error; otherwise
   return the selector coordinates in source order.

Full-adder lemma. For all eight triples u,v,c, the five equations have a
unique solution and satisfy u+v+c=s+2d. Hence each ripple row computes addition
modulo 2^W with a uniquely determined carry out.

No overflow, including unselected branches. Since every item is at least 1,
each selected prefix product is at most the product of all items in that prefix.
Every partial shifted accumulation at stage i is nonnegative and at most
P_(i-1)*a_i. This bound holds even if x_i=0 and the multiplication branch will
not be selected. When n>0, the product of all input items is strictly less than
2^D; when n=0 it is 1. All computed words therefore fit in W bits, every
discarded carry is zero, and modular wraparound cannot create a false witness.

Forward correctness. Given a feasible subset, set its selectors and evaluate
the fresh gates in construction order. The full-adder lemma and the arithmetic
bound make each multiplication exact. Starting at P_0=1, the multiplexers give
P_i=product_{t<=i, x_t=1} a_t. Thus P_n=B and all final equations hold.

Backward correctness. In any satisfying target witness, P_0=1 is forced.
Every subsequently allocated gate is a deterministic function of earlier wires
and selectors. Induction through the additions and multiplexers therefore forces
P_i to be the selected prefix product. The final equations force exact equality
with B in all W positions, so the projected selectors form a feasible source
subset. In particular, every satisfying target witness is the unique extension
of its selectors, not merely one extension selected by the constructor.

Binary complexity. Let L=D+ell(B)+n+1. Since H<=D, n<=D when n>0, and
W<=L, there are O(L^2) constant-size Boolean expression nodes. Names require
O(log L) bits each, so the explicit named encoding takes O(L^2 log L) bits.
Emitting the equations and sorting their names is polynomial; comparison sorting
of O(L^2) names gives the conservative bit-time bound O(L^2 log^2 L).
No prime factorization or exponential integer search is used.

Input and machine bounds. The mathematical domain includes all positive
arbitrary-precision integers. Rust stores magnitudes as BigUint, with no i64
or floating-point conversion. Width, popcount totals, emitted counts, expression
counts, and allocation-size arithmetic are checked. Unrepresentable machine
indices or sizes produce ReductionError::IntegerOverflow; failure to reserve
the target assignment buffer produces a typed target error. A construction error
does not claim mathematical infeasibility. Zero or negative magnitudes are
outside the source model's domain and are rejected by its constructor/loader.

Size Overhead

Every full-adder column has five new variables, five assignments, five assignment
outputs, and 15 expression-tree nodes. Each multiplexer has one new variable,
one assignment/output, and eight expression nodes. There are WH full-adder
columns, nW multiplexers, W initial constants, and W final constant constraints.

All four declarations have the explicit reason that bit lengths and popcounts
are not bounded by num_elements. These exact formulas do not justify a
registry formula in n alone: even one item can have arbitrarily many bits.

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 full-domain proof above is the correctness argument. Finite tests provide
counterexample search and implementation evidence; they do not replace the proof.

• Constructor audit: seed 2026101310; 3,983 instances and 78,186 checks, including
  11 symbolic, 11,955 size, 15,923 structure, 46,032 forward/backward, and 4,257
  extraction checks, plus four YES and four NO example checks.
• Independent adversary: implemented only from the proof, without access to the
  constructor or Rust implementation during that phase. Seed 2026101317;
  3,535 instances, 757 YES and 2,778 NO; 2,351,936 checks. These include
  581,884 branch-arithmetic checks, 63,494 forward checks, 63,494 no-overflow
  checks, 62,481 mutated-output checks, and 98,373 raw Cartesian checks.
• Exhaustive adversarial item lists over {1,2} for every n<=5 and B from 1 through
  2^n+1. Where larger magnitudes prevented exhaustive input enumeration, there
  were 300 random instances per n=1,...,5. Two distinct Hypothesis strategies
  each ran 300 examples (seeds 2026101317 and 2026101318), covering repeated
  factors/ones and sparse constants through 129 bits.
• Every feasible target assignment in every adversarial instance was enumerated
  using a separate expression-to-CNF translation and generic DPLL, and compared
  with arithmetic forward evaluation: 2,268 satisfying target witnesses checked.
  Raw Cartesian enumeration additionally covered circuits with at most 15 bits.
• Independent cross-comparison: seed 2026101323, 41 targets structurally identical
  modulo private variable renaming, 404 forward checks, 41 complete solution-set
  comparisons, 42 extraction checks, and 2,050 randomized feasibility checks.
  Zero disagreements. Constructor/adversary reports retain their historical
  “cross pending” labels; the later cross report establishes mathematical
  VERIFIED status.
• Rust commit 1866078865159c7e03bdfcc6bb2d11220b50aac0 adds the production
  reduction and 19 dedicated tests (18 without example-db). Tests construct all
  gate values directly without a target solver, exhaust small source configuration
  spaces, inspect unselected products and carries, and cover empty inputs, ones,
  129-bit items, wide unattainable targets, malformed witness lengths, each
  single-bit corruption of the canonical witness, dimension-overflow guards,
  registry metadata, aggregate recovery, and canonical export. The shared
  brute-force round-trip oracle is used only on tiny empty-source circuits.

Local evidence is under research/coauthorship-2026-10-13/: the proof
proofs/subsetproduct_circuit.typ, constructor
verification/subsetproduct_constructor.py, independent audit
adversary/adv_subsetproduct_circuit.py, their JSON reports, and
verification/cross_subsetproduct_circuit_report.json.

Example

YES source. Items (2,3,5), target B=30. Their bit lengths are (2,2,3),
so D=7; their popcounts are (1,2,2), so H=5; W=max(8,5)=8.

Construction and target. There are three selectors and four eight-bit product
words P_0,...,P_3. The five shifted additions contribute 585=200 gate outputs.
The 24 multiplexer assignments add three product words; eight constants set P_0,
and eight repeated-output constraints fix P_3. Therefore the measured target
has 235 variables, 240 assignments, 240 assignment outputs, and 808 expression
nodes, exactly matching the formulas.

With selectors (1,1,1), P_0=1 and the stage values are:

The final little-endian word is (0,1,1,1,1,0,0,0), the eight-bit representation
of 30. Every internal wire is determined by the five equations per adder column.
Reading the selector coordinates returns (1,1,1), whose source product is 30.
The canonical Rust example stores the complete 235-bit target witness; the
manual obtains its example data from the canonical example export.

NO source. Keep items (2,3,5) and set B=7. Width and all four measured counts
remain unchanged. The eight possible subset products are
{1,2,3,5,6,10,15,30}; none is 7. The final equations now demand little-endian
(1,1,1,0,0,0,0,0). By backward correctness every satisfying circuit would encode
one of the eight listed products, so this target has no satisfying witness.

Although the YES target has 235 variables, its three selectors permit only
eight deterministic gate extensions. The example is hand-checkable through
those eight subsets; enumerating all 2^235 raw target vectors is unnecessary.

BibTeX

@article{wallace1964fastmultiplier,
  author = {Wallace, C. S.},
  title = {A Suggestion for a Fast Multiplier},
  journal = {IEEE Transactions on Electronic Computers},
  volume = {EC-13},
  number = {1},
  pages = {14--17},
  month = feb,
  year = {1964},
  doi = {10.1109/PGEC.1964.263830}
}

Attribution and status

Responsible human contributor: Thiago Costa
(@ThiagoCAltoe). Codex AI agents assisted
discovery, proof drafting, implementation, independent counterexample search,
and cross-comparison. Human scientific review is pending. The classical
arithmetic technique and the existing Factoring circuit rule are credited
above. Maintainer acceptance, authorship credit, and worldwide novelty are not
claimed.