Module lll 

Satisfiability from sparsity — the Lovász Local Lemma certificate and its constructive Moser–Tardos witness. The lower bookend to the first-moment bound.

The first-moment bound (crate::families::ksat_threshold_first_moment_upper) says: above a clause density the expected number of solutions vanishes, so the formula is UNSAT with high probability. This module is the opposite side: a formula that is locally sparse — every clause shares variables with few others — is satisfiable, and the witness can be constructed.

Symmetric LLL: a uniform random assignment violates a width-w clause with probability 2⁻ʷ. If each clause shares a variable with at most d others and e · p · (d+1) ≤ 1 (where p = 2^{−w_min} is the worst-case violation probability), then some assignment satisfies all clauses. This is:

• sound — the LLL theorem (and we fuzz it against brute force: a certificate never lies);
• re-checkable — recompute w_min and d;
• constructive — Moser–Tardos resampling reaches a model in expected O(m) steps under the condition, so the certificate is also a witness recipe.

Structs

LllSatCert

A re-checkable SAT certificate from the Lovász Local Lemma: the minimum clause width w_min and the maximum dependency degree d that together satisfy e · 2^{−w_min} · (d+1) ≤ 1.

Functions

lll_certifies_sat

Certify satisfiability from sparsity via the symmetric LLL. Returns the witnessing degrees when e · 2^{−w_min} · (d+1) ≤ 1; otherwise None (the condition is sufficient, not necessary — None means “this certificate does not apply”, never “UNSAT”). An empty clause set is vacuously SAT; a set containing an empty clause can never be certified (it is UNSAT).

lll_dependency_degree

The LLL dependency degree: the maximum, over all clauses, of the number of other clauses that share at least one variable with it. Clauses over disjoint variable sets are independent events and do not count toward the degree.

moser_tardos_witness

Constructively find a satisfying assignment by Moser–Tardos resampling: start from a random assignment and, while some clause is violated, resample the variables of one violated clause. Under the LLL condition this terminates in expected O(m) resamples; the max_resamples cap is a safety net (only reachable when the condition does not hold). Returns a model, or None if the cap is hit.