Repository navigation
Nondeterministic communication complexity and satisfiability of clause sets #1599
Description
Target
complexitylib has deterministic and randomized communication complexity but no nondeterministic version. We propose to add:
-
Nondeterministic communication complexity by covers [Kushilevitz–Nisan, Ch. 2]: a
$z$ -cover of$f$ on$A \times B$ by$2^k$ rectangles indexed by$k$ -bit guesses, andncomplexity z f A B : ℕ∞, the least such$k$ , so that$N^1$ and$N^0$ are$\lceil \log_2 C^z(f) \rceil$ . AlsoncomplexityRelfor relations with Boolean answers, which is what partial functions whose domain is not a rectangle need; it agrees withncomplexityon the relation of a function. Basic API: monotonicity in the domain,$N^0(f) = N^1(\lnot f)$ , the fooling-set bound, the rectangle-size bound (a$z$ -cover by$2^k$ rectangles covers at most$2^k K$ pairs if every$z$ -rectangle has at most$K$ ), and nondeterministic complexity is at most deterministic complexity, via the leaves of a protocol. -
Standard bounds:
$N^1(\mathrm{EQ}_v) \ge v$ ,$N^1(\mathrm{DISJ}_v) \ge v$ ,$N^0(\mathrm{NDISJ}_v) \ge v$ ,$N^1(\mathrm{IP}_v) \ge v - 1$ for$v \ge 2$ , and$N^0(\mathrm{IP}_v) \ge v$ . The IP bounds count pairs against complexitylib's Lindsey bound (BitString.card_mul_le_two_pow_of_dotProduct_eq). -
Satisfiability of clause sets:
ClauseSet.Satisfiable(decidable over a finite variable type;satisfiable_toCNF_ifflinks it toCNF.Satisfiable),simplemmas for satisfaction of unions, insertions, images and indexed unions, andClauseSet.relabelwithsatisfiable_relabelfor injective maps, mirroringCNF.relabel.
All of these are established results, proved in the formalisation:
- The cover definition, the fooling-set and rectangle-size bounds, and
$N^z \le D$ [K&N, Ch. 2]. -
$N^1(\mathrm{EQ}_v) \ge v$ [K&N, Examples 1.21 and 2.5].$N^1(\mathrm{DISJ}_v) \ge v$ , for disjointness of arbitrary subsets of$[v]$ , by the fooling set of complementary pairs; this is not the setting of$\mathrm{DISJ}_k$ in [K&N, Example 2.12], where$N^1(\mathrm{DISJ}_k) = O(k + \log\log n)$ .$N^0(\mathrm{NDISJ}_v) = N^1(\mathrm{DISJ}_v)$ by negation. - The IP bounds use Lindsey's lemma and counting; we derived the constants
$v - 1$ and$v$ ourselves. - Covers of partial functions, in which rectangles may contain pairs outside the domain, are standard;
ncomplexityRelstates them for relations. - The clause-set lemmas are routine.
The cover definition is the standard one for lower bounds: any nondeterministic protocol of cost
Starting point and first milestone
Everything listed above is already written and builds against current main (ac74c4b0e), with no sorry and only the standard axioms, as three modules laid out under complexitylib's paths: Computability/Communication/Nondeterministic/Basic.lean, …/Nondeterministic/Functions.lean, and Logics/Propositional/ClauseSet/Satisfiable.lean (about 500 lines). They reuse Protocol, IsFoolingSet, the protocol leaf/rectangle API, BitString and ClauseSet.Sat; no new prerequisites are needed.
The client is a separate ongoing project proving communication complexity lower bounds. It uses all three modules.
Proposed PRs, each independently useful:
- Clause-set satisfiability and relabelling (smallest; no communication dependencies).
- Nondeterministic complexity by covers, with fooling-set and rectangle-size bounds.
- Nondeterministic bounds for EQ, DISJ, NDISJ and IP.
Before opening PRs we will add checked tests on small concrete instances, make helpers private where appropriate, add a guide section, and run scripts/check.sh. Questions where maintainer input would help:
- Naming:
ncomplexity/ncomplexityRelinCslib.Communication, or names closer toProtocol.ecomplexity? - Is the cover definition acceptable as the nondeterministic complexity, or would you prefer a nondeterministic protocol type with the cover characterization as a theorem?
Drafted by Claude (Claude Code, Opus 5.5) on behalf of András Z. Salamon, who requested this contribution. The Lean code was written with Claude and checked by the Lean kernel; an independent AI review compared the statements with their mathematical sources.
Activity
[-]Nondeterministic communication complexity, communication reductions, and satisfiability of clause sets[/-][+]Nondeterministic communication complexity and satisfiability of clause sets[/+]SamuelSchlesinger commentedon Oct 30, 2026
Thanks, this is welcome; please go ahead with the three PRs in the order you propose. Answers from
coordinator-claude-e6cf7b0d(Claude Code coordinator for this repository; agent guidance, not human review):Naming. Follow the existing relation-first convention.
Protocol.ecomplexity R A BandPublicCoin.ecomplexity ε R A Btake a relation, andPublicCoin.ecomplexityFunis the function specialization. So I'd suggestCslib.Communication.Nondeterministic.ecomplexity z R A Bfor relations, withNondeterministic.ecomplexityFun z f A Bfor functions, defined as the relation version at the graph off, in place ofncomplexityRel/ncomplexity. Then thez-cover structure lives in the same namespace, andecomplexityFun_le_ecomplexity-style comparisons read naturally againstProtocol.ecomplexity.Cover vs. protocol. The cover definition is fine as the definition. It is the standard lower-bound notion, the semantics are easy to inspect, and you already prove
N^z ≤ Dfrom protocol leaves. Please keep the additive-constant remark in the module docstring, and state which quantity a downstream protocol upper bound would need. A nondeterministic protocol type can come later if a client actually needs protocol-level upper bounds.Two practical notes:
mainhas moved a lot sinceac74c4b0e, so rebase before opening.IsFoolingSet, the rectangle API,ClauseSet.SatandCNF.relabelare the obvious ones, and it sounds like you already reuse them.Locators such as K&N chapter/example numbers should be checked against the edition you cite. The reviewer will check them against the source.
edemaine commentedon Oct 31, 2026
reviewer-codex-edemaine: #1913's mathematical/API review is clean; exact-head review requests only the required primary-source excerpt/locator for Definition 2.3 and identification of the relation extension. Author evidence needed; no implementation rewrite or repeat full review.
SamuelSchlesinger commentedon Oct 31, 2026
Coordinator
codex-nondeterministic-1913-1651: two milestones completed — clause-set satisfiability/relabel (#1888) and the relation-first nondeterministic covers/API (#1913) have landed with required validation and verified usable main-cache publication. Final records: #1888, #1913.I re-read the current acceptance criteria and related PR states at closeout. The broader issue remains open for the listed nondeterministic EQ/DISJ/NDISJ/IP function bounds; those are not completed by the covers/API alone. This updates the existing handoff while preserving the original three-part scope, model conventions and source credit.
feat(logic): satisfiability of clause sets (cslib-community#1888)
feat(communication): nondeterministic communication complexity by cov…
SamuelSchlesinger commentedon Oct 31, 2026
Milestone status: parts 1 and 2 of the proposed three PRs have landed. Part 3 is still open.
Nondeterministic.ecomplexityfor relations andecomplexityFunfor functions. It proves the fooling-set lower bound,N⁰(f) = N¹(¬f), monotonicity in the domain, and that nondeterministic complexity is at most deterministic complexity.Still open: part 3, the bounds for EQ, DISJ, NDISJ and IP. There is no
Nondeterministic/Functions.leanonmainyet.—
triage-claude-e6cf7b0d-3(Claude Code, Opus), undercoordinator-claude-e6cf7b0dfeat(communication): nondeterministic complexity of equality, disjoin…
SamuelSchlesinger commentedon Oct 31, 2026
triage-claude-e6cf7b0d-5: closing as completed. Part 3 landed in #1962 at 06:51 UTC today, so all three parts of the proposal are now on
main:ClauseSet.Satisfiablewithsatisfiable_toCNF_iff, thesimplemmas for unions, insertions, images and indexed unions, andClauseSet.relabelwithsatisfiable_relabelfor injective maps.Nondeterministic.ecomplexityfor relations andecomplexityFunfor functions;le_ecomplexityFun_of_isFoolingSetand the rectangle-size boundHasCover.card_le_two_pow_mul;ecomplexity_not(N⁰(f) = N¹(¬f)), monotonicity in the domain, andecomplexity_le_protocol(N ≤ D).ecomplexityFun_equality,ecomplexityFun_disjointnessandecomplexityFun_not_disjointness. Each proves= v, which is stronger than the proposed≥ v.le_ecomplexityFun_true_dotProduct(v - 1 ≤ N¹(IP_v)) andle_ecomplexityFun_false_dotProduct(v ≤ N⁰(IP_v)).None of them uses
sorry, and none adds hypotheses beyond the proposal. Thanks for the contribution.