Моделирование логической головоломки - PullRequest
Новая
       49

Моделирование логической головоломки

0 голосов
/ 10 декабря 2018

Я пытаюсь смоделировать логическую головоломку из Чтобы издеваться над пересмешником .Я изо всех сил пытаюсь перевести его в SMT-LIB.Головоломка выглядит примерно так:

Есть сад, в котором все цветы красного, желтого или синего цвета и представлены все цвета.Для любых трех цветов, которые вы выбираете, по крайней мере один будет красным, а другой - желтым.Третий цветок всегда будет синим?

Я пытался смоделировать сад как Array Int Flower, но это не сработало, я полагаю, потому что область массива зафиксирована так, чтобы варьироватьсявсе целые числа.Z3 услужливо говорит мне, что это неудовлетворительно, CVC4 просто сразу возвращает неизвестное.

Единственное решение головоломки - это сад с ровно одним цветком каждого цвета, но как мне заставить решателя сказать мне это?

Это моя неудачная попытка: 

(declare-datatypes () ((Flower R Y B)))
(declare-const garden (Array Int Flower))
(assert (forall ((a Int) (b Int) (c Int))
                (and (or (= (select garden a) R)
                         (= (select garden b) R)
                         (= (select garden c) R))
                     (or (= (select garden a) Y)
                         (= (select garden b) Y)
                         (= (select garden c) Y)))))
(check-sat)

1 Ответ

0 голосов
/ 11 декабря 2018

Я думаю, что есть неявное предположение, что цветы всех трех цветов представлены в саду.Имея это в виду, вот как я мог бы написать кодирование с использованием интерфейсов Python и Haskell для Z3;потому что код на этих языках просто проще, чем непосредственно в SMTLib.

Python 

from z3 import *

# Color enumeration
Color, (R, Y, B) = EnumSort('Color', ('R', 'Y', 'B'))

# An uninterpreted function for color assignment
col = Function('col', IntSort(), Color)

# Number of flowers
N = Int('N')

# Helper function to specify distinct valid choices:
def validPick (i1, i2, i3):
    return And( Distinct(i1, i2, i3)
              , 1 <= i1, 1 <= i2, 1 <= i3
              , i1 <= N, i2 <= N, i3 <= N
              )

# Helper function to count a given color
def count(pickedColor, flowers):
    return Sum([If(col(f) == pickedColor, 1, 0) for f in flowers])

# Get a solver and variables for our assertions:
s = Solver()
f1, f2, f3 = Ints('f1 f2 f3')

# There's at least one flower of each color
s.add(Exists([f1, f2, f3], And(validPick(f1, f2, f3), col(f1) == R, col(f2) == Y, col(f3) == B)))

# You pick three, and at least one of them is red
s.add(ForAll([f1, f2, f3], Implies(validPick(f1, f2, f3), count(R, [f1, f2, f3]) >= 1)))

# You pick three, and at least one of them is yellow
s.add(ForAll([f1, f2, f3], Implies(validPick(f1, f2, f3), count(Y, [f1, f2, f3]) >= 1)))

# For every three flowers you pick, one of them has to be blue
s.add(ForAll([f1, f2, f3], Implies(validPick(f1, f2, f3), count(B, [f1, f2, f3]) == 1)))

# Find a satisfying value of N
print s.check()
print s.model()[N]

# See if there's any other value by outlawing the choice
nVal = s.model()[N]
s.add(N != nVal)
print s.check()

При запуске это печатает: 

sat
3
unsat

Способ прочитать этовывод состоит в том, что данные условия действительно выполняются при N=3;как вы пытались узнать.Кроме того, если вы также утверждаете, что N является , а не 3, то не существует удовлетворительной модели, т. Е. Выбор 3 обусловлен данными условиями.Я считаю, что это то, что вы хотели установить.

Я надеюсь, что код ясен, но не стесняйтесь спрашивать разъяснения.Если вам это нужно в SMT-Lib, вы всегда можете вставить: 

print s.sexpr()

перед вызовами на s.check() и увидеть созданный SMTLib.

Haskell

Также можно кодировать то же самое в Haskell / SBV.Посмотрите эту суть почти буквального кодирования того же самого: https://gist.github.com/LeventErkok/66594d8e94dc0ab2ebffffe4fdabccc9 Обратите внимание, что решение Haskell может использовать преимущества конструкции allSat SBV (которая возвращает все удовлетворяющие предположения), и более просто показать, что N=3 являетсяЕдинственное решение.

...