Implementation of the wave function collapse algorithm in SAT with custom propagator

Thumbnail Image

Files

master_Ngo_Trung_2026.pdf (3.62 MB)

URL

Journal Title

Journal ISSN

Volume Title

School of Science | Master's thesis
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.

Authors

Date

2025-12-31

Department

Major/Subject

Computer Science

Mcode

Degree programme

Master's Programme in Computer, Communication and Information Sciences
Master's Programme in Computer, Communication and Information Sciences
Master's Programme in Computer, Communication and Information Sciences

Language

en

Pages

40

Series

Abstract

Procedural content generation represents an interesting challenge in modern game development, requiring the synthesis of coherent, playable game environments while satisfying diverse structural constraints. This thesis presents a novel implementation of the Wave Function Collapse (WFC) algorithm formulated as a Boolean Satisfiability (SAT) problem with custom propagators, enabling the declarative specification of complex global constraints in procedurally generated content. The implementation extends the CaDiCaL SAT solver through its external propagator interface, integrating random sampling into the deterministic solving process to achieve stochastic generation while maintaining the constraint satisfaction guarantees. The work introduces efficient encoding schemes for finite domain variables using unary representation with lazy clause generation, achieving up to six times less memory consumption, enabling larger artifacts to be generated. Furthermore, the thesis develops and evaluates multiple encodings for global constraints for controlled game level generation with a focus on path-based constraints. Experimental results demonstrate that the SAT-based approach achieves performance comparable to established procedural implementations such as DeBroglie while providing superior expressiveness through declarative constraint specification. The declarative nature of the SAT formulation allows game designers to specify high-level design requirements without implementing domain-specific propagation algorithms, offering a more accessible and maintainable approach to constraint-based procedural content generation.

Description

Supervisor

Rintanen, Jussi

Thesis advisor

Lehtonen, Tuomo

Keywords

procedural content generation, boolean satisfiability, wave function collapse, constraint satisfaction, game development, declarative programming

Other note

Citation

Permanent link to this item

https://urn.fi/URN:NBN:fi:aalto-202601221835

Collections

[dipl] Perustieteiden korkeakoulu / SCI