permanganate

docs.rs

Rust 中的布尔可满足性 Flow Free 求解器。

lib.rs:

permanganate

一个用于解决 Numberlink 及其变体（如移动游戏 Flow Free 和其扩展）的求解器。首先使用如 SquareBoardBuilder 或 builder 模块中的其他构建器构建一个棋盘对象。将其转换为棋盘对象，然后调用 solve()，消耗棋盘并返回棋盘的解决方案。

permanganate 可以在由 Sh 类型参数编码的通用棋盘形状上操作。这些形状必须实现 Shape 并将自动实现 FullShape。

内部结构

该软件包通过将问题表示为布尔可满足性问题（SAT），从该求解器中提取信息，并根据棋盘重新表示来驱动。早期对此领域的研究，如 Matt Zucker 的解决方案，依赖于“路径形状”的概念，这对于没有桥梁和扭曲的矩形棋盘是足够的。在这里，我们沿着与 Ben Torvaney 的项目 和 Sam Goldman 的工作 类似的方式进行了泛化。

高级概述如下

给定输入，将棋盘表示为无向图 G。一个顶点对应于游戏中的单元格，边自然地编码顶点之间的连接。通过使用尽可能一般的术语，我们可以表示地图特征，如桥梁和扭曲，以及超越矩形网格的单元格形状。

我们在 SAT 形式下做出以下断言

1. 每个顶点要么是一个“终点”（流的起点），要么是一个“路径”（从一端到另一端的路径的一部分）。所有单元格都必须着色，因此该顶点具有一些“归属”不等于空归属，0。如果 V 是一个终点，则恰好有一个入边与 V 具有相同的归属。否则，恰好有两个入边具有相同的归属。
2. 每条边要么属于0，意味着其端点有不同的归属，要么属于非零，意味着它与端点共享归属并且位于从具有相同归属的一个终端到另一个终端的路径上。

然后我们相应地解决并分配数据给图。这比回溯或基于图的算法解决方案更高效。