Домашнее задание: лабораторная работа 4
Во втором лабораторном упражнении для SMT (лабораторное занятие 4) мы собираемся решить задачу Chicken McNugget с помощью решателя SMT (пример проблемы с фробирующими монетами).
Предположим, что сеть быстрого питания продает коробки с кусочками жареной курицы размером A = 7, B = 9, C = 16. Ваши друзья и вы голодны и хотите съесть кусочки курицы Х (натуральное число). Первый вопрос, на который мы собираемся ответить, это то, можно ли купить U-ящики размера A, V-ящики размера B и W-ящики размера C, чтобы получить ровно X кусочков курицы (без остатка). В первой части (1 балл) сформулируйте это как проблему SMT и попытайтесь решить ее для заданных значений A, B, C и X = 40. Сначала определите нужный вам logi c, а затем введите кодировку SMT lib вручную. Во второй части (1.5 балла) проверьте, что X0 = X + 0, ..., X6 = X + 6 также имеют аналогичные представления в терминах U0, V0, W0, ..., U6, V6, W6. С помощью этого кодирования определяют минимальное число X, которое дает удовлетворительное решение. Тогда Y = X-1 является решением проблемы Цыпленка МакНуггетса для фиксированных значений A, B, C выше, что означает, что это наибольшее число Y, которое НЕ может быть представлено таким образом, или в терминах кусочков курицы. Независимо от того, сколько (U, V, W) коробок заданных размеров (A, B, C) вы покупаете, и ваши друзья едят ровно Y кусочков, тогда должно быть несколько оставшихся кусочков. Генерация этих двух кодировок SMT LIB для этих двух частей для конкретного бетона A, B, C и возможность представить решение (а также изменить и проверить его вручную на наличие других значений) даст вам половину баллов (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 почти с каждой цифрой, чтобы она была удовлетворительной, но она не работает. Кто-нибудь может мне помочь?