Repository navigation
Conversation
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Collaborator
Author
Verification certificateVerdict: VERIFIED — BoyceCoddNormalFormViolation → Satisfiability (#1202). Type chain: Constructor script (seed 2026110301)676,968 checks, 0 failures. Exhaustive: N ≤ 3 with ≤ 2–3 dependencies × every R; N = 4 single dependency × every R; N = 5 single dependency × sampled R; 1,574 sampled instances up to N = 6;
Independent re-implementation (written from the proof only; never imports the constructor)3,245,636 checks, 0 failures over 39,036 instances, seed 20261103, run time 19 s. Exhaustive: N = 1 (D ≤ 3), N = 2 (D ≤ 3), N = 3 (D ≤ 2), N = 4 (D ≤ 1), each × every R (15 + 5,655 + 22,351 + 3,615 instances); random (N, D) ∈ {4}×{2,3,4}, {5}×{1..5}, {6}×{1,2,3,4,6}, 500 each (6,500); Claims tested: overhead formulas (exact variables, clause and literal upper bounds), closure lemma both halves, forward and backward direction, bijection between target models and source solutions, extraction (and rejection of bad lengths and non-models), special cases (no dependencies, all right sides empty, |R| = 1, duplicates, derivation through an attribute outside R), clause well-formedness, YES example (34 vars / 74 clauses / 160 literals, unique model, extracts to X = {0}) and NO example (27 / 62 / 138, unsatisfiable, source infeasible). Cross-comparison
Typst proof#set page(margin: 2cm)
#set heading(numbering: "1.")
#let ST = $"SAT"$
= BoyceCoddNormalFormViolation $->$ Satisfiability
*Provenance.* Derived here from the source model's closure predicate. Layered closure circuits with equivalence gates are a standard technique; issue \#445 (AdditionalKey) sketches the same closure encoding and is credited. No theorem of Beeri and Bernstein (ACM TODS 4(1), 1979, DOI 10.1145/320064.320066) is used. No existing library rule has the source as an endpoint.
*Type resolution.* Source: `BoyceCoddNormalFormViolation`, no variants, `Value = Or`, `Solution = Vec<bool>`, one bit per attribute of the normalized `target_subset` (`src/models/misc/boyce_codd_normal_form_violation.rs`). Target: `Satisfiability`, no variants, `Value = Or`, `Solution = Vec<bool>` over `num_vars` variables (`src/models/formula/sat.rs`). $"Or" -> "Or"$: compatible, so the aggregate mapping is the identity. `pred path BoyceCoddNormalFormViolation Satisfiability --limit all` reports no path, and `pred show` lists 0 outgoing and 0 incoming rules for the source: the rule is not dominated.
*Source instance.* Attributes $A = {0, dots, N-1}$; dependencies $F = ((L_d, R_d))_(d=0)^(D-1)$ with $L_d != emptyset$ and $R_d$ possibly empty, both sorted and deduplicated; target set $R subset.eq A$, non-empty, sorted, $r = |R|$. For $X subset.eq R$, $X^+$ is the least set containing $X$ and closed under $F$ over all of $A$. $X$ is a solution iff $(X^+ without X) inter R != emptyset$ and $R without X^+ != emptyset$. Put $L = sum_d |L_d|$ and $B = sum_d |R_d|$.
*Theorem.* The CNF $Phi$ below is satisfiable iff the source has a solution; the first $r$ variables of every satisfying assignment form a source solution, and the map from satisfying assignments to source solutions is a bijection.
== Construction
+ *Variables* (one-based, in this order): selection bits $x_a$, $a in R$ (numbers $1..r$, in sorted order of $R$); closure bits $c_(t,a)$ for $t = 0..N$ and $a in A$ (round-major); trigger bits $g_(t,d)$ for $t = 0..N-1$, $d = 0..D-1$ (round-major); gain bits $w_a$, $a in R$.
+ *Initial layer.* For $a in R$: clauses $(not c_(0,a) or x_a)$ and $(c_(0,a) or not x_a)$. For $a in.not R$: the unit $(not c_(0,a))$.
+ *Rounds.* For each $t = 0..N-1$:
- for each $d$ and each $a in L_d$: $(not g_(t,d) or c_(t,a))$; and the clause $(g_(t,d) or or.big_(a in L_d) not c_(t,a))$;
- for each $a in A$, with $H_(t,a) = {c_(t,a)} union {g_(t,d) : a in R_d}$: for each $h in H_(t,a)$ the clause $(not h or c_(t+1,a))$, and the clause $(not c_(t+1,a) or or.big_(h in H_(t,a)) h)$.
+ *Gain gates.* For each $a in R$: $(not w_a or not x_a)$, $(not w_a or c_(N,a))$, $(w_a or x_a or not c_(N,a))$.
+ *Final clauses.* $(or.big_(a in R) w_a)$ and $(or.big_(a in R) not c_(N,a))$.
Every gate is a full equivalence: $g_(t,d) <-> and.big_(a in L_d) c_(t,a)$, $c_(t+1,a) <-> c_(t,a) or or.big_(d : a in R_d) g_(t,d)$, $w_a <-> (not x_a and c_(N,a))$. Attributes outside $R$ keep all their layer bits, because a derivation may pass through them.
== Overhead
#table(columns: 3,
[target parameter], [formula], [kind],
[`num_vars`], [$N(N+1) + N D + 2r$], [exact],
[`num_clauses`], [$N + 4r + N(L + B + D + 2N) + 2 <= N + 4r + N(2 N D + D + 2N) + 2$], [exact in $L,B$; bound in $N,D,r$],
[`num_literals`], [$N + 12 r + N(3L + 3B + D + 4N) <= N + 12 r + N(6 N D + D + 4N)$], [exact in $L,B$; bound in $N,D,r$],
)
Derivation. Initial layer: $N + r$ clauses, $N + 3r$ literals ($4$ literals for each $a in R$, $1$ for the others). Per round, triggers: $L + D$ clauses, $3L + D$ literals (a trigger with $k$ conjuncts costs $k$ binary clauses and one of length $k+1$). Per round, transitions: attribute $a$ has $|H_(t,a)| = 1 + B_a$ with $sum_a B_a = B$, giving $(1 + B_a) + 1$ clauses and $2(1 + B_a) + (2 + B_a)$ literals, so $B + 2N$ clauses and $3B + 4N$ literals in total. Gain gates: $3r$ clauses, $7r$ literals. Final: $2$ clauses, $2r$ literals. Duplicates are counted. Normalized sides satisfy $L + B <= 2 N D$ (each side has at most $N$ elements), giving the bounds.
== Correctness
*Closure lemma.* Let $S_0 = X$ and $S_(t+1) = S_t union union.big_(d : L_d subset.eq S_t) R_d$. Any assignment satisfying the initial and round clauses, with $X = {a in R : x_a}$, has $c_(t,*) = S_t$ for every $t$ and uniquely determined triggers. _Proof by induction on $t$._ Layer 0 is forced by the initial clauses: $c_(0,a) = x_a$ on $R$ and false outside. If layer $t$ equals $S_t$, the two trigger clause kinds force $g_(t,d)$ true iff all of $L_d$ lies in $S_t$; the transition clauses force $c_(t+1,a)$ true iff $a in S_t$ or some $g_(t,d)$ with $a in R_d$ is true. This is $S_(t+1)$. The sequence $S_t$ is increasing and bounded by $A$; a round that adds nothing gives $S_(t+1) = S_t$, which then stays fixed. Each round that changes the set adds at least one of $N$ attributes, so $S_N$ is a fixed point containing $X$ and closed under $F$. Every element of $S_N$ is derived from $X$ by finitely many dependency applications, so $S_N$ is contained in every closed superset of $X$. Hence $S_N = X^+$, the least closure.
*(⇒) Source solution gives satisfying assignment.* Let $X$ be a solution. Set $x_a = [a in X]$, $c_(t,*) = S_t$, $g_(t,d) = [L_d subset.eq S_t]$, $w_a = [a in.not X and a in S_N]$. Every equivalence gate holds by the definitions, so all clauses of items 2 to 4 hold. Since $S_N = X^+$ there is $a in (X^+ without X) inter R$, for which $w_a$ is true, satisfying the first final clause. There is $b in R without X^+$, for which $c_(N,b)$ is false, satisfying the second final clause.
*(⇐) Satisfying assignment gives source solution.* Let an assignment satisfy $Phi$ and $X = {a in R : x_a}$. By the closure lemma $c_(N,*) = X^+$. The gain gates force $w_a = [a in.not X and a in X^+]$ for $a in R$. The first final clause gives $a in R$ with $w_a$ true, that is $a in (X^+ without X) inter R$. The second gives $b in R$ with $b in.not X^+$; since $X subset.eq X^+$, also $b in.not X$, so $b in R without X^+$. Hence $X$ is a solution. Because the lemma determines all auxiliary bits from $X$, distinct satisfying assignments have distinct selection bits: the map is a bijection onto the source solutions.
== Solution extraction
Check that the target witness has length equal to `num_vars` and satisfies every clause (one validation); then return its first $r$ bits, in the sorted order of $R$, which is the source's configuration order. No search, repair, or defaults. By (⇐) the result is a source solution.
== Special cases
- Empty dependency list ($D = 0$): no triggers; the layers copy $X$, so $X^+ = X$ and no gain is possible: both sides infeasible (target has $N(N+1) + 2r$ variables).
- Empty right sides: such a dependency has $B_d = 0$; its trigger is built but concludes nothing; no gain, infeasible if all right sides are empty.
- Derivation through an attribute outside $R$: attributes outside $R$ have layer bits (initially false) so the chain $a -> m -> b$ with $m in.not R$ is simulated.
- $X = emptyset$: all $L_d$ are non-empty, so no trigger can fire, $X^+ = emptyset$, and $w$ is all false: $X = emptyset$ is never a solution.
- $|R| = 1$: gain and miss would need two distinct attributes outside $X$ (or one gained and one missing), impossible for a single attribute: always infeasible.
- Duplicate dependencies and $L_d inter R_d != emptyset$ are accepted and counted in $L, B, D$.
- Fewer rounds would suffice ($N - |X|$); the construction keeps $N$ rounds.
== YES example
$N = 4$, $F = ({0} -> {1}, {1} -> {2})$, $R = {0, 1, 3}$, so $r = 3$, $D = 2$, $L = B = 2$. Take $X = {0}$, selection $(1,0,0)$. Closure layers over attributes $0,1,2,3$: $1000, 1100, 1110, 1110, 1110$. Triggers $(g_(t,0) g_(t,1))$ for $t = 0..3$: $10, 11, 11, 11$. Gains over $R$: $w = 010$ (attribute 1 is gained: $1 in X^+ without X$; attribute 3 is missing). The satisfying vector is $100 | 1000 1100 1110 1110 1110 | 10 11 11 11 | 010$, $34$ bits $= N(N+1) + N D + 2r = 20 + 8 + 6$. Clauses: $4 + 12 + 4 (2 + 2 + 2 + 8) + 2 = 74$; literals $N + 12 r + N(3L + 3B + D + 4N) = 4 + 36 + 4 dot 30 = 160$. Extraction returns $(1,0,0)$, i.e. $X = {0}$. Attribute 2 lies outside $R$ and is carried through the layers, it is not read by the extraction. The model count is 1 per source solution.
== NO example
$N = 3$, $F = ({0} -> {1}, {1} -> {2}, {2} -> {0})$, $R = {0,1,2}$, $r = 3$, $D = 3$, $L = B = 3$. For $X = emptyset$: $X^+ = emptyset$, every $w_a$ is false and the first final clause fails. For $X != emptyset$: the cycle gives $X^+ = {0,1,2} = R$, so every $c_(3,a)$ is true and the second final clause fails (and for $X = R$ also the first). By the closure lemma each of the 8 selections fixes all auxiliaries, so no assignment satisfies the CNF. Sizes: $12 + 9 + 6 = 27$ variables, $3 + 12 + 3(3 + 3 + 3 + 6) + 2 = 62$ clauses, $3 + 36 + 3(9 + 9 + 3 + 12) = 138$ literals.Constructor script#!/usr/bin/env python3
"""Constructor script: BoyceCoddNormalFormViolation -> Satisfiability (#1202).
Reduces a BCNF-violation instance to a CNF with an unrolled least-closure circuit.
Seven sections; ends with `TOTAL: <checks> checks, <failures> failures`.
Source semantics follow src/models/misc/boyce_codd_normal_form_violation.rs:
config = bits over sorted(R); value Or(exists y,z in R\\X with y in X+ and z not in X+).
Target semantics follow src/models/formula/sat.rs: signed one-based literals, Or value.
"""
import itertools, random, sys
from collections import defaultdict
import sympy as sp
from hypothesis import given, settings, strategies as st, HealthCheck
SEED = 2026110301
random.seed(SEED)
CHECKS = defaultdict(int)
FAILS = defaultdict(int)
MSGS = []
def check(section, cond, msg=""):
CHECKS[section] += 1
if not cond:
FAILS[section] += 1
if len(MSGS) < 20:
MSGS.append(f"[{section}] FAIL {msg}")
# ---------------------------------------------------------------- source model
def normalize(N, fds, R):
fds = [(sorted(set(l)), sorted(set(r))) for l, r in fds]
assert all(l for l, _ in fds) and R
assert all(0 <= a < N for l, r in fds for a in l + r)
R = sorted(set(R))
assert all(0 <= a < N for a in R)
return N, fds, R
def closure(X, fds):
c = set(X)
ch = True
while ch:
ch = False
for l, r in fds:
if all(a in c for a in l):
for a in r:
if a not in c:
c.add(a)
ch = True
return c
def src_eval(inst, bits):
N, fds, R = inst
assert len(bits) == len(R)
X = {R[i] for i, b in enumerate(bits) if b}
c = closure(X, fds)
gain = any(a not in X and a in c for a in R)
miss = any(a not in X and a not in c for a in R)
return gain and miss
def src_solutions(inst):
r = len(inst[2])
return [b for b in itertools.product([False, True], repeat=r) if src_eval(inst, list(b))]
# ---------------------------------------------------------------- reduction
def sizes_params(inst):
N, fds, R = inst
return N, len(fds), len(R), sum(len(l) for l, _ in fds), sum(len(r) for _, r in fds)
def var_layout(inst):
"""Return index maps (1-based variable numbers)."""
N, fds, R = inst
D, r = len(fds), len(R)
pos = {a: i for i, a in enumerate(R)}
x = {a: 1 + pos[a] for a in R}
base = r
c = {(t, a): base + 1 + t * N + a for t in range(N + 1) for a in range(N)}
base += (N + 1) * N
g = {(t, d): base + 1 + t * D + d for t in range(N) for d in range(D)}
base += N * D
w = {a: base + 1 + pos[a] for a in R}
base += r
return x, c, g, w, base
def reduce(inst, mutant=None):
"""Return (num_vars, clauses). `mutant` weakens the construction (used to show checks can fail)."""
N, fds, R = inst
D, r = len(fds), len(R)
x, c, g, w, nv = var_layout(inst)
rounds = N - 2 if mutant == "few_rounds" else N
rounds = max(rounds, 0)
cl = []
Rset = set(R)
for a in range(N):
if a in Rset:
cl.append([-c[0, a], x[a]])
cl.append([c[0, a], -x[a]])
else:
cl.append([-c[0, a]])
for t in range(N):
if t >= rounds:
# mutant only: leave later rounds copying the previous layer
for a in range(N):
cl.append([-c[t + 1, a], c[t, a]])
cl.append([c[t + 1, a], -c[t, a]])
for d in range(D):
cl.append([-g[t, d]])
continue
for d, (l, rr) in enumerate(fds):
gd = g[t, d]
for a in l:
cl.append([-gd, c[t, a]])
if mutant != "one_way_gate":
cl.append([gd] + [-c[t, a] for a in l])
for a in range(N):
hs = [g[t, d] for d, (l, rr) in enumerate(fds) if a in rr]
if mutant != "no_persist":
hs = [c[t, a]] + hs
if mutant == "drop_nonR" and a not in Rset:
hs = []
for h in hs:
cl.append([-h, c[t + 1, a]])
if mutant != "one_way_or":
cl.append([-c[t + 1, a]] + hs)
for a in R:
cl.append([-w[a], -x[a]])
if mutant != "w_no_closure":
cl.append([-w[a], c[N, a]])
cl.append([w[a], x[a], -c[N, a]] if mutant != "w_no_notx" else [w[a], -c[N, a]])
cl.append([w[a] for a in R])
if mutant != "no_missing_clause":
cl.append([-c[N, a] for a in R])
return nv, cl
def extract(inst, nv, cl, sol):
"""Validate the full target witness once, then return the first r bits."""
if len(sol) != nv or not sat_eval(cl, sol):
return None
return list(sol[: len(inst[2])])
def sat_eval(cl, sol):
return all(any((lit > 0) == sol[abs(lit) - 1] for lit in c) for c in cl)
# ---------------------------------------------------------------- independent SAT enumerator
def all_models(nv, cl, limit=None):
"""DPLL with unit propagation, enumerating all total models (decision order = index)."""
occ = defaultdict(list)
for i, c in enumerate(cl):
for lit in c:
occ[abs(lit)].append(i)
asg = [None] * (nv + 1)
models = []
def propagate(trail):
queue = list(range(len(cl)))
while queue:
i = queue.pop()
unassigned = None
nun = 0
sat = False
for lit in cl[i]:
v = asg[abs(lit)]
if v is None:
nun += 1
unassigned = lit
elif v == (lit > 0):
sat = True
break
if sat:
continue
if nun == 0:
return False
if nun == 1:
asg[abs(unassigned)] = unassigned > 0
trail.append(abs(unassigned))
queue.extend(occ[abs(unassigned)])
return True
def rec():
trail = []
ok = propagate(trail)
if ok:
v = next((i for i in range(1, nv + 1) if asg[i] is None), None)
if v is None:
models.append([bool(asg[i]) for i in range(1, nv + 1)])
else:
for val in (False, True):
asg[v] = val
rec()
asg[v] = None
for t in trail:
asg[t] = None
rec()
return models
# ---------------------------------------------------------------- instance families
def all_fds(N):
for lm in range(1, 1 << N):
L = [a for a in range(N) if lm >> a & 1]
for rm in range(1 << N):
yield (L, [a for a in range(N) if rm >> a & 1])
def instances_exhaustive():
# N<=3: every list of <=2 FDs (ordered, duplicates allowed) x every nonempty R.
for N in (1, 2, 3):
fl = list(all_fds(N))
Rs = [[a for a in range(N) if m >> a & 1] for m in range(1, 1 << N)]
lists = [()]
lists += [(f,) for f in fl]
if N <= 2:
lists += list(itertools.product(fl, repeat=2))
if N == 2:
lists += list(itertools.product(fl, repeat=3))
else:
lists += list(itertools.combinations_with_replacement(fl, 2))
for lst in lists:
for R in Rs:
yield normalize(N, list(lst), R)
# N=4: every single FD and every nonempty R; N=5: every single FD x a few R
for N, Rsel in ((4, None), (5, 6)):
fl = list(all_fds(N))
Rs = [[a for a in range(N) if m >> a & 1] for m in range(1, 1 << N)]
for f in fl:
for R in (Rs if Rsel is None else random.sample(Rs, Rsel)):
yield normalize(N, [f], R)
def rand_instance(rng, N, D, pL=0.35, pR=0.35):
fds = []
for _ in range(D):
L = [a for a in range(N) if rng.random() < pL] or [rng.randrange(N)]
Rr = [a for a in range(N) if rng.random() < pR]
fds.append((L, Rr))
R = [a for a in range(N) if rng.random() < 0.6] or [rng.randrange(N)]
return normalize(N, fds, R)
def sampled_instances():
rng = random.Random(SEED)
for N in range(2, 7):
for D in range(0, 5):
for _ in range(70 if N <= 5 else 30):
yield rand_instance(rng, N, D)
# chains through attributes outside R, and cycles
for N in range(3, 7):
chain = [([i], [i + 1]) for i in range(N - 1)]
for R in ([0, N - 1], [0, 1], [N - 1], list(range(N)), [0, N - 2, N - 1]):
yield normalize(N, chain, R)
yield normalize(N, [([i], [(i + 1) % N]) for i in range(N)], list(range(N)))
# ---------------------------------------------------------------- sections
def section1_symbolic():
S = "1-symbolic"
N, D, r, L, B = sp.symbols("N D r L B", nonnegative=True)
# per-part contributions derived from the construction (see proof.typ)
clauses_parts = {"init": N + r, "trig": N * (L + D), "close": N * (B + 2 * N), "gain": 3 * r, "final": 2}
lits_parts = {"init": N + 3 * r, "trig": N * (3 * L + D), "close": N * (3 * B + 4 * N), "gain": 7 * r, "final": 2 * r}
clauses = sum(clauses_parts.values())
lits = sum(lits_parts.values())
nvars = r + N * (N + 1) + N * D + r
check(S, sp.expand(clauses - (N + 4 * r + N * (L + B + D + 2 * N) + 2)) == 0, "clauses formula")
check(S, sp.expand(lits - (N + 12 * r + N * (3 * L + 3 * B + D + 4 * N))) == 0, "literals formula")
check(S, sp.expand(nvars - (N * (N + 1) + N * D + 2 * r)) == 0, "variables formula")
# upper bounds in registered parameters via L+B <= 2ND
ub_c = N + 4 * r + N * (2 * N * D + D + 2 * N) + 2
ub_l = N + 12 * r + N * (6 * N * D + D + 4 * N)
check(S, sp.expand(ub_c - clauses - N * (2 * N * D - L - B)) == 0, "clause slack identity")
check(S, sp.expand(ub_l - lits - 3 * N * (2 * N * D - L - B)) == 0, "literal slack identity")
# sample points: bound >= exact whenever L+B <= 2ND
for _ in range(200):
n_, d_, r_ = random.randint(1, 30), random.randint(0, 30), random.randint(1, 30)
l_ = random.randint(d_, n_ * d_)
b_ = random.randint(0, n_ * d_)
check(S, ub_c.subs({N: n_, D: d_, r: r_}) >= clauses.subs({N: n_, D: d_, r: r_, L: l_, B: b_}), "ub clauses")
check(S, ub_l.subs({N: n_, D: d_, r: r_}) >= lits.subs({N: n_, D: d_, r: r_, L: l_, B: b_}), "ub literals")
# per-part checks against the stated per-gate counts
check(S, sp.expand(clauses_parts["trig"] / N - (L + D)) == 0, "trigger clauses per round = L + D")
check(S, sp.expand(lits_parts["close"] / N - (3 * B + 4 * N)) == 0, "closure literals per round")
# the YES/NO example values
yes = {N: 4, D: 2, r: 3, L: 2, B: 2}
no = {N: 3, D: 3, r: 3, L: 3, B: 3}
check(S, (nvars.subs(yes), clauses.subs(yes), lits.subs(yes)) == (34, 74, 160), "YES example sizes")
check(S, (nvars.subs(no), clauses.subs(no), lits.subs(no)) == (27, 62, 138), "NO example sizes")
def full_instance_check(inst):
"""Sections 2, 3, 4, 5 for a single instance."""
N, fds, R = inst
D, r = len(fds), len(R)
nv, cl = reduce(inst)
srcs = src_solutions(inst)
models = all_models(nv, cl)
# section 2: feasibility equivalence, and strong form: #models == #source solutions
check("2-feasibility", (len(models) > 0) == (len(srcs) > 0), f"{inst}")
check("2-feasibility", len(models) == len(srcs), f"model count {inst}")
# forward direction: each source solution lifts to a model by direct simulation
for b in srcs:
sol = lift(inst, list(b))
check("2-feasibility", len(sol) == nv and sat_eval(cl, sol), f"lift {inst} {b}")
# backward: every model projects to a source solution
proj = set()
for m in models:
ex = extract(inst, nv, cl, m)
check("3-extraction", ex is not None, f"extract validated {inst}")
check("3-extraction", ex is not None and src_eval(inst, ex), f"extract is solution {inst}")
proj.add(tuple(m[:r]))
check("3-extraction", proj == set(srcs), f"projection onto exactly the solutions {inst}")
check("3-extraction", len(proj) == len(models), f"projection injective {inst}")
# extraction rejects non-witnesses and wrong lengths
if models:
bad = list(models[0])
# flip one auxiliary-or-selection bit; extraction must reject iff the CNF is violated
k = random.randrange(nv)
bad[k] = not bad[k]
check("3-extraction", (extract(inst, nv, cl, bad) is not None) == sat_eval(cl, bad), "reject unsatisfying")
check("3-extraction", extract(inst, nv, cl, models[0] + [True]) is None, "reject long")
check("3-extraction", extract(inst, nv, cl, models[0][:-1]) is None, "reject short")
# section 4: measured sizes
N_, D_, r_, L, B = sizes_params(inst)
check("4-sizes", nv == N * (N + 1) + N * D + 2 * r, "num_vars")
check("4-sizes", len(cl) == N + 4 * r + N * (L + B + D + 2 * N) + 2, f"num_clauses {inst}")
check("4-sizes", sum(len(c) for c in cl) == N + 12 * r + N * (3 * L + 3 * B + D + 4 * N), f"num_literals {inst}")
check("4-sizes", len(cl) <= N + 4 * r + N * (2 * N * D + D + 2 * N) + 2, "clause bound")
check("4-sizes", sum(len(c) for c in cl) <= N + 12 * r + N * (6 * N * D + D + 4 * N), "literal bound")
check("4-sizes", L + B <= 2 * N * D, "L+B <= 2ND")
# section 5: well-formedness
check("5-structure", all(c and all(1 <= abs(l) <= nv for l in c) for c in cl), "literal range, nonempty clauses")
check("5-structure", all(len({abs(l) for l in c}) == len(c) for c in cl), f"no repeated variable in a clause {inst}")
used = {abs(l) for c in cl for l in c}
check("5-structure", used == set(range(1, nv + 1)), "every variable occurs")
# every aux variable is determined by x: fixing x yields at most one model
cnt = defaultdict(int)
for m in models:
cnt[tuple(m[:r])] += 1
check("5-structure", all(v == 1 for v in cnt.values()), "auxiliaries functionally determined by selection bits")
# the final layer equals the least closure on every selection, via forced propagation
for bits in itertools.product([False, True], repeat=r):
X = {R[i] for i, b in enumerate(bits) if b}
sol = lift(inst, list(bits))
x, c, g, w, _ = var_layout(inst)
cN = {a for a in range(N) if sol[c[N, a] - 1]}
check("5-structure", cN == closure(X, fds), f"layer N = closure {inst} {bits}")
check("5-structure", sat_eval(cl, sol) == src_eval(inst, list(bits)), f"lift satisfies iff solution {inst} {bits}")
def lift(inst, bits):
"""Forward-direction assignment: selection bits, successive closure sets, triggers, gains."""
N, fds, R = inst
D = len(fds)
x, c, g, w, nv = var_layout(inst)
sol = [False] * nv
X = {R[i] for i, b in enumerate(bits) if b}
for a in R:
sol[x[a] - 1] = a in X
layer = set(X)
for t in range(N + 1):
for a in range(N):
sol[c[t, a] - 1] = a in layer
if t < N:
nxt = set(layer)
for d, (l, rr) in enumerate(fds):
on = all(a in layer for a in l)
sol[g[t, d] - 1] = on
if on:
nxt |= set(rr)
layer = nxt
for a in R:
sol[w[a] - 1] = (a not in X) and (a in layer)
return sol
def section_examples():
# YES example
inst = normalize(4, [([0], [1]), ([1], [2])], [0, 1, 3])
nv, cl = reduce(inst)
S = "6-yes-example"
check(S, (nv, len(cl), sum(len(c) for c in cl)) == (34, 74, 160), "YES sizes")
sol = lift(inst, [True, False, False])
x, c, g, w, _ = var_layout(inst)
layers = ["".join("1" if sol[c[t, a] - 1] else "0" for a in range(4)) for t in range(5)]
check(S, layers == ["1000", "1100", "1110", "1110", "1110"], f"layers {layers}")
trig = ["".join("1" if sol[g[t, d] - 1] else "0" for d in range(2)) for t in range(4)]
check(S, trig == ["10", "11", "11", "11"], f"triggers {trig}")
gains = "".join("1" if sol[w[a] - 1] else "0" for a in inst[2])
check(S, gains == "010", f"gains {gains}")
check(S, len(sol) == 34 and sat_eval(cl, sol), "complete vector satisfies")
check(S, extract(inst, nv, cl, sol) == [True, False, False], "extraction")
check(S, src_eval(inst, [True, False, False]), "source witness")
check(S, "".join("1" if v else "0" for v in sol) ==
"100" + "".join(layers) + "".join(trig) + "010", "concatenated vector")
ms = all_models(nv, cl)
check(S, sorted(src_solutions(inst)) == sorted(tuple(m[:3]) for m in ms), "model set = source solutions")
# X = {0} is one of the solutions; list all
check(S, (True, False, False) in src_solutions(inst), "X={0} solution")
def section_no_example():
S = "7-no-example"
inst = normalize(3, [([0], [1]), ([1], [2]), ([2], [0])], [0, 1, 2])
nv, cl = reduce(inst)
check(S, (nv, len(cl), sum(len(c) for c in cl)) == (27, 62, 138), "NO sizes")
check(S, src_solutions(inst) == [], "source infeasible")
check(S, all_models(nv, cl) == [], "target infeasible (complete DPLL)")
# per selection X, the forced assignment violates exactly a final clause
x, c, g, w, _ = var_layout(inst)
for bits in itertools.product([False, True], repeat=3):
sol = lift(inst, list(bits))
viol = [i for i, k in enumerate(cl) if not any((l > 0) == sol[abs(l) - 1] for l in k)]
check(S, set(viol) <= {len(cl) - 2, len(cl) - 1} and viol, f"only final clauses violated {bits} {viol}")
if not any(bits):
check(S, viol == [len(cl) - 2], "X empty: no gain")
else:
want = [len(cl) - 2, len(cl) - 1] if all(bits) else [len(cl) - 1]
check(S, viol == want, "X nonempty: closure complete (and no gain when X=R)")
# brute force over all 2^27 is infeasible; DPLL above is complete. also brute-force a reduced sanity
check(S, extract(inst, nv, cl, [False] * nv) is None, "all-zero rejected")
def section_special_cases():
S = "5-structure"
cases = {
"empty dependency list": normalize(3, [], [0, 1, 2]),
"empty right sides": normalize(3, [([0], []), ([1], [])], [0, 1, 2]),
"derivation through attribute outside R": normalize(4, [([0], [2]), ([2], [1])], [0, 1, 3]),
"R is a single attribute": normalize(3, [([0], [1])], [0]),
"duplicate dependencies": normalize(3, [([0], [1]), ([0], [1]), ([0, 0], [1, 1])], [0, 1, 2]),
"N=1": normalize(1, [([0], [0])], [0]),
"lhs contains rhs": normalize(4, [([0, 1], [1, 2])], [0, 1, 2, 3]),
}
expect_feasible = {
"empty dependency list": False, "empty right sides": False,
"derivation through attribute outside R": True, "R is a single attribute": False,
"duplicate dependencies": True, "N=1": False, "lhs contains rhs": True,
}
for name, inst in cases.items():
nv, cl = reduce(inst)
ms = all_models(nv, cl)
check(S, (len(ms) > 0) == expect_feasible[name], f"special case {name}")
check(S, len(ms) == len(src_solutions(inst)), f"special case count {name}")
N, fds, R = inst
D, r = len(fds), len(R)
_, _, _, L, B = sizes_params(inst)
check(S, len(cl) == N + 4 * r + N * (L + B + D + 2 * N) + 2, f"special size {name}")
# X = empty: closure is empty because every left side is nonempty
inst = normalize(3, [([0], [1])], [0, 1, 2])
sol = lift(inst, [False] * 3)
x, c, g, w, _ = var_layout(inst)
check(S, not any(sol[c[N_, a] - 1] for N_ in [3] for a in range(3)), "X empty gives empty closure")
# outside-R chain: dropping outside-R attributes from the layers would lose the derivation
inst = cases["derivation through attribute outside R"]
nv, cl = reduce(inst)
check(S, len(all_models(nv, cl)) == 1, "exactly the X={0} witness")
def section_mutants():
S = "2-feasibility"
pool = list(instances_exhaustive())
pool += list(sampled_instances())
for mut in ["one_way_gate", "one_way_or", "no_persist", "drop_nonR", "few_rounds",
"w_no_closure", "w_no_notx", "no_missing_clause"]:
killed = False
for inst in pool:
nv, cl = reduce(inst, mutant=mut)
r = len(inst[2])
srcs = set(src_solutions(inst))
# cheap test: lifted true assignment of the correct construction vs the mutant CNF,
# plus the mutant's own model set projected on x
ms = all_models(nv, cl)
if {tuple(m[:r]) for m in ms} != srcs:
killed = True
break
check(S, killed, f"mutant {mut} must be detected by the exhaustive comparison")
# ---------------------------------------------------------------- hypothesis
def run_hypothesis():
S = "2-feasibility"
@st.composite
def inst_strategy(draw):
N = draw(st.integers(1, 6))
D = draw(st.integers(0, 5))
fds = []
for _ in range(D):
L = draw(st.lists(st.integers(0, N - 1), min_size=1, max_size=N))
Rr = draw(st.lists(st.integers(0, N - 1), max_size=N))
fds.append((L, Rr))
R = draw(st.lists(st.integers(0, N - 1), min_size=1, max_size=N))
return normalize(N, fds, R)
@st.composite
def chain_strategy(draw):
# long derivations, many through attributes outside R
N = draw(st.integers(3, 6))
perm = draw(st.permutations(list(range(N))))
k = draw(st.integers(1, N - 1))
fds = [([perm[i]], [perm[i + 1]]) for i in range(k)]
if draw(st.booleans()):
fds.append((draw(st.lists(st.integers(0, N - 1), min_size=1, max_size=2)),
draw(st.lists(st.integers(0, N - 1), max_size=2))))
R = draw(st.lists(st.integers(0, N - 1), min_size=1, max_size=N))
return normalize(N, fds, R)
for name, strat in (("general", inst_strategy()), ("chains", chain_strategy())):
@settings(max_examples=250, deadline=None, database=None, derandomize=False,
suppress_health_check=list(HealthCheck))
@given(strat)
def prop(inst):
nv, cl = reduce(inst)
ms = all_models(nv, cl)
srcs = src_solutions(inst)
r = len(inst[2])
check(S, sorted(tuple(m[:r]) for m in ms) == sorted(srcs), f"hypothesis[{name}] {inst}")
for m in ms:
ex = extract(inst, nv, cl, m)
check("3-extraction", ex is not None and src_eval(inst, ex), f"hypothesis[{name}] extract")
N, fds, R = inst
_, D, _, L, B = sizes_params(inst)
check("4-sizes", len(cl) == N + 4 * r + N * (L + B + D + 2 * N) + 2, f"hypothesis[{name}] size")
prop()
def main():
section1_symbolic()
n = 0
for inst in instances_exhaustive():
full_instance_check(inst)
n += 1
m = 0
for inst in sampled_instances():
full_instance_check(inst)
m += 1
section_examples()
section_no_example()
section_special_cases()
section_mutants()
run_hypothesis()
print(f"seed {SEED}; exhaustive instances {n}; sampled instances {m}")
order = ["1-symbolic", "2-feasibility", "3-extraction", "4-sizes", "5-structure", "6-yes-example", "7-no-example"]
for s in order:
print(f" section {s}: {CHECKS[s]} checks, {FAILS[s]} failures")
if CHECKS[s] == 0:
FAILS[s] += 1
print(" EMPTY SECTION")
for msg in MSGS:
print(msg)
tot = sum(CHECKS.values())
fails = sum(FAILS.values())
print(f"TOTAL: {tot} checks, {fails} failures")
return 1 if fails else 0
if __name__ == "__main__":
sys.exit(main())Independent re-implementation (reduction and closure checker)"""Independent implementation of BoyceCoddNormalFormViolation -> Satisfiability,
written from the Typst proof alone.
Public API
normalize(n, fds, R) -> (n, fds, R) as the source model's constructor does
reduce(n, fds, R) -> Target(num_vars, clauses, tags)
extract(n, fds, R, target, assignment) -> list[bool] (validates the witness once)
source_ok(n, fds, R, config) -> bool (the source model's predicate)
closure(X, fds) -> frozenset (linear-time counter algorithm)
layers(n, fds, X, rounds) -> list of frozensets S_0..S_rounds (naive iteration)
var_x/var_c/var_g/var_w -> variable numbers from the proof's numbering
count_models(num_vars, clauses, fixed) -> list of models (DPLL with unit propagation)
brute_models(num_vars, clauses) -> set of models as ints (exhaustive, no propagation)
"""
from __future__ import annotations
from dataclasses import dataclass, field
from itertools import product
class InvalidInstance(ValueError):
pass
def normalize(n, fds, R):
"""Mirror the source model's validation and normalization."""
if len(R) == 0:
raise InvalidInstance("target_subset must be non-empty")
out = []
for i, (lhs, rhs) in enumerate(fds):
if len(lhs) == 0:
raise InvalidInstance(f"FD {i} has an empty LHS")
lhs = sorted(set(lhs))
rhs = sorted(set(rhs))
for a in lhs + rhs:
if not (0 <= a < n):
raise InvalidInstance(f"FD {i} attribute {a} out of range")
out.append((tuple(lhs), tuple(rhs)))
R = sorted(set(R))
for a in R:
if not (0 <= a < n):
raise InvalidInstance(f"target attribute {a} out of range")
return n, out, tuple(R)
# ---------------------------------------------------------------- numbering
def var_x(i, n, D, r):
return i + 1
def var_c(t, a, n, D, r):
return r + t * n + a + 1
def var_g(t, d, n, D, r):
return r + n * (n + 1) + t * D + d + 1
def var_w(i, n, D, r):
return r + n * (n + 1) + n * D + i + 1
@dataclass
class Target:
num_vars: int
clauses: list # list of tuples of signed ints
tags: list = field(default_factory=list) # section tag per clause
@property
def num_clauses(self):
return len(self.clauses)
@property
def num_literals(self):
return sum(len(c) for c in self.clauses)
def reduce(n, fds, R, rounds=None):
"""Build Phi exactly as the proof's numbered construction describes."""
n, fds, R = normalize(n, fds, R)
D, r = len(fds), len(R)
T = n if rounds is None else rounds
X = lambda i: var_x(i, n, D, r)
C = lambda t, a: var_c(t, a, n, D, r)
# equal to var_g / var_w when T == n (the proof's construction)
G = lambda t, d: r + n * (T + 1) + t * D + d + 1
W = lambda i: r + n * (T + 1) + T * D + i + 1
pos_in_R = {a: i for i, a in enumerate(R)}
cls, tags = [], []
def add(c, tag):
cls.append(tuple(c))
tags.append(tag)
# item 2: initial layer
for a in range(n):
if a in pos_in_R:
i = pos_in_R[a]
add((-C(0, a), X(i)), "init")
add((C(0, a), -X(i)), "init")
else:
add((-C(0, a),), "init")
# item 3: rounds
for t in range(T):
for d, (lhs, rhs) in enumerate(fds):
for a in lhs:
add((-G(t, d), C(t, a)), f"trig:{t}:{d}")
add((G(t, d),) + tuple(-C(t, a) for a in lhs), f"trig:{t}:{d}")
for a in range(n):
H = [C(t, a)] + [G(t, d) for d, (lhs, rhs) in enumerate(fds) if a in rhs]
for h in H:
add((-h, C(t + 1, a)), f"trans:{t}:{a}")
add((-C(t + 1, a),) + tuple(H), f"trans:{t}:{a}")
# item 4: gain gates (use the final layer index T)
for i, a in enumerate(R):
add((-W(i), -X(i)), "gain")
add((-W(i), C(T, a)), "gain")
add((W(i), X(i), -C(T, a)), "gain")
# item 5: final clauses
add(tuple(W(i) for i in range(r)), "final")
add(tuple(-C(T, a) for a in R), "final")
num_vars = r + n * (T + 1) + T * D + r
return Target(num_vars, cls, tags)
def satisfies(clauses, assignment):
"""assignment: sequence of bools, index v-1 for variable v."""
for c in clauses:
if not any((assignment[abs(l) - 1] if l > 0 else not assignment[abs(l) - 1]) for l in c):
return False
return True
def extract(n, fds, R, target: Target, assignment):
n, fds, R = normalize(n, fds, R)
if len(assignment) != target.num_vars:
raise ValueError("wrong witness length")
if not satisfies(target.clauses, assignment):
raise ValueError("witness does not satisfy the CNF")
return [bool(b) for b in assignment[: len(R)]]
# ---------------------------------------------------------------- source side
def closure(X, fds):
"""Linear-time closure (counter per dependency); deliberately not the
round-based iteration used by the construction."""
fds = list(fds)
missing = [len(set(lhs)) for lhs, _ in fds]
watch = {}
for d, (lhs, _) in enumerate(fds):
for a in set(lhs):
watch.setdefault(a, []).append(d)
result = set(X)
queue = list(result)
while queue:
a = queue.pop()
for d in watch.get(a, ()):
missing[d] -= 1
if missing[d] == 0:
for b in fds[d][1]:
if b not in result:
result.add(b)
queue.append(b)
return frozenset(result)
def layers(n, fds, X, rounds):
S = [frozenset(X)]
for _ in range(rounds):
cur = S[-1]
nxt = set(cur)
for lhs, rhs in fds:
if set(lhs) <= cur:
nxt |= set(rhs)
S.append(frozenset(nxt))
return S
def source_ok(n, fds, R, config):
"""The model's predicate: exists y, z in R \\ X, y in X+, z not in X+."""
n, fds, R = normalize(n, fds, R)
if len(config) != len(R):
raise ValueError("wrong config length")
X = {a for a, b in zip(R, config) if b}
cl = closure(X, fds)
rest = [a for a in R if a not in X]
return any(a in cl for a in rest) and any(a not in cl for a in rest)
def source_solutions(n, fds, R):
n, fds, R = normalize(n, fds, R)
return [tuple(cfg) for cfg in product([False, True], repeat=len(R)) if source_ok(n, fds, R, cfg)]
# ---------------------------------------------------------------- SAT side
def count_models(num_vars, clauses, fixed=None, cap=None):
"""Enumerate all models with DPLL + unit propagation.
Returns a list of models (tuples of bools). `fixed` maps var -> bool."""
occ = [[] for _ in range(num_vars + 1)]
for ci, c in enumerate(clauses):
for l in c:
occ[abs(l)].append(ci)
models = []
def propagate(assign, trail_start_vars):
# assign: list of None/bool, index = var
queue = list(trail_start_vars)
while queue:
v = queue.pop()
for ci in occ[v]:
c = clauses[ci]
unassigned = None
n_un = 0
sat = False
for l in c:
val = assign[abs(l)]
if val is None:
n_un += 1
unassigned = l
elif (val if l > 0 else not val):
sat = True
break
if sat:
continue
if n_un == 0:
return False
if n_un == 1:
u = abs(unassigned)
assign[u] = unassigned > 0
queue.append(u)
return True
def all_clauses_ok(assign):
for c in clauses:
if not any((assign[abs(l)] if l > 0 else not assign[abs(l)]) for l in c):
return False
return True
assign = [None] * (num_vars + 1)
init = []
if fixed:
for v, b in fixed.items():
assign[v] = b
init.append(v)
# unit clauses
for c in clauses:
if len(c) == 1:
v = abs(c[0])
b = c[0] > 0
if assign[v] is None:
assign[v] = b
init.append(v)
elif assign[v] != b:
return []
if not propagate(assign, init):
return []
# empty clause
if any(len(c) == 0 for c in clauses):
return []
def rec(assign):
if cap is not None and len(models) >= cap:
return
try:
v = assign.index(None, 1)
except ValueError:
if all_clauses_ok(assign):
models.append(tuple(assign[1:]))
return
for b in (False, True):
a2 = list(assign)
a2[v] = b
if propagate(a2, [v]):
rec(a2)
rec(assign)
return models
def brute_models(num_vars, clauses):
"""Exhaustive over 2^num_vars, bit v-1 of the int = variable v."""
masks = []
for c in clauses:
pos = neg = 0
for l in c:
if l > 0:
pos |= 1 << (l - 1)
else:
neg |= 1 << (-l - 1)
masks.append((pos, neg))
full = (1 << num_vars) - 1
out = set()
for a in range(1 << num_vars):
na = full ^ a
for pos, neg in masks:
if not (a & pos) and not (na & neg):
break
else:
out.add(a)
return out
def model_to_int(m):
return sum(1 << i for i, b in enumerate(m) if b) |
Collaborator
Author
Agentic Review ReportSubject: rule Verdict: approve. No open findings. Structural and semantic
Quality14 rule tests, each under 2.5 s, covering:
Weakening the trigger gate while keeping every size unchanged makes 6 of the tests fail. Feature test
FindingsNone open. All six findings from earlier review rounds are resolved:
|
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1239 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 152088 +530
========================================
+ Hits 147308 147830 +522
- Misses 4250 4258 +8 ☔ 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 #1202
Summary
Adds the reduction
BoyceCoddNormalFormViolation → Satisfiability.N(N+1) + N·D + 2rvariables (exact), with clause and literal counts given as upper bounds in the attribute, dependency and target-attribute counts.|R|bits.The closure-encoding sketch in #445 is the starting point for this construction; thanks to its author.
Test plan
make checkmake paper