smt - 有没有人可以帮我做smt作业？

Question

作业：实验室 4

在第二个 SMT 实验室练习（实验 4）中，我们将在 SMT 求解器（Frobenious Coin Problem 的一个实例）的帮助下解决 Chicken McNugget 问题。

假设一家快餐连锁店销售尺寸为 A=7、B=9、C=16 的炸鸡块包装盒。你和你的朋友饿了，想吃 X 块鸡块（自然数）。我们要解决的第一个问题是，是否有可能购买尺寸 A 的 U 盒、尺寸 B 的 V 盒和尺寸 C 的 W 盒，这样你就可以得到正好 X 个鸡块（没有剩余）。在第一部分（1 分）中，将其表述为一个 SMT 问题，并尝试针对给定的 A、B、C 值和 X=40 来解决它。首先确定您需要的逻辑，然后手动编码到 SMT 库中。在第二部分（1.5 分）检查 X0 = X+0, ..., X6 = X + 6 在 U0,V0,W0, ..., U6,V6,W6 方面也有类似的表示。在这种编码的帮助下，确定给出一个令人满意的解决方案的最小数字 X。那么 Y=X-1 就是上面固定的 A、B、C 值的 Chicken McNuggets 问题的解，这意味着它是不能用这种方式表示的最大数 Y，或者就鸡块而言，没有无论您购买了多少（U，V，W）给定尺寸（A，B，C）的盒子，而您的朋友确实吃了 Y 块，那么必须有一些剩余的块。为给定的具体 A、B、C 的这两个部分生成这两个 SMT LIB 编码并能够呈现解决方案（并手动修改和检查其他值）将为您提供实验室的一半分数（2.5） . 您需要携带自己的已安装笔记本电脑，并且可以使用 SMT 求解器进行演示（Web 界面还不够）。这意味着它是不能以这种方式表示的最大数字 Y，或者以鸡块表示，无论您购买多少给定尺寸（A，B，C）的（U，V，W）盒子，并且你的朋友确实吃了 Y 块，那么一定有一些剩下的块。为给定的具体 A、B、C 的这两个部分生成这两个 SMT LIB 编码并能够呈现解决方案（并手动修改和检查其他值）将为您提供实验室的一半分数（2.5） . 您需要携带自己的已安装笔记本电脑，并且可以使用 SMT 求解器进行演示（Web 界面还不够）。这意味着它是不能以这种方式表示的最大数字 Y，或者以鸡块表示，无论您购买多少给定尺寸（A，B，C）的（U，V，W）盒子，并且你的朋友确实吃了 Y 块，那么一定有一些剩下的块。为给定的具体 A、B、C 的这两个部分生成这两个 SMT LIB 编码并能够呈现解决方案（并手动修改和检查其他值）将为您提供实验室的一半分数（2.5） . 您需要携带自己的已安装笔记本电脑，并且可以使用 SMT 求解器进行演示（Web 界面还不够）。那么必须有一些剩余的部分。为给定的具体 A、B、C 的这两个部分生成这两个 SMT LIB 编码并能够呈现解决方案（并手动修改和检查其他值）将为您提供实验室的一半分数（2.5） . 您需要携带自己的已安装笔记本电脑，并且可以使用 SMT 求解器进行演示（Web 界面还不够）。那么必须有一些剩余的部分。为给定的具体 A、B、C 的这两个部分生成这两个 SMT LIB 编码并能够呈现解决方案（并手动修改和检查其他值）将为您提供实验室的一半分数（2.5） . 您需要携带自己的已安装笔记本电脑，并且可以使用 SMT 求解器进行演示（Web 界面还不够）。

我的 SMT 代码：

(set-logic QF_AUFNIA)

(declare-const u Int)
(declare-const v Int)
(declare-const w Int)
(declare-const x Int)


(assert (>= u 0))
(assert (>= v 0))
(assert (>= w 0))

(assert (= 40(+ (* u 7)(* v 9)(* w 16))))
(assert (= 40(+ (* u 7)(* v 9))))
(assert (= 40(+ (* v 9)(* w 16))))
(assert (= 40(+ (* u 7)(* w 16))))
(assert (= 40(* v 9)))
(assert (= 40(* u 7)))
(assert (= 40(* w 16)))




(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(declare-const x3 Int)
(declare-const x4 Int)
(declare-const x5 Int)
(declare-const x6 Int)
(declare-const u0 Int)
(declare-const u1 Int)
(declare-const u2 Int)
(declare-const u3 Int)
(declare-const u4 Int)
(declare-const u5 Int)
(declare-const u6 Int)
(declare-const v0 Int)
(declare-const v1 Int)
(declare-const v2 Int)
(declare-const v3 Int)
(declare-const v4 Int)
(declare-const v5 Int)
(declare-const v6 Int)
(declare-const w0 Int)
(declare-const w1 Int)
(declare-const w2 Int)
(declare-const w3 Int)
(declare-const w4 Int)
(declare-const w5 Int)
(declare-const w6 Int)
(declare-const y Int)

(assert (= x0 (+ x 0)))
(assert (= x1 (+ x 1)))
(assert (= x2 (+ x 2)))
(assert (= x3 (+ x 3)))
(assert (= x4 (+ x 4)))
(assert (= x5 (+ x 5)))
(assert (= x6 (+ x 6)))


(assert (= u0 (+ u 0)))
(assert (= u1 (+ u 1)))
(assert (= u2 (+ u 2)))
(assert (= u3 (+ u 3)))
(assert (= u4 (+ u 4)))
(assert (= u5 (+ u 5)))
(assert (= u6 (+ u 6)))

(assert (= v0 (+ v 0)))
(assert (= v1 (+ v 1)))
(assert (= v2 (+ v 2)))
(assert (= v3 (+ v 3)))
(assert (= v4 (+ v 4)))
(assert (= v5 (+ v 5)))
(assert (= v6 (+ v 6)))


(assert (= w0 (+ w 0)))
(assert (= w1 (+ w 1)))
(assert (= w2 (+ w 2)))
(assert (= w3 (+ w 3)))
(assert (= w4 (+ w 4)))
(assert (= w5 (+ w 5)))
(assert (= w6 (+ w 6)))

(assert (= x 40))
(assert (= x (+ (* u 7)(* v 9)(* w 16))))


(check-sat)
(exit)

我写了我的代码，但总是不能令人满意。据说，X 应该是可满足的。我几乎对每个数字都尝试了 X 以获得令人满意的结果，但它不起作用。有没有人可以帮助我？

标签： smt

Answer 1

你得到unsat一个非常简单的原因。考虑这一行：

(assert (= 40(* u 7)))

哪里u是一个Int值。Z3 可以很容易地确定没有这样的整数值，因为7没有除40。同样，由于类似的原因，您还有许多其他无法满足的约束。

这是一个推进的简单想法。如果有人给你u,v和w值，并要求你检查它们确实是一个正确的解决方案，你会如何编程？写下这些值必须满足的属性，并简单地断言它们。通过约束求解的魔力，您认为“检查”解决方案将成为“找到”解决方案。希望有帮助！

此外，当您提出具体和尖锐的问题时，堆栈溢出效果最好，而不是倾倒整个问题集。如果你提出具体的问题，你会得到更好的答案。祝你好运！