[Rule] BoyceCoddNormalFormViolation to Satisfiability

Source

BoyceCoddNormalFormViolation, with no variant parameters. Let A={0,…,N−1} be the attribute universe, F={(L_d,R_d)} a list of D functional dependencies, and R⊆A the nonempty target attribute set. The existing constructor normalizes each side and R, requires nonempty left sides, and permits empty right sides. For X⊆R, define X⁺ as the least set containing X and closed under F, using all attributes of A.

Find X⊆R such that both (X⁺\X)∩R and R\X⁺ are nonempty. These respectively give a newly determined target attribute and a target attribute not determined by X. Source solutions are Vec<bool> in normalized R order; the value is Or.

Target

Satisfiability, an unrestricted CNF with signed one-based literals, Vec<bool> solutions and Or values. Completed feasibility maps identically. The decoder validates the complete target witness before reading the original subset bits.

Motivation

This gives the existing database-normalization model a direct SAT route. The core difficulty is encoding the least functional-dependency closure, rather than an arbitrary closed superset that could invent a BCNF violation. Synchronous layers and bidirectional gate clauses make every closure bit determined by the chosen source subset.

The source model is #447, implemented in PR #685. Related AdditionalKey model #445 already sketches SAT closure, minimality and known-key exclusion. That idea is acknowledged and is not claimed as a separate contribution. Here the final predicate is simultaneous gain and missing closure membership, with no key minimality or known-key list. HittingSet→BCNF proposal #462 has different endpoints and direction.

No dedicated source→SAT proposal was found in the captured all-state issues/PR history as of 2026-10-13. Layered closure circuits and equivalence clauses are standard techniques, so maintainers must judge whether this direct application merits independent nontriviality credit.

Reference

The proof below establishes the reduction directly from the existing model's closure predicate. Historical model background: Catriel Beeri and Philip A. Bernstein, Computational Problems Related to the Design of Normal Form Relational Schemas, ACM TODS 4(1), 30–59 (1979), DOI 10.1145/320064.320066. Bibliographic metadata was identified, but the full text was not obtained in this audit. No unread theorem from that paper is used to certify this encoding, and no global novelty claim is made.

Reduction Algorithm

Let r=|R|. Allocate variables in this order:

1. Selection bits x_a for a∈R, in normalized target order.
2. Closure bits c_(t,a) for rounds t=0,…,N and every a∈A, round-major.
3. Dependency triggers g_(t,d) for t=0,…,N−1, dependency-major within each round.
4. Gain bits w_a for a∈R.

Initialize c_(0,a)↔x_a if a∈R, using two binary clauses; for a∉R, add unit ¬c_(0,a).

For every round t<N:

g_(t,d) ↔ ∧_(a∈L_d) c_(t,a)
c_(t+1,a) ↔ (c_(t,a) ∨ ∨_(d:a∈R_d) g_(t,d))

Encode g↔∧h_i by each (¬g∨h_i) and one (g∨¬h_1∨…∨¬h_k). Encode c↔∨h_i by each (¬h_i∨c) and one (¬c∨h_1∨…∨h_k). The closure disjunction always includes its previous-round bit, even if no dependency concludes the attribute.

Finally enforce w_a↔(¬x_a∧c_(N,a)) with (¬w_a∨¬x_a), (¬w_a∨c_(N,a)), (w_a∨x_a∨¬c_(N,a)). Add the two clauses ∨_(a∈R)w_a and ∨_(a∈R)¬c_(N,a).

Closure lemma. The initial clauses force precisely X. Given layer t, exact AND and OR equivalences uniquely force layer t+1 to be that set plus every dependency conclusion whose left side is contained in it. This is a monotone closure iteration. Each changing round adds at least one of the N attributes; once a round changes nothing, it is a fixed point. Therefore layer N equals the least closure X⁺. Attributes outside R must remain in the layers because they may mediate dependencies back into R.

Forward proof. For a source witness X, assign selection bits, all successive closure sets, all dependency trigger truths, and exact gain indicators. The closure and gate equations hold. The gained attribute supplies a true final w, and the missing attribute supplies a true negative final closure literal. Hence the CNF is satisfiable.

Backward proof. A satisfying assignment defines X by its selection bits. By the lemma its final layer is exactly X⁺. A true gain bit gives an attribute in (X⁺\X)∩R; the second final clause gives an attribute in R\X⁺. That attribute is also outside X by monotonicity. Thus X satisfies the source predicate. Auxiliary assignments cannot claim unsupported closure facts.

Extraction. After one full target-feasibility validation, return the first r bits. They are already in the source's normalized attribute order. No minimization, search, defaults or witness repair is performed.

Size Overhead

Write L=Σ_d|L_d| and B=Σ_d|R_d|, measured after constructor normalization.

Initialization contributes N+r clauses and N+3r literals. Each round contributes L+D / 3L+D for triggers and B+2N / 3B+4N for closure transitions. Gain gates contribute 3r / 7r; final clauses contribute 2 / 2r. Duplicate clauses remain counted, matching the target constructor.

The registry exposes N,D,r, not L,B. Since normalized sides satisfy L+B≤2ND, register the exact variable count and these upper bounds:

num_clauses  ≤ N+4r+N(2ND+D+2N)+2
num_literals ≤ N+12r+N(6ND+D+4N)

Pre-indexing dependencies by their concluded attributes gives construction time and storage O(N²+N(L+B+D)+r). This is polynomial under the explicit attribute-universe convention, not in log N alone for an arbitrarily large implicit unused universe. Allocation products and signed literal numbers are checked. Empty dependency lists and empty right sides are supported and yield the correct infeasibility when no gain is possible.

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.

Finite assertions are implementation audits and counterexample searches, not replacements for the closure proof.

• Constructor: 7,978 instance executions, 107,529 assertions, seed 2026101304; all seven sections passed, including forward/backward checks, extraction, sizes, malformed structural patterns and YES/NO examples.
• Independent fresh-context adversary: 4,731 instance executions, 89,174 assertions, seeds 2026101311 and 2026101312; two Hypothesis strategies with 300 examples each, database=None, deadline=None; zero failures.
• Cross-comparison: 100 targets identical after sorting clauses and literals, with identical variable indices; 458 forward checks, 5,000 target-checker comparisons and 7 cross-extractions, zero disagreements.
• Rust: 6 focused tests passed, 0 failed, 0.18 seconds, including 25 dependency families, a derivation through an attribute outside R, exhaustive small target vectors, malformed witness rejection and the canonical example. Initial implementation commit 295d3a14d99814d73433e771dc62c9eb52751b26, branch contrib/bcnf-sat.

Counts refer to assertions and instance executions, not independent statistical samples. Local durable evidence is under research/coauthorship-2026-10-13/: verification/algebra_bcnf_constructor_report.json, proof/constructor/targets, adversary/adv_bcnf_sat*, and verification/cross_algebra_round2_report.json. These are prepared artifacts, not public links.

Example

YES. Let N=4, F=({0}→{1},{1}→{2}), and R={0,1,3}. Choose X={0}, represented by (1,0,0).

• Closure layers, in attribute order 0,1,2,3: 1000, 1100, 1110, 1110, 1110.
• Trigger vectors: 10, 11, 11, 11.
• Gain bits in target order: 010. Attribute 1 is gained; attribute 3 is missing.

Concatenate the selection vector, the five closure layers, four trigger vectors and gain vector. This complete satisfying target vector has 34 bits. With L=B=D=2 and r=3, there are 74 clauses and 160 literal occurrences. Decoding the first three bits returns the source witness. Attribute 2 lies outside R and is correctly retained in the closure simulation.

NO. Let N=3, dependencies 0→1, 1→2, 2→0, and R={0,1,2}. For empty X, no attribute is gained. For every nonempty X, the closure is all of R, leaving no missing attribute. The target therefore fails one of its two final clauses for every assignment consistent with its closure gates. It has 27 variables, 62 clauses and 138 literal occurrences.

BibTeX

@article{BeeriBernstein1979NormalForms,
  author = {Beeri, Catriel and Bernstein, Philip A.},
  title = {Computational Problems Related to the Design of Normal Form Relational Schemas},
  journal = {ACM Transactions on Database Systems},
  year = {1979},
  volume = {4},
  number = {1},
  pages = {30--59},
  doi = {10.1145/320064.320066}
}

Attribution and submission status

Responsible human contributor: Thiago Costa (@ThiagoCAltoe). Codex AI agents assisted discovery, proof drafting, implementation and independent automated audits. Human scientific review is pending. No acceptance, reserved credit or earned coauthorship is asserted; maintainers decide nontriviality, including overlap with #445's closure-encoding idea.