Как кодировать проблему задания частоты в Z3 как Max-SMT - PullRequest
Новая
       118

Как кодировать проблему задания частоты в Z3 как Max-SMT

2 голосов
/ 30 октября 2019

Я пытаюсь закодировать Проблема назначения частот (точнее, Экземпляр 6) через Z3 в Python, используя информацию из статьи О SAT Modulo Theories и задачах оптимизации , который я постараюсь кратко описать.

Проблема состоит в назначении частот парам радиолиний таким образом, чтобы были соблюдены некоторые ограничения. Каждую частоту следует выбирать из конечного набора Di , и ограничения имеют вид: 

|fi − fj| > k (soft, comes with a cost associated )

|fi - fj| = d (hard)

fi = pi (pre-assignment, hard)

В документе описывается, как домены можно рассматривать как несвязное объединение четырех наборов:

{2 + 14m | 1 ≤ m ≤ 11}
{2 + 14m | 18 ≤ m ≤ 28}
{8 + 14km | 29 ≤ m ≤ 39}
{8 + 14m | 46 ≤ m ≤ 56}

И что мы можем выразить, что fi находится в Di с: 

ti  → (1 ≤ mi ≤ 11   ∨ 18 ≤ mi ≤ 28)

¬ti → (29 ≤ mi ≤ 39  ∨ 46 ≤ mi ≤ 56)

, где ti указывает, является ли fi 2 по модулю 14 или нет, а mi представляет fi mod 14 .

Что касаетсяограничения, это будет зависеть от ti и tj . Их можно записать как 

| 2 + 14mi - 8 - 14mj | > k

, когда (ti ∧ ¬tj) , и после некоторых манипуляций мы получим: 

(ti ∧ ¬tj ) → ( mi−mj ≥ floor((k+6)/14 + 1 ∨  mi−mj ≤ ceil((-k-6)/14) - 1)

Мне удалось использоватьэто кодирование с помощью SolverFor ('QF_LIA'), и оно возвращает unsat , поскольку экземпляр невозможен.

Что мне не удалось сделать, так это кодировать его как Max-SMTпроблема.

Я попытался вместо этого использовать Оптимизировать и добавить мягкие ограничения с их весами, просто утверждая жесткие, но Z3 часами не дает мне ответа.

В статье говорится окаждое превращающееся взвешенное предложение 

(Ci, wi) into (Ci ∨ pi)

, где pi - свежая пропозициональная переменная, а затем с использованием: 

pi → (ki = wi)         ¬pi → (ki = 0)

для весов. Но я еще не совсем понял.

Вопрос 1

Означает ли это, что 

 (ti ∧ ¬tj ) → ( mi−mj ≥ floor((k+6)/14 + 1 ∨  mi−mj ≤ ceil((-k-6)/14) - 1)

становится

  ((ti ∧ ¬tj ) → ( mi−mj ≥ floor((k+6)/14 + 1 ∨  mi−mj ≤ ceil((-k-6)/14) - 1) ∨ pi)

?

Вопрос 2

Как мне его кодировать, если я хочу минимизировать затраты и увидетьего ценность? Спасибо,

Редактировать

После публикации вопроса я потратил некоторое время на его взлом. Удалось заставить его работать на другом экземпляре (SUBCELAR6 / CELAR6-SUB0, который является небольшим под экземпляром экземпляра 6), но найденная стоимость (574) превышает оптимальную (159) найденную здесь

Репо можно найти здесь с набором данных , но основная часть: 

import mongoengine as me
from models import Graph
from z3 import *
from math import ceil, floor

me.connect(db='tcc')

instance = next(Graph.objects(name='scen06')) 

Vars = instance.var 
Doms = instance.dom
Ctrs = instance.ctr


weights = {
 1 : 1000,
 2 :  100,
 3 :   10,
 4 :    1
}


s = Optimize()

for ctr in Ctrs:

  ti = Bool('t_%d' % ctr.first_var)
  tj = Bool('t_%d' % ctr.second_var)
  mi = Int('m_%d'  % ctr.first_var)
  mj = Int('m_%d'  % ctr.second_var)
  k  = ctr.deviation

  # ti  → (1  ≤ mi ≤ 11 ∨ 18 ≤ mi ≤ 28)
  # ¬ti → (29 ≤ mi ≤ 39 ∨ 46 ≤ mi ≤ 56)

  # Encoding the domain of Fi

  s.add(Implies(ti,      Or( And(1  <= mi, mi <= 11),  And(18 <= mi, mi <= 28))))
  s.add(Implies(Not(ti), Or( And(29 <= mi, mi <= 39),  And(46 <= mi, mi <= 56))))

  # Encoding the domain of Fj
  s.add(Implies(tj     , Or(And(1  <= mj, mj <= 11), And(18 <= mj, mj <= 28))))
  s.add(Implies(Not(tj), Or(And(29 <= mj, mj <= 39), And(46 <= mj, mj <= 56))))

  if ctr.operator == '=':
    # (ti ∧ ¬tj )
    s.add(Implies(And(ti,Not(tj)), Or(mi - mj == floor((k+6)/14) + 1, mi - mj == ceil((-k+6)/14) -1 )))

    # (¬ti ∧ tj)
    s.add(Implies(And(Not(ti),tj), Or(mi - mj == math.floor((k-6)/14) + 1, mi - mj == ceil((-k-6)/14) -1 )))

    # (ti ∧ tj)
    s.add(Implies(And(ti,tj), Or(mi - mj == math.floor(k/14) + 1, mi - mj == ceil(-k/14) -1 )))

    # (¬ti ∧ ¬tj)
    s.add(Implies(And(Not(ti),Not(tj)),   Or(mi - mj == math.floor(k/14) + 1, mi - mj == ceil(-k/14) -1 )))



  # encoding the soft constraints
    if ctr.operator == '>':

        weight = costs[ctr.weight]

        # (ti ∧ ¬tj)
        s.add_soft(
            Implies(And(ti, Not(tj)), Or( mi - mj >= floor((k+6)/14) + 1,  mi - mj <= ceil((-k+6)/14) -1 )),
            weight
        )

        # (¬ti ∧ tj)
        s.add_soft(
            Implies( And(Not(ti), tj), Or( mi - mj >= floor((k-6)/14) + 1,   mi - mj <= ceil((-k-6)/14) - 1 )),              
            weight
        )

        # (ti ∧ tj)
        s.add_soft(
            Implies(And(ti,tj) ,    Or( mi - mj >= floor(k/14) + 1   ,      mi - mj <= ceil(-k/14) -1   )),
            weight
        )


        # (¬ti ∧ ¬tj)
        s.add_soft(
            Implies(And(Not(ti), Not(tj)), Or(mi - mj >= floor(k/14) + 1,    mi - mj <= ceil(-k/14) -1 ))
            , weight
        )



print(s.check())

m = s.model()
print([ m.evaluate(o) for o in s.objectives() ])
...