[Rule] ConjunctiveQueryFoldability to Satisfiability

Source

ConjunctiveQueryFoldability, without variant parameters. Let the disjoint
term sets be constants D, distinguished variables X, and undistinguished
variables Y, of sizes d,x,u. Write R=d+x+u. Terms are encoded as zero-based
indices in the concatenation (D,X,Y). Each relation has a fixed arity,
possibly zero. The atom lists Q1=(A1,...,Ap), Q2=(B1,...,Bq) allow duplicates.

A source witness is a substitution σ:Y→D∪X∪Y fixing constants and
distinguished variables, such that the set of atoms σ(Q1) equals the set
of atoms Q2. Apply the substitution once; do not recursively substitute a
resulting term in Y. Idempotence and retraction are not required by the
current evaluator.

The concrete solution is a vector of exactly u encoded term indices, with
value Or. This proposal preserves the actual exact-image predicate and
does not equate it with query containment or historical retraction folding.

Target

Satisfiability, without variant parameters: unrestricted CNF, signed
one-based literal indices, Boolean-vector witnesses, and value Or.
Completed feasibility values map identically. Decode only after validating
the entire target witness once.

Motivation

The direct CNF expresses both directions of atom-set coverage, while retaining
one-step substitution, repeated atoms, repeated variable occurrences, and
nullary relations. Candidate compression avoids enumeration of a potentially
huge declared constant domain.

The source model is #448,
with an incoming rule in #463
and implementation in PR #687.
Those contributions are acknowledged. No dedicated outgoing source-to-SAT
proposal was located in the 4,700-record all-state public-history capture
dated 2026-10-13. The baseline graph had no witness path between these exact
endpoints. These are bounded project-history findings, not worldwide novelty.

The standard one-hot and equivalence-clause techniques are not claimed as new.
Maintainers must assess the usefulness and nontriviality of the complete
exact-image encoding and its domain compression. An outgoing SAT route does
not establish NP-hardness of the source.

Reference

Ashok K. Chandra and Philip M. Merlin, Optimal Implementation of Conjunctive
Queries in Relational Data Bases, STOC 1977, pp. 77–90,
DOI 10.1145/800105.803397,
primary PDF.

The folding definition on p. 81, Theorem 11 on p. 82, and homomorphism Lemma 13
on p. 83 were read during the mathematical investigation. The paper's folding
definition uses a retraction fixing its image. The repository evaluator instead
uses the exact-image, one-step predicate stated above. The reference supplies
context and exposes that semantic boundary; it is not cited as a theorem for
this different predicate. The self-contained proof below certifies the latter.

Reduction Algorithm

1. Let C be the sorted list of distinct encoded terms occurring in Q2,
   additionally containing term 0 when R>0. Write c=|C|.
   For R=0, C is empty and u=0.
2. Allocate uc selectors e_(y,t), ordered by variable y, then candidate t.
   For each y, add one clause containing all its selectors and each pairwise
   clause (¬e_(y,t)∨¬e_(y,s)), t<s. Exactly one candidate is chosen per variable.
3. Allocate pq match bits z_(i,j) after the selectors, source-atom-major.
   A pair is incompatible if relation symbols differ, a fixed source argument
   differs from its target argument, or repeated occurrences of one source
   undistinguished variable require different target terms. Add (¬z_(i,j))
   for an incompatible pair.
4. For each compatible pair, collect the distinct required selectors, one per
   undistinguished variable appearing in Ai, in source-variable order.
   Encode z_(i,j) ↔ AND(required selectors) by (¬z_(i,j)∨e) for every
   requirement e, and one clause containing z_(i,j) and the negations of all
   requirements. With no requirements, the latter is the positive unit z_(i,j).
5. Add a row cover OR_j z_(i,j) for each source atom and a column cover
   OR_i z_(i,j) for each target atom. An empty disjunction is an empty,
   false clause.
6. Validate the complete target witness. For each y, read its unique true
   selector and return that candidate's encoded term, in source order.

Compression lemma. In any exact-image source witness, every variable
occurring in Q1 maps to a term of Q2, since that term occurs in its image atom.
A variable absent from Q1 can be changed to term 0 without affecting any atom.
Such a variable implies u>0, hence R>0 and term 0 is legal. Thus every source
YES instance has a witness using only C. Conversely every candidate is a
legal source term.

Forward. Compress a source witness as in the lemma, set its one-hot
selectors, and set z_(i,j) exactly when σ(Ai)=Bj. Incompatible pairs are
unequal; compatible equality is precisely the conjunction of required
selectors. Exact equality of the two atom sets makes every row and column
cover true. The resulting CNF assignment is feasible.

Backward. A satisfying CNF chooses one legal image per source variable.
The match equivalences force each z_(i,j) to mean exactly σ(Ai)=Bj: fixed
arguments agree, repeated arguments are consistent, and every other equality
is the specified selector. Row covers imply every source image belongs to
Q2; column covers imply every target atom occurs in the image. Therefore the
atom sets are equal. Duplicates do not change this reasoning. Extraction
returns the defined substitution, without recursive substitution or repair.

Corners. Both queries empty give a feasible formula with free one-hot
choices for unused variables. Exactly one query empty, with the other nonempty,
gives an empty cover clause and is infeasible. Nullary equal atoms use positive
match units. Different relation symbols, conflicting repeated arguments, and
unequal constants/distinguished variables use negative match units. A legal
swap of two undistinguished variables need not be idempotent.

Size Overhead

A compatible match requiring k_(i,j)≤u distinct selectors has k_(i,j)+1
clauses and 3k_(i,j)+1 literal occurrences. An incompatible match has one
clause and one literal. One-hot blocks contribute u(1+c(c−1)/2) clauses
and uc² literals. Covers contribute p+q clauses and 2pq literals.

Source parameter names are domain_size, num_distinguished,
num_undistinguished, num_conjuncts_q1, and num_conjuncts_q2.
Registry formulas substitute their sum for R and use exact signed integer
arithmetic, including the zero product at R=0.

For a very large legal source universe, these theoretical upper bounds can
exceed the registry's u64 output range even when candidate compression gives
a tiny valid target. Evaluating such metadata returns the typed
OutputOutOfRange result; it does not invalidate the constructed target or
the mathematical bound.

The actual construction loops over C, whose size is at most one plus the
target argument-occurrence count, rather than over all R possible terms.
Match construction scans the explicit atom arguments. Time and output size
are polynomial in the explicit queries and the declared explicit witness
dimension u, with term-index comparisons charged by their bit length.

Encoding limitation. This is not a polynomial-size claim in log(u)
alone. A binary declaration of arbitrarily many unused undistinguished
variables still requires exactly u source coordinates under the existing
Vec<usize> model and uc selectors in this rule. Compressing the term domain
does not compress witness coordinates. A stronger succinct-input claim would
require a separate source-model/witness representation change.

Numeric contract. Source construction and loading reject d+x+u overflow
before evaluation. The rule checks selector/match counts and signed SAT
literal-index representability. Unsupported machine sizes return typed
construction/reduction errors, never false infeasibility. Large representable
constant domains are supported without domain enumeration.

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 general argument above establishes correctness. Finite checks search for
counterexamples and audit the concrete encoding.

• Constructor: 10,996 executions / 104,923 assertions, seed 2026101305;
  all seven sections passed. Complete unary query-list pairs of length at most
  two over a two-term universe and the four documented fixed/substitutable
  splits; 300 samples per (u=0,...,5,p+q=0,...,5). Includes repeated/nullary
  atoms, exact image, swaps, and large compressed term domains.
• Independent adversary, written only from the proof: 26,645 executions /
  294,561 assertions, seeds 2026101319/2026101320; two Hypothesis strategies
  with 300 examples each, database=None, deadline=None. It enumerated every
  satisfying target CNF witness in each audited instance with generic DPLL,
  with separate small raw Boolean-space checks.
• Cross-comparison: 108 targets and 108 complete solution sets identical
  modulo clause/literal order, unchanged variable indices and retained
  multiplicity; 188,185 forward checks, 5,400 feasibility comparisons
  and 39 cross-extractions; zero disagreements.
• Rust implementation and eight dedicated test functions are present (seven
  without example-db), covering the canonical witness, both image directions,
  repeated-argument conflicts, non-retractions, all tiny target assignments,
  malformed/unsatisfied witnesses, large implicit domains, count/literal guards,
  and canonical export. The ordinary test batches and separate doctest retry passed.

Counts are assertions and executions, not statistically independent samples.
All possible integer domains or all queries up to five variables were not
exhaustively enumerated.

Durable local evidence: proof,
constructor,
independent adversary,
cross-comparison, and the
consolidated certificate. Generated JSON reports are
local artifacts, not public certificate URLs.

Example

Use no constants, distinguished variable x, undistinguished variables u,v,a,
and one binary relation R. Encodings are x=0,u=1,v=2,a=3.

YES source.

Q1 = [R(x,u), R(u,v), R(v,x), R(u,u)]
Q2 = [R(x,a), R(a,a), R(a,x)]

The substitution vector (3,3,3) maps the source atoms to
R(x,a),R(a,a),R(a,x),R(a,a), exactly the target set.
Candidates are C=(0,3). Selector bits are (0,1,0,1,0,1).
Match rows are (1,0,0), (0,1,0), (0,0,1), (0,1,0).
Concatenate them to obtain the complete 18-bit target witness:

[0,1,0,1,0,1, 1,0,0, 0,1,0, 0,0,1, 0,1,0]

Every row and column has a true bit. The target has 18 variables, 34 clauses
and 75 literals: one-hot blocks give 6 clauses / 12 literals; match blocks
21 / 39; covers 7 / 24. Extraction returns (3,3,3).

NO source. Keep Q1 and use

Q2 = [R(x,v), R(v,a), R(a,x)]

Every target atom has distinct arguments, while R(u,u) always substitutes
to an equal-argument atom. Its three matches are forced false, contradicting
its row cover. Both instances are NO. Candidates are C=(0,2,3), giving
21 variables, 39 clauses and 87 literals: one-hot 12 / 27, match blocks
20 / 36, covers 7 / 24.

The YES source and complete witness match the canonical Rust example and
are reproduced by the independent audits.

BibTeX

@inproceedings{ChandraMerlin1977ConjunctiveQueries,
  author = {Chandra, Ashok K. and Merlin, Philip M.},
  title = {Optimal Implementation of Conjunctive Queries in Relational Data Bases},
  booktitle = {Proceedings of the Ninth Annual ACM Symposium on Theory of Computing},
  pages = {77--90},
  year = {1977},
  doi = {10.1145/800105.803397},
  url = {https://www.cs.ubc.ca/~laks/cpsc504/chandra-merlin-1977.pdf}
}

Attribution and submission status

Responsible human contributor: Thiago Costa
(@ThiagoCAltoe). Codex AI agents assisted
discovery, proof drafting, implementation and independent automated checking.
Human scientific review is pending. Existing model contributors and
Chandra/Merlin are credited above. Maintainer acceptance, reserved priority,
worldwide novelty and coauthorship credit are not claimed.