Z3py SMT кодирование следующих переменных и формул

Question

Я действительно новичок в решателях Z3 и SMT. У меня есть следующая проблема, которую я не знаю, как закодировать в Z3py.

В приведенной выше схеме N является множество узлов, таким образом, N = {Node1, Node2, node3, Node4, Node5, Node6, Node7}

Я это набор входов, I = { Я , я , я , я }

вывода множество выходов, O = {O , о, О }

G представляет собой группу, где для любых последовательных 2 выходов (O _я, О _J), если O _я генерируется первый выход и О _J является второй выход генерируется тогда, G _к является множеством узлов, которые были запланированы после генерации O _я и до генерации O _J, но, если O _J был создан до O _i, тогда G _k содержит все блоки, которые были запланированы до O _j. Планирование узлов задается другой программой. Например, в приведенном выше блок-схеме планирования узлов наряду с выработкой продукции выглядит следующим образом:

• Первый узел по расписанию = Node1
• Второй узел по расписанию = Node2
• Третий узел по расписанию = Node5
• Выход генерируется = O
• Четвертый узел запланирован = node3
• Пятый узел по расписанию = Node6
• Выход генерируется = O
• Шестой узел запланированную = Node4
• Пятый узел по расписанию = Node7
• Выход генерируется = O

Таким образом, из вышесказанного можно сказать, что G за (O , O) is = {Node3, Node6}

Но G для (O , О) является = {Node1, Node2, Node5}

Для выполнения каждого узла нам нужно задание, задание может реализовать 1 узел или ее набор узлов за раз.

Узел _{г, я} обозначает I ^й узел в группе G _г. Задача _{r, m} обозначает m ^th Задача в группе G _r.

Булевы переменные (может быть либо 0 или 1):

• е _{Узел г, я Задача г, т} представляет, если Узел _{г, я} отображается в Task _{г, т}
• Ду _{Узел R, I Узел с, J} представляет, если Узел _{s, j} зависит от узла _{r, i} i.e.если существует путь от узла _{г, я} к узлу _{S, J}
• DT _{Задача г, т Задача с, п} обозначает, является ли Задача _{S, N} зависит от задачи _{г, т}
• м _{Задача г, т} представляет собой, если есть любой узел отображается на целевой _{г, м}

Основываясь на приведенной выше информации, я должен сформулировать следующие уравнения в SMT.

1. Минимизация (Σ _{г, т} М _{Задача г, т})
2. М _{Задача г, т}> = е _{Узел г, я Задача r, m} (для всех i)
3. Σ _м е _{Узел г, я Задача г, т} = 1 (для всех г = I, O!) пример: е _{Узел г, я Задача г, т} + ж _{Узел г, я Задача г, т + 1} + ж _{Node R, I Задача г, т + 2} = 1 + 0 + 0 = Это говорит о том, что узел _{г, я} сопоставлен к задаче _{г, т} Поскольку F _{Node г, я задача г, т} = 1 (только один узел может быть отображен в 1 задачи в то время, но задача может быть отображен на нескольких узлах одновременно)
4. е _{узел г, я Задача s, m} = 0 (для всех г! = S)
5. F _{Узел г, я Задача г, т} = 1 (для всех г = I, О и т = I)
6. ф _{Узел R, I задачи r, m} = 0 (для всех r = I, O и m!= Я)
7. ДТ _{Задача г, т Задача с, п}> = F _{Узел R, I задач г, м} + F _{Узел с, J Задача с , п} + Д.Н. _{Узел R, I Узел с, J} - 2
8. ДТ _{Задача г, т Задача с, п}> = DT _{Задача г, т Задача т, л} + DT _{Задача т, л Задача с, п} - 1
9. ДТ _{Задача г, т Задача с, п} + DT _{задач s, N задач г , М} < = 1

Я не понимаю, как представлять переменные и эти формулы в формате SMT.

Answer 1

Я не уверен, как лучше всего ответить, потому что в этом вопросе содержится много ссылок на специфику, которые не указаны полностью. Например, что такое I, и O? Вероятно, вы спрашиваете, как добавить систему линейных неравенств. Или как указать проблемы с целыми переменными, которые могут быть либо 0, либо 1.

Одним из подходов является введение функции следующим образом:

 a = Function('a', IntSort(), IntSort(), IntSort()) 

Тогда «а» это функция, которая отображает пары целых чисел целое число. Вы можете объявить функцию 'n' аналогичным образом (но, я думаю, ваш пример на самом деле имеет некоторые опечатки, и вы используете n как функцию и как индексную переменную). Вы можете также объявлять функции f, h, q аналогичным образом.

Тогда в питона вы можете написать:

 N = 5 
    s = Solver() # create a solver context 
    for r in range(N): 
     for i in range(N): 
      for m in range(N): 
       if m != i: 
        s.add(f(n(r,i),a(r,m)) == 0) 

Это добавляет ограничения равенства на е, которые вы указали. Другие ограничения равенства и неравенства могут быть добавлены аналогичным образом. В конце вы спрашиваете, является ли результирующее состояние выполнимым.

print s.check() 
    print s.model() # print model for satisfiable outcome. 

и другие подходы, которые вы объявляете различные константы для разных версий ф. В конце концов, ваша предлагаемая проблема указывает, что вы всего лишь , записывая большую систему неравенств по переменным, созданным в разных способах .

E.g., вы можете создать и постоянную v:

v = Const('f(a[%d][%d],a[%d][%d])' % (r,m,r,i), IntSort()) 

вместо приложения функции.