Компонент EvoGuessAI предназначен для поиска декомпозиционных множеств и их использования для решения SAT-экземпляров. Поиск декомпозиционных множеств осуществляется посредством оптимизации специальных псевдобулевых "black-box" функций, которые оценивают либо значение ρ в случае использования EvoguessAI в режиме ρ-backdoors, либо сложность декомпозиции, соответствующую используемому методу декомпозиции и рассматриваемому множеству в случае режима IBS. Для оптимизации значения таких функций используются метаэвристические алгоритмы, в частности, эволюционные.
git clone git@github.com:ctlab/evoguess-ai.git
cd evoguess-ai
pip install -r requirements.txtОбязательные пакеты:
-
numpy (>=1.21.6)
pip install numpy
-
python-sat (~=1.8.dev4) – PySAT — это набор инструментов, предоставляющий удобные функции для использования оракулов SAT.
pip install python-sat
Необязательные пакеты:
- tqdm – пакет для логирования процесса.
pip install tqdm
EvoGuessAI поддерживает использование ρ-лазеек (ρ-backdoors) для решения SAT относительно СNF и MaxSAT относительно WCNF.
Кратко, ρ-лазейка — это лазейка, который позволяет разложить исходную CNF на два подмножества подзадач. Первое множество будет состоять из подзадач, которые SAT-оракул решает с учетом заданного ограничения по какой-либо мере (чаще всего, времени или числу конфликтов), второе — из всех остальных подзадач. Доля первого подмножества равна (ρ), второго — (1-ρ).
На практике (и в EvoGuessAI) такие лазейки стремятся максимизировать ρ. Соответственно, каждая лазейка будет генерировать небольшое количество сложных подзадач (также называемых hard tasks). Также можно использовать несколько лазеек для решения исходной задачи. При этом для множеств сложных задач, полученные от разных лазеек, строится их декартово произведение.
EvoGuessAI способен находить лазейки, максимизируя значение ρ. Затем запускается итерационный процесс отфильтровывания сложных задач. На каждой итерации строится декартово произведение сложных задач из разных ρ-лазеек, а затем оно фильтруется для поиска новых сложных задач. В какой-то момент все сложные задачи начинают решаться для некоторого заданного ограничения (по времени или конфликтам). Если ρ-лазейки для построения декартовых произведений заканчиваются раньше, то заданное ограничение отключается, и все оставшиеся сложные задачи решаются как обычно.
python3 main_rho.py [-h] [-s [SOLVERNAME]] [-nr [NOFEARUNS]]
[-ni [NOFEAITERS]] [-np [NOFPROCESSES]]
[-bds [BACKDOORSIZE]] [-tl [TIMELIMIT]]
[-cl [CONFLICTLIMIT]] [-rs [RANDOMSEED]]
formula
| Полное имя параметра | Сокращение | Описание |
|---|---|---|
| formula | файл с входной формулой (в виде CNF или WCNF), является обязательным параметром | |
| --solvername | -s | краткое название SAT-решателя, используемого в качестве SAT-оракула. Доступные названия: g3 -- Glucose 3; cd, cd 15, cd19 -- различные версии Cadical (см. документацию PySAT) |
| --nofearuns | -nr | число запусков эволюционного алгоритма поиска ρ-лазеек. Каждый запуск может привести к генерации нескольких ρ-лазеек, если они имеют одинаковое значение ρ |
| --nofeaiters | -ni | число итераций эволюционного алгоритма за один запуск |
| --nofprocesses | -np | число выделяемых процессов для работы EvoguessAI в многопоточном режиме |
| --backdoorsize | -bds | размер ρ-лазеек (число переменных), которые ищутся |
| --timelimit | -tl | ограничение по времени для SAT-оракула при решении сложных задач |
| --conflictlimit | -cl | ограничение на число конфликтов для SAT-оракула при решении сложных задач. При запуске выбирается только одно из установленных ограничений, соответственно следует задать либо ограничение по времени, либо по числу конфликтов |
| --randomseed | -rs | случайный seed, который используется для поиска ρ-лазеек |
Пример:
python3 ./main_rho.py -f ./examples/data/pvs_4_7.cnf -s g3 -nr 40 -np 8 -bds 10 -tl 0 -cl 20000Этот скрипт запускает соответствующий пайплайн rho_solve.py, который находится в модуле pipeline.
Команда выше запустит EvoGuessAI в режиме ρ-backdoors для решения одной из образцовых CNF (задача LEC для алгоритмов «блинной» сортировки и «блинной» и сортировки «выбором» для восьми 3-битных чисел). В решении будет задействовано 8 процессов. Эволюционный алгоритм будет запущен 40 раз, при этом будут искаться ρ-лазейки из 10 переменных. Сложные задачи будут решаться с ограничением в 20,000 конфликтов на задачу.
Результат с комментариями:
00:00:01 ---------------------- Running on 4 threads ----------------------
00:00:01 -------------------------------------------------------------------
00:00:01 ------------------- Phase 1 (Prepare backdoors) -------------------
00:00:01 Searching: 100%|██████████| 40/40 [03:31<00:00, 5.29s/run, 7009 bds]
# На этапе 1 было найдено 7009 лазеек. Это были лазейки с максимальным rho из каждого потока.
00:03:33 Deriving: 100%|██████████| 608/608 [00:52<00:00, 11.65bd/s, 844 clauses]
# В процессе вывода из всех лазеек в исходную CNF было добавлено 844 дополнительных клозов.
00:04:25 ---------------------- Prepared 10 backdoors ----------------------
# Все лазейки были отфильтрованы от бесполезных (не несущих новых переменных).
# Осталось 10 лазеек.
00:04:25 -------------------------------------------------------------------
00:04:25 --------------------- Phase 2 (Solve problem) ---------------------
00:04:25 ------------------- Used 2 backdoors (20 vars) -------------------
00:04:25 Sifting: 100%|██████████| 4/4 [00:04<00:00, 1.06s/task, 4 hard]
# Сложные задачи от первых двух лазеек были использованы для построения декартового произведения. Его длина — 4 задачи.
# При решении этих 4 задач с ограничением по числу конфликтов оказалось, что все 4 слишком сложны.
# Поэтому добавляем следующую лазейку (строит декартово произведение текущего набора задач
# и сложных задач из следующей лазейки).
00:04:29 ------------------- Used 3 backdoors (22 vars) -------------------
00:04:29 Sifting: 100%|██████████| 8/8 [00:07<00:00, 1.14task/s, 8 hard]
00:04:36 ------------------- Used 4 backdoors (24 vars) -------------------
00:04:36 Sifting: 100%|██████████| 16/16 [00:15<00:00, 1.03task/s, 16 hard]
00:04:52 ------------------- Used 5 backdoors (26 vars) -------------------
00:04:52 Sifting: 100%|██████████| 32/32 [00:31<00:00, 1.02task/s, 32 hard]
00:05:23 ------------------- Used 6 backdoors (36 vars) -------------------
00:05:23 Sifting: 100%|██████████| 64/64 [01:03<00:00, 1.01task/s, 64 hard]
00:06:27 ------------------- Used 7 backdoors (38 vars) -------------------
00:06:27 Sifting: 100%|██████████| 128/128 [02:22<00:00, 1.11s/task, 125 hard]
00:08:49 ------------------- Used 8 backdoors (39 vars) -------------------
00:08:49 Sifting: 100%|██████████| 250/250 [05:41<00:00, 1.37s/task, 220 hard]
00:14:31 ------------------- Used 9 backdoors (42 vars) -------------------
00:14:31 Sifting: 100%|██████████| 440/440 [11:20<00:00, 1.55s/task, 394 hard]
00:25:51 ------------------- Used 10 backdoors (44 vars) -------------------
00:25:51 -------------- Disable solver budget (last backdoor) --------------
# Поскольку 10-ая лазейка был последней, оставшиеся сложные задачи решаются без ограничений.
00:25:51 Sifting: 100%|██████████| 788/788 [46:31<00:00, 3.54s/task, 0 hard]
01:12:23 -------------------------------------------------------------------
01:12:23 ---------------------------- Solution ----------------------------
01:12:23 -------------------------- UNSATISFIABLE --------------------------
# EvoguessAI доказал, что формула невыполнима.
01:12:23 -------------------------------------------------------------------
01:12:23 -------------------- Search time: 213.179 sec. --------------------
01:12:23 -------------------- Derive time: 52.396 sec. --------------------
01:12:23 ------------------- Solving time: 4077.635 sec. -------------------
01:12:23 -------------------------------------------------------------------
01:12:23 ------------------- Summary time: 4343.21 sec. -------------------Поиск ρ-лазеек с использованием островной модели задействует модуль lib_metalg который содержит соответсвующий алгоритм поиска.
python3 main_rho_im.py [-h] [-s [SOLVERNAME]] [-nl [NOFEALIMIT]]
[-ng [NOFEAGROUPS]] [-np [NOFPROCESSES]]
[-bds [BACKDOORSIZE]] [-tl [TIMELIMIT]]
[-cl [CONFLICTLIMIT]] [-rs [RANDOMSEED]]
formula
| Полное имя параметра | Сокращение | Описание |
|---|---|---|
| formula | файл с входной формулой (в виде CNF или WCNF), является обязательным параметром | |
| --solvername | -s | краткое название SAT-решателя, используемого в качестве SAT-оракула. Доступные названия: g3 -- Glucose 3; cd, cd 15, cd19 -- различные версии Cadical (см. документацию PySAT) |
| --nofealimit | -nl | число найденных ρ-бэкдоров, после которого алгоритм прекратит поиск. |
| --nofeagroups | -ni | число групп с различным значением ρ, которые могут существовать одновременно. |
| --nofprocesses | -np | число выделяемых процессов для работы EvoguessAI в многопоточном режиме |
| --backdoorsize | -bds | размер ρ-лазеек (число переменных), которые ищутся |
| --timelimit | -tl | ограничение по времени для SAT-оракула при решении сложных задач |
| --conflictlimit | -cl | ограничение на число конфликтов для SAT-оракула при решении сложных задач. При запуске выбирается только одно из установленных ограничений, соответственно следует задать либо ограничение по времени, либо по числу конфликтов |
| --randomseed | -rs | случайный seed, который используется для поиска ρ-лазеек |
Пример:
python3 ./main_rho_im.py -f /examples/data/pvs_4_7.cnf -s cd195 -nl 500 -ng 5 -bds 10 -cl 20000Этот скрипт запускает соответствующий пайплайн rho_solve_im.py, который находится в модуле pipeline.
Исследование проводится при поддержке Исследовательского центра сильного искусственного интеллекта в промышленности Университета ИТМО в рамках мероприятия программы центра: Разработка и испытания экспериментального образца библиотеки алгоритмов сильного ИИ в части решения задачи выполнимости булевой формулы посредством эвристик работы с ограничениями и переменными, поиска вероятностных лазеек и инверсных полиномиальных лазеек.
Документация по основным режимам использования EvoguessAI доступна в формате
Markdown файла
intro.md.
Также EvoguessAI поддерживает low level использование в качестве библиотеки. В этом режиме пользователь может использовать собственные реализации классов и функций. Документация для этого режима доступна здесь и включает в себя инструкции по установке и базовое руководство пользователя.