The mmin/mmax Table Modes in Picat

[Neng-Fa Zhou]

Below is the abstract of the talk I gave at the PIP workshop. 

Cheers,

NF

Picat's tabling mechanism has long supported optimization through the min/max table modes, which retain only one optimal answer for each tabled call. While sufficient for many optimization problems, these modes are inadequate when all optimal solutions are required. This presentation introduces the new mmin/mmax table modes, which preserve all minimum or maximum answers for each tabled call. The new mmin/mmax modes extend Picat's tabling framework with a practical and expressive mechanism for multi-optimal computation, broadening the range of optimization algorithms that can be implemented concisely and efficiently in Picat.

The presentation first gives the operational semantics of the new modes, explaining how answers are inserted, compared, and maintained during table evaluation, and how the modes interact with Picat's linear-tabling mechanism. The presentation also demonstrates the usefulness of the new modes through two application examples. The first shows how mmin can be used to compute all shortest paths in a graph, as required by the 2024 Advent of Code Day 16 problem [1]. The second presents a more advanced application in SAT encoding for the single-constant multiplication (SCM) constraint [2]. By exploiting mmin, a dynamic programming algorithm enumerates all near-optimal decompositions of intermediate subproblems, allowing the encoder to make globally informed choices that lead to smaller and higher-quality SAT encodings.

1) https://github.com/nfzhou/aoc/blob/main/2024/aoc_24_16_part2.pi

2) https://github.com/nfzhou/Picat/blob/master/scm.pi