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

【问题标题】：Is there anyone, who can help me with my smt homework?有没有人可以帮我做smt作业？
【发布时间】：2020-01-27 19:47:55
【问题描述】：

家庭作业：实验室 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 求解器进行演示（网络界面还不够）。

我的 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 以获得令人满意的结果，但它不起作用。有没有人可以帮助我？

【问题讨论】：

这是什么语言？
@sleepToken 和其他反对者，虽然这是一个家庭作业问题，但这是 OP 在提问之前努力解决问题的罕见情况。对于一个新的贡献者，我认为我们的反应有点混乱。
@noany，请在发帖前阅读此内容
@CoreyOgburn OP 收到的严厉反应很可能是滥用与问题本身无关的标签如java、python 和c++ 的结果。观看这些标签的人更多（与smt 标签相比），由于每天收到大量问题，他们往往更严格地遵守规则。不过，我投票支持重新打开这个问题，因为它是一个合适的smt 问题，并且 OP 在询问之前表现出足够的努力。
@noany SMT-LIB 可以增量使用，这意味着您可以在同一个公式中解决不同的问题。但是，您应该查看(push 1) 和(pop 1) 命令。你得到unsat，因为你以增量方式提供了冲突的约束，不可能同时满足。 - 你问题的第二部分对我来说完全不清楚。你应该计算什么？

标签： smt

【解决方案1】：

您收到unsat 的原因很简单。考虑这一行：

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

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

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

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

【讨论】：