Я пробую разные решатели для игрушки проблема клики и с удивлением обнаружил, что или инструменты с использованием SAT кажется намного быстрее, чем z3. Мне интересно, не делаю ли я что-то не так, учитывая, что z3 так хорошо показывает себя в опубликованных тестах. Вот МВЕ:
Сначала создайте случайный граф со 150 вершинами:
# First make a random graph and find the largest clique size in it
import igraph as ig
import random
from tqdm import tqdm
random.seed(7)
num_variables = 150 # bigger gives larger running time gap between z3 and ortools grow
print("Making graph")
g = ig.Graph.Erdos_Renyi(num_variables, 0.6)
# Make a set of edges. Maybe this isn't necessary
print("Making set of edges")
edges = set()
for edge in tqdm(g.es):
edges.add((edge.source, edge.target))
Теперь используйте z3, чтобы найти максимальный размер клики:
import z3
z3.set_option(verbose=1)
myVars = []
for i in range(num_variables):
myVars += [z3.Int('v%d' % i)]
opt = z3.Optimize()
for i in range(num_variables):
opt.add(z3.Or(myVars[i]==0, myVars[i] == 1))
for i in tqdm(range(num_variables)):
for j in range(i+1, num_variables):
if not (i, j) in edges:
opt.add(myVars[i] + myVars[j] <= 1)
t = time()
h = opt.maximize(sum(myVars))
opt.check()
print(round(time()-t,2))
На моем ПК это занимает около 70 секунд.
Теперь сделайте то же самое, используя SAT от ortools.
from ortools.linear_solver import pywraplp
solver = pywraplp.Solver.CreateSolver('SAT')
solver.EnableOutput()
myVars = []
for i in range(num_variables):
myVars += [solver.IntVar(0.0, 1.0, 'v%d' % i)]
for i in tqdm(range(num_variables)):
for j in range(i+1, num_variables):
if not (i, j) in edges:
solver.Add(myVars[i] + myVars[j] <= 1)
print("Solving")
solver.Maximize(sum(myVars))
t = time()
status = solver.Solve()
print(round(time()-t,2))
На моем компьютере это занимает около 4 секунд.
Если вы увеличите num_variables, разрыв станет еще больше.
Я что-то делаю не так или это просто очень плохой случай для оптимизатора z3?
Обновлять
Оказывается, ortools, использующие SAT, по умолчанию являются многоядерными, используя 8 ядер, поэтому сроки несправедливы. Используя улучшение @AxelKemper, я теперь получаю (на другой машине):
Итак, Z3 Только в 2,5 раза медленнее, чем ortools.
Обновление 2
Используя улучшенный код @alias, который использует s.add(z3.PbGe([(x, 1) for x in myVars], k))
, теперь это занимает 30,4 секунды, что при делении на 8 быстрее, чем ortools!
@kaya3 Я не знаю. Я попробовал версию z3.And(myVars[i] >=0, myVars[i] <=1)
, но это ничего не изменило.
Просто комментарий, грубо говоря, z3 и CP-SAT используют одну и ту же базовую технологию (называемую LCG в сообществе Constraint Programming). Теперь CP-SAT также работает как решатель MIP и встраивает внутрь симплекс. Может быть, это поможет.
Я не согласен с более быстрым, чем or-tools. Можно сказать энергоэффективнее, чем or-tools, но быстрее — нет. Параллельный поиск SAT — открытая проблема. Так что параллельный SMT — открытая проблема.
@LaurentPerron Это справедливое замечание. Кроме того, Z3, к сожалению, снова намного медленнее, если вы просто увеличите 150 до 200.
Замена переменных Int
переменными Bool
уменьшила время выполнения z3py на 28%
на моей машине:
z3.set_option(verbose=1)
myVars = []
for i in range(num_variables):
myVars += [z3.Bool('v%d' % i)] # Bool rather than Int
opt = z3.Optimize()
for i in tqdm(range(num_variables)):
for j in range(i+1, num_variables):
if not (i, j) in edges:
opt.add(Not(And(myVars[i], myVars[j])))
t = time()
h = opt.maximize(Sum([If(myVars[i], 1, 0) for i in range(num_variables)]))
opt.check()
print(round(time()-t,2))
Это очень приятное улучшение! Вы знаете, как сделать z3 многоядерным?
К сожалению, set_option("parallel.enable", True)
здесь ничего не меняет.
Я тоже это заметил. Я предполагаю, что решатель не был реализован как многоядерный.
также CP-SAT не реализует разделение работы, поэтому понятие идеального параллелизма спорно :-)
@LaurentPerron Извините, я не совсем понимаю. CP-SAT, безусловно, быстрее, если вы используете больше ядер. Может быть, я не знаю, что такое разделение работы? Вы имеете в виду, что я мог бы провести тот же эксперимент, используя вместо этого CP-SAT, и установить solver.parameters.num_search_workers = 1
?
@LaurentPerron Или вы имели в виду, что CP-SAT всегда имеет идеальный параллелизм?
Нет. Он не разделяет работу. Он использует портфель работников с различными эвристиками.
Cp-sat не настроен на работу только с 1 воркером. Обычно при использовании 8 воркеров получается огромный выигрыш, еще больший прирост идет к 16, и немного лучшие решения, быстрее выше, но нет более быстрого доказательства оптимальности.
Пользовательский инструмент, такой как ortools, обычно трудно превзойти, поскольку он понимает только фиксированное количество доменов и использует преимущества параллельного оборудования. Решатель SMT блистает не скоростью, а тем, что он позволяет: комбинацией множества теорий (арифметика, структуры данных, булевы значения, вещественные числа, целые числа, числа с плавающей запятой и т. д.), так что это некорректное сравнение.
Сказав это, мы можем заставить z3 работать быстрее, используя три идеи:
Используйте Bool
вместо Int
, как предложил Аксель. z3 гораздо лучше работает с булевыми значениями как есть, вместо того, чтобы кодировать их через целые числа. См. этот более ранний ответ для общих советов по кодированию в z3.
Обычный решатель z3 гораздо лучше справляется со многими ограничениями по сравнению с оптимизатором. Хотя у оптимизатора определенно есть свое применение, избегайте его, если можете. Если для вашей проблемы можно использовать итеративный подход (т. е. получить решение и продолжать улучшать его, добавляя новые ограничения), определенно стоит попробовать. Конечно, не все проблемы оптимизации поддаются такой оптимизации на основе итераций, но когда это применимо, это может окупиться. (Одна из причин этого заключается в том, что оптимизация представляет собой гораздо более сложную задачу, из-за которой решатель может увязнуть в ненужных деталях. Вторая причина заключается в том, что в последние годы оптимизатору z3 не уделялось большого внимания по сравнению с решателями, поэтому он не не отставая от улучшений, которые были сделаны в основном решателе.По крайней мере, это мое впечатление.)
Используйте псевдобулевы равенства, для которых у z3 есть внутренняя тактика, позволяющая работать гораздо эффективнее. Для псевдобулевых ограничений увидеть этот ответ.
Собрав все эти идеи вместе, вот как я бы закодировал вашу проблему в z3:
import igraph as ig
import random
from time import *
import z3
# First make a random graph and find the largest clique size in it
from tqdm import tqdm
random.seed(7)
num_variables = 150 # bigger gives larger running time gap between z3 and ortools grow
print("Making graph")
g = ig.Graph.Erdos_Renyi(num_variables, 0.6)
# Make a set of edges. Maybe this isn't necessary
print("Making set of edges")
edges = set()
for edge in tqdm(g.es):
edges.add((edge.source, edge.target))
myVars = []
for i in range(num_variables):
myVars += [z3.Bool('v%d' % i)]
total = sum([z3.If(i, 1, 0) for i in myVars])
s = z3.Solver()
for i in tqdm(range(num_variables)):
for j in range(i+1, num_variables):
if not (i, j) in edges:
s.add(z3.Not(z3.And(myVars[i], myVars[j])))
t = time()
curTotal = 0
while True:
s.add(z3.PbGe([(x, 1) for x in myVars], curTotal+1))
r = s.check()
if r == z3.unsat:
break
curTotal = s.model().evaluate(total, model_completion=True).as_long()
print(r, curTotal, round(time()-t,2))
print("DONE total time = ", round(time()-t,2))
Обратите внимание на использование z3.PbGe
, которое вводит псевдологические ограничения. В моих экспериментах это работает быстрее, чем обычная версия ограничения; и если вы также предполагаете ускорение полного распараллеливания 8 ядер, я думаю, что это выгодно отличается от решения ortools.
Обратите внимание, что приведенный выше итеративный цикл закодирован линейным образом, т. Е. Мы запрашиваем решение curTotal+1
, увеличивая последнее решение, найденное z3, только на единицу при каждом вызове check
. За счет некоторого дополнительного программирования вы также можете реализовать рутину, подобную бинарному поиску, т. Е. Запросить удвоение последнего результата, и если unsat
уменьшить масштаб, чтобы найти оптимум, используя push
/pop
для управления стеком утверждений. Этот трюк может работать еще лучше, если он амортизируется в течение многих прогонов.
Пожалуйста, сообщите о результатах собственных экспериментов!
Спасибо. Замедление в 2,5 раза уже учитывает распараллеливание. Может быть, оптимизатор z3 можно заставить выводить промежуточные решения, чтобы избежать явного поиска?
Я не думаю, что оптимизатор z3 генерирует какой-либо «промежуточный» результат, на который можно положиться. Для некоторых переменных он сохраняет связанную информацию, но до тех пор, пока не будет получено решение, они могут быть ненадежными. Смотрите обсуждение здесь: stackoverflow.com/q/55363925/936310
Может быть, хороший вопрос для их github.
@graffe Похоже, что использование псевдобулевых ограничений заставляет z3 работать намного быстрее. Смотрите мой обновленный ответ. Я хотел бы посмотреть, поэкспериментируете ли вы с ним и узнаете, какие результаты синхронизации вы получите по сравнению с ortools. (Конечно, после факторинга для распараллеливания.)
30 секунд! Это довольно удивительно
К сожалению, если вы увеличите число от 150 до 200, z3 снова остановится, и ortools очень быстро найдет оптимальный ответ (14). Вы видите то же самое?
Я не удивлен .. Я внес небольшое изменение, которое вместо увеличения на единицу пытается работать быстрее, пытаясь найти «лучшее» решение по сравнению с прошлым разом. Увы, в моем маленьком тесте он тоже ходил по пространству один за другим. Я думаю, что эксперименты с идеей бинарного поиска могут окупиться. (т. е. запросите решение в два раза лучше, затем удвойте его, пока не получите unsat
, затем уменьшите масштаб, чтобы найти оптимальное.) Но с очень большими графиками вам придется уступить специальным инструментам, таким как ortools, чтобы выйти вперед. . Я сомневаюсь, что вы можете многое сделать для дальнейшего масштабирования.
В качестве альтернативы можно было бы написать «специальную» тактику в z3 для решения подобных проблем. Но поиск максимальной клики — это NP-полная задача, и, как правило, вы не можете рассчитывать на то, что пользовательский решатель превзойдет стандартный SMT-решатель для такой задачи. (т.е. в лучшем случае вы продублируете алгоритмы ortools в z3, но какой в этом смысл?)
Я не согласен с понятием пользовательского решателя и универсального решателя. API-интерфейсы для модели z3 и моделей or-tools очень похожи. Таким образом, разница заключается только во времени, затраченном на выполнение инженерных работ на серверной части.
@Laurent Perron Я уверен, что люди из z3 были бы признательны за вклад, который поможет ему быстрее справляться с проблемами такого рода! Однако это проблема ограниченных человеческих ресурсов; не уверен, достаточно ли ROI для инвестирования в z3, чтобы сделать это, если есть лучшие инструменты для их решения более эффективно.
Любопытно, что ваш новый код вообще не пропускает никаких значений. bpa.st/JW7A
да я тоже это заметил. вы действительно хотите реализовать идею «бинарного поиска», чтобы воспользоваться преимуществом пропуска значений.
Я не уверен, что оно того стоит. Сумма времен для всех, кроме оптимального, намного меньше, чем время только для оптимального значения. Интересно, что ваш предыдущий код до улучшения PbGe пропускал значения.
Наверное, действительно не стоит. Если вы можете начать с более разумного значения (вместо 0), это, вероятно, может помочь. Это может быть возможно в зависимости от проблемы; возможно, у вас есть некоторое ожидание того, каким должно быть значение, благодаря предварительному знанию формы графика? Но, конечно, это второстепенные аспекты проблемы; не имеет прямого отношения к ускорению z3.
Действительно ли
z3.Or(myVars[i]==0, myVars[i] == 1)
правильный способ сделать переменную int равной 0 или 1? Я отмечаю, что ваша другая программа может напрямую указывать границы, что может помочь ей вывести границы для арифметических ограничений.