Я использую z3 через привязки Python, чтобы найти решения для головоломки рассечения (подумайте Tangram ).Признаюсь, что я на самом деле не знаю, что я делаю, и рассматриваю это как интересный опыт обучения.
Большая часть кода посвящена геометрии, затем я создаю решатель без указания логики (вызывая z3.solver()), создайте загрузку переменных Bool и добавьте для них чисто логические ограничения.Также в миксе есть ограничения ровно 1 из n и самое большее 1 из n, созданные с использованием z3.PbEq() и z3.PbLe().
Моя программа работает, но проблемаогромен, и я делаю исчерпывающий поиск всех удовлетворительных моделей, поэтому я смотрю на недели и месяцы обработки.
Мой общий вопрос о том, могу ли я помочь z3 любым способом.Более конкретно я спрашиваю о трех областях, перечисленных ниже.Будучи невежественным, я слепо экспериментировал с параметрами, которые кажутся связанными.
Я понимаю, что на этот вопрос нет простых ответов.Я был бы признателен за указатели на материал или ключевые слова, чтобы найти свое продолжение, чтобы продолжить свое обучение этому предмету.
1) Явно выберите теорию:
Вместо z3.solver() Я попытался позвонить z3.solverFor('QF_FD').
Это само по себе не имело никакого значения.Есть ли способ узнать, какие существуют теории, чем они на самом деле пользуются, если я просто вызываю solver ()?Где я могу узнать о том, какая теория может подходить для моей проблемы?
2) Попробуйте включить параллелизм:
Я заметил, что моя программа не использует все ядра ЦП, которые должен иметь мой компьютерпредлагает.Вместо того, чтобы думать о том, как его распараллелить, я попытался понять, на что способен z3.
Я установил различные параметры, выбранные из вывода help (), которые звучали так, как будто они могут управлять параллелизмом / многопоточностью:
z3.set_param('parallel.enable', True)
z3.set_param('parallel.threads.max', 32)
z3.set_param('sat.local_search_threads', 3)
z3.set_param('sat.threads', 3)
Я получил другое поведение от этого.Программа выполнялась в несколько потоков и значительно разогревала мой компьютер по сравнению с другими запусками.Но, к сожалению, вместо постоянного набора удовлетворительных моделей я получил настройки по умолчанию, которые я не получил даже после нескольких дней обработки.
Где - кроме источника z3 - Могу ли я узнать о том, как это работает иможет быть, структурировать мою проблему так, чтобы ее можно было лучше распараллелить?
3) Другие неясные параметры.
Я также играл с этими:
z3.set_param('sat.lookahead_simplify', True)
z3.set_param('sat.acce', True)
z3.set_param('sat.pb.solver', 'solver')
Но ничего заметно не изменилось.Существуют ли объяснения того, что они означают на уровне между строкой из help () и реальным кодом?