SMT 语法中的矩形拟合（Z3 求解器）

Posted 2023-02-25

【中文标题】SMT 语法中的矩形拟合（Z3 求解器）

【英文标题】：Rectangle fitting in SMT syntax (Z3 solver)

【发布时间】：2022-01-11 04:29:37

【问题描述】：

我尝试将 N 个不同大小的矩形块放入一个网格中，通过公式化 作为 CSP 问题。 块不应相互重叠，它们可以接触到边缘，并且可以有 空的地方。 例如，将 4 个 2x2 大小的矩形块放入 8x8 网格中。 （改变块的数量、块的大小和网格的大小。）我知道公式为

我尝试编写程序或脚本来生成公式，但我很困惑，我无法用 SMT 语法编写。如果有人帮助我，我会感激不尽。谢谢。

【问题讨论】：

解决你的（作业？）问题：选择你的决策变量；定义每个变量的类型和值范围；定义约束；将您的模型翻译成SMT2 语法；运行 Z3。如果您在路上遇到困难，请发布一个具体问题。

您可能会从我为related question 发布的MinizInc model 中受益。

【参考方案1】：

您应该具体说明您尝试了什么，什么没有奏效。如果您的问题与语法有关，那么这里有一些帮助您入门的方法：

(set-option :produce-models true)

(declare-fun xi () Int)
(declare-fun wi () Int)
(declare-fun xj () Int)
(declare-fun wj () Int)

(assert (or (<= (+ xi wi) xj)
            (<= (+ xj wj) xi)))

上面对公式中的前两个析取进行了编码。您可以根据需要添加其他变量并断言所有其他条件。