Cutting the cake into crumbs: verifying envy-free cake cutting protocols using bounded integer arithmetic

Lester, M. M. ORCID: https://orcid.org/0000-0002-2323-1771 (2024) Cutting the cake into crumbs: verifying envy-free cake cutting protocols using bounded integer arithmetic. In: Gebser, M. and Sergey, I. (eds.) Practical aspects of declarative languages: 26th international symposium, PADL 2024, London, UK, January 15–16, 2024, Proceedings. Lecture Notes in Computer Science (14512). Springer, Cham, pp. 100-115. ISBN 9783031520372 doi: 10.1007/978-3-031-52038-9_7

Abstract/Summary

Fair division protocols specify how to split a continuous resource (conventionally represented by a cake) between multiple agents with different preferences. Envy-free protocols ensure no agent prefers any other agent's allocation to his own. These protocols are complex and manual proofs of their correctness may contain errors. Recently, Bertram and others developed the DSL Slice for describing these protocols and showed how verification of envy-freeness can be reduced to SMT instances in the theory of quantified non-linear real arithmetic. This theory is decidable, but the decision procedure is slow, both in theory and in practice. We prove that, under reasonable assumptions about the primitive operations used in the protocol, counterexamples to envy-freeness can always be found with bounded integer arithmetic. Building on this result, we construct an embedded DSL for describing cake-cutting protocols in declarative-style C. Using the bounded model-checker CBMC, we reduce verifying envy-freeness of a protocol to checking unsatisfiability of pure SAT instances. This leads to a substantial reduction in verification time when the protocol is unfair.

Item Type	Book or Report Section
URI	https://reading-clone.eprints-hosting.org/id/eprint/115785
Identification Number/DOI	10.1007/978-3-031-52038-9_7
Refereed	Yes
Divisions	Science > School of Mathematical, Physical and Computational Sciences > Department of Computer Science
Uncontrolled Keywords	fair division constraint programming declarative C
Publisher	Springer
Download/View statistics	View download statistics for this item