This video demonstrates how to model and solve domino tiling problems on a chessboard using Prolog, focusing on the Constraint Logic Programming over Boolean variables (CLP(B)) library. It introduces two main approaches: a high-level geometric constraint method (geost) and a detailed boolean modeling (exact cover problem) approach. The explanation delves into the benefits of CLP(B), particularly its internal use of Binary Decision Diagrams (BDDs) for canonical representation, complete constraint propagation, and efficient operations like solution counting and uniform random sampling. The presenter covers implementation specifics, addresses performance challenges and optimizations, and discusses the philosophical balance between relying on computational power versus applying human creative insight for complex combinatorial tasks, illustrated with examples like fault-free tilings and the mutilated chessboard problem.
Prolog and Chessboard Tilings: A Deep Dive into Boolean Constraint Solving
0:00 Introduction to Domino Tilings with Prolog: The video introduces the challenge of covering a chessboard with dominoes and explores how Prolog can be used to describe and solve such problems.
0:23 Advanced Tiling Problems: The discussion expands to more complex scenarios, including identifying "faults" (straight lines through the board not crossing any domino), completing tilings with pre-placed tiles, and generalizing to other shapes like trominoes.
1:43 Geometric Constraints with SICStus Prolog (geost): Prolog offers powerful geometric constraints, notably the geost predicate in SICStus Prolog, which can conveniently express non-overlapping, multi-dimensional objects with specified shapes, suitable for tiling problems.
3:21 Boolean Modeling as Exact Cover Problem: An alternative, often simpler, approach is presented: a boolean model where each possible domino placement is represented by a boolean variable. The problem then becomes an "exact cover problem," ensuring each square is covered by precisely one chosen placement.
5:51 Exact Cover Formulation with CLP(B): The exact cover problem is precisely formulated in Prolog using the library(clpb) (Constraint Logic Programming over Boolean variables). The core constraint ensures that for each square (column), exactly one of the relevant placement variables is true using sat/1.
8:36 Representing Tiles and Board Positions: Tiles are represented as lists of lists of integers (0s and 1s). A Definite Clause Grammar (DCG) is employed to describe how a tile's shape maps to a "row" of 0s and 1s in the boolean matrix, effectively handling placement positions on the board.
11:40 Core Logic: sat/1 and tfilter/4: The sat/1 predicate from clpb confirms the satisfiability of the boolean expression, while tfilter/4 is used to filter variables based on whether a placement covers a specific square.
16:50 Handling Geometric Rules in Boolean Model: Even with a boolean model, some geometric rules (e.g., a domino not extending across rows) still require explicit constraints within the boolean formulation.
20:11 Demonstrating with a 2x2 Board: The program is demonstrated on a small 2x2 chessboard, successfully generating the matrix of possible placements and finding the two distinct tiling solutions using labeling.
26:02 Counting Solutions with sat_count/2: A key feature of CLP(B) is the ability to count the number of solutions for a given boolean expression. This is shown to be efficient, especially when reifying the constraints to avoid costly residual goal projections.
32:45 Fault-Free Tilings: The program's versatility is highlighted by showing how it can be extended to find "fault-free" tilings by adding specific disjunctive constraints that ensure no straight line (horizontal or vertical) on the board can pass through an uncovered section.
37:31 Binary Decision Diagrams (BDDs) Explained: The video explains that CLP(B) internally uses Reduced and Ordered Binary Decision Diagrams (ROBDDs). BDDs are canonical, compact graph representations of boolean functions, enabling efficient operations like satisfiability checks and solution counting.
39:30 Zero-Suppressed BDDs (ZDDs): A more efficient variant, ZDDs, is mentioned as beneficial for problems where solutions tend to have many variables set to false.
40:21 Unique Properties of CLP(B): CLP(B) offers unique advantages: it's a complete constraint solver (deriving all consequences), can count all solutions, and allows for selecting uniformly random solutions.
41:06 Performance Considerations and NP-Completeness: While powerful, posting sat constraints can be computationally intensive for some problems due to the NP-completeness of Boolean satisfiability. Factors like variable and constraint ordering significantly impact efficiency.
44:32 Optimizations and Future Development: Suggestions for improving performance include sorting input data, using ZDDs, and optimizing the underlying Prolog engine (e.g., JIT compilation, hash tables, or integrating Rust components). These are proposed as ambitious thesis projects.
47:29 High-Level Interface and Design Philosophy: CLP(B) provides a high-level, declarative interface that abstracts away BDD internals, allowing for flexible underlying implementations. This leads to a discussion on whether to expose more low-level BDD operations for greater control or maintain abstraction for changeability and to encourage creative problem-solving.
50:22 The Mutilated Chessboard Problem: The video concludes with the classic mutilated chessboard problem (a chessboard with two opposite corners removed). While CLP(B) can computationally prove its insolvability, human insight (color argument) provides a much faster and elegant proof, illustrating the powerful synergy between computational tools and genuine human creativity in problem-solving.