Verifying Cake-Cutting, Faster
Noah Bertram, Tean Lai, Justin Hsu

TL;DR
This paper enhances the Slice language and verification methods for envy-free cake-cutting protocols, enabling efficient verification of more complex protocols, including the first nontrivial four-agent example.
Contribution
It introduces a linear type system and reduces verification to linear real arithmetic, improving scalability and enabling verification of complex protocols.
Findings
Successfully verified complex cake-cutting protocols
Reduced verification to linear real arithmetic formulas
Verified the first nontrivial four-agent protocol
Abstract
Envy-free cake-cutting protocols procedurally divide an infinitely divisible good among a set of agents so that no agent prefers another's allocation to their own. These protocols are highly complex and difficult to prove correct. Recently, Bertram, Levinson, and Hsu introduced a language called Slice for describing and verifying cake-cutting protocols. Slice programs can be translated to formulas encoding envy-freeness, which are solved by SMT. While Slice works well on smaller protocols, it has difficulty scaling to more complex cake-cutting protocols. We improve Slice in two ways. First, we show any protocol execution in Slice can be replicated using piecewise uniform valuations. We then reduce Slice's constraint formulas to formulas within the theory of linear real arithmetic, showing that verifying envy-freeness is efficiently decidable. Second, we design and implement a linear…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsOptimization and Packing Problems
