SAT решатель

Компьютерная программа для задачи булевой выполнимости

В информатике и формальных методах решатель SAT — это компьютерная программа , которая направлена ​​на решение проблемы выполнимости булевых уравнений . При вводе формулы над булевыми переменными, такими как «( x или y ) и ( x или не y )», решатель SAT выводит, является ли формула выполнимой , то есть существуют возможные значения x и y , которые делают формулу истинной, или невыполнимой, то есть таких значений x и y нет . В этом случае формула выполнима, когда x является истинным, поэтому решатель должен вернуть «выполнимо». С момента появления алгоритмов для SAT в 1960-х годах современные решатели SAT превратились в сложные программные артефакты, включающие большое количество эвристик и оптимизаций программы для эффективной работы.

Согласно результату, известному как теорема Кука–Левина , булева выполнимость является NP-полной проблемой в целом. В результате известны только алгоритмы с экспоненциальной сложностью в худшем случае. Несмотря на это, в 2000-х годах были разработаны эффективные и масштабируемые алгоритмы для SAT, которые способствовали резкому прогрессу в способности автоматически решать примеры задач, включающие десятки тысяч переменных и миллионы ограничений. ^[1]

Решатели SAT часто начинают с преобразования формулы в конъюнктивную нормальную форму . Они часто основаны на основных алгоритмах, таких как алгоритм DPLL , но включают ряд расширений и функций. Большинство решателей SAT включают тайм-ауты, поэтому они завершат работу в разумные сроки, даже если не смогут найти решение, с выводом типа «неизвестно» в последнем случае. Часто решатели SAT не просто предоставляют ответ, но могут предоставить дополнительную информацию, включая пример назначения (значения для x , y и т. д.) в случае, если формула выполнима или минимальный набор невыполнимых предложений, если формула невыполнима.

Современные решатели SAT оказали значительное влияние на такие области, как проверка программного обеспечения , анализ программ , решение ограничений , искусственный интеллект , автоматизация электронного проектирования и исследование операций . Мощные решатели легко доступны в виде бесплатного и открытого программного обеспечения и встроены в некоторые языки программирования, например, выставляя решатели SAT как ограничения в программировании логики ограничений .

Обзор

Булева формула — это любое выражение, которое можно записать с использованием булевых (пропозициональных) переменных x, y, z, ... и булевых операций AND, OR и NOT. Например,

( x И y ) ИЛИ ( x И (НЕ z ))

Назначение состоит из выбора для каждой переменной назначения ИСТИНА или ЛОЖЬ. Для любого назначения v булева формула может быть оценена и принимает значение истина или ложь. Формула выполнима, если существует назначение (называемое удовлетворяющим назначением ), для которого формула принимает значение истина.

Проблема выполнимости булевой формулы — это задача принятия решения , которая требует на входе булевой формулы определить, выполнима ли эта формула или нет. Эта задача является NP-полной .

Основные алгоритмы

Решатели SAT обычно разрабатываются с использованием одного из двух основных подходов: алгоритма Дэвиса–Патнэма–Логеманна–Лавленда (DPLL) и обучения на основе конфликтных положений (CDCL).

ДПЛЛ

Решатель DPLL SAT использует систематическую процедуру поиска с возвратом для исследования (экспоненциального размера) пространства переменных назначений в поисках удовлетворяющих назначений. Основная процедура поиска была предложена в двух основополагающих работах в начале 1960-х годов (см. ссылки ниже) и теперь обычно называется алгоритмом DPLL . ^{[2] [3]} Многие современные подходы к практическому решению SAT выводятся из алгоритма DPLL и имеют ту же структуру. Часто они повышают эффективность только определенных классов задач SAT, таких как примеры, которые появляются в промышленных приложениях или случайно сгенерированные примеры. ^[4] Теоретически, экспоненциальные нижние границы были доказаны для семейства алгоритмов DPLL. ^{[ необходима ссылка ]}

CDCL

Современные решатели SAT (разработанные в 2000-х годах) бывают двух видов: «управляемые конфликтами» и «упреждающие». Оба подхода происходят от DPLL. ^[4] Решатели, управляемые конфликтами, такие как обучение на основе положений конфликта (CDCL), дополняют базовый алгоритм поиска DPLL эффективным анализом конфликтов, обучением на основе положений, обратным переходом , формой распространения единиц «два наблюдаемых литерала» , адаптивным ветвлением и случайными перезапусками. Было эмпирически показано, что эти «дополнения» к базовому систематическому поиску необходимы для обработки больших экземпляров SAT, которые возникают в автоматизации электронного проектирования (EDA). ^[5] Большинство современных решателей SAT основаны на фреймворке CDCL по состоянию на 2019 год. ^[6] Известные реализации включают Chaff ^[7] и GRASP . ^[8]

Решатели с опережающим просмотром особенно усилили сокращения (выходящие за рамки распространения единичного предложения) и эвристики, и они, как правило, сильнее решателей, управляемых конфликтами, на сложных экземплярах (в то время как решатели, управляемые конфликтами, могут быть намного лучше на больших экземплярах, которые на самом деле имеют внутри простой экземпляр). ^{[ необходима цитата ]}

MiniSAT, основанный на конфликтах и ​​относительно успешно работавший на конкурсе SAT 2005 года, содержит всего около 600 строк кода. Современный решатель Parallel SAT — ManySAT. ^[9] Он может достигать сверхлинейных ускорений для важных классов задач. Примером решателей с опережающим просмотром является march_dl, завоевавший приз на конкурсе SAT 2007 года. Решатель CP-SAT от Google, входящий в состав OR-Tools , завоевал золотые медали на конкурсах Minizinc по программированию ограничений в 2018, 2019, 2020 и 2021 годах.

Определенные типы больших случайных выполнимых примеров SAT могут быть решены методом распространения опроса (SP). ^{[ необходима ссылка ]} В частности, в приложениях проектирования и верификации оборудования выполнимость и другие логические свойства заданной пропозициональной формулы иногда определяются на основе представления формулы в виде двоичной диаграммы решений (BDD).

Разные решатели SAT найдут разные примеры легкими или сложными, и некоторые преуспеют в доказательстве невыполнимости, а другие в поиске решений. Все эти модели поведения можно увидеть в соревнованиях по решению SAT. ^[10]

Параллельные подходы

Параллельные решатели SAT делятся на три категории: алгоритмы портфолио, «разделяй и властвуй» и параллельные алгоритмы локального поиска . При параллельных портфолио несколько различных решателей SAT работают одновременно. Каждый из них решает копию экземпляра SAT, тогда как алгоритмы «разделяй и властвуй» делят задачу между процессорами. Существуют различные подходы к распараллеливанию алгоритмов локального поиска.

Международный конкурс SAT Solver Competition имеет параллельный трек, отражающий последние достижения в параллельном решении SAT. В 2016, ^[11] 2017 ^[12] и 2018, ^[13] тесты проводились на системе с общей памятью с 24 процессорными ядрами , поэтому решатели, предназначенные для распределенной памяти или многоядерных процессоров, могли не соответствовать требованиям.

Портфолио

В общем, не существует решателя SAT, который бы работал лучше всех других решателей для всех задач SAT. Алгоритм может хорошо работать для экземпляров задач, с которыми другие борются, но будет работать хуже с другими экземплярами. Кроме того, при наличии экземпляра SAT нет надежного способа предсказать, какой алгоритм решит этот экземпляр особенно быстро. Эти ограничения мотивируют подход параллельного портфеля. Портфель — это набор различных алгоритмов или различных конфигураций одного и того же алгоритма. Все решатели в параллельном портфеле работают на разных процессорах для решения одной и той же задачи. Если один решатель завершает работу, решатель портфеля сообщает, что задача выполнима или невыполнима в соответствии с этим решателем. Все остальные решатели завершаются. Диверсификация портфелей путем включения различных решателей, каждый из которых хорошо работает на разных наборах задач, повышает надежность решателя. ^[14]

Многие решатели используют генератор случайных чисел внутри себя . Диверсификация их семян — простой способ диверсификации портфеля. Другие стратегии диверсификации включают включение, отключение или диверсификацию определенных эвристик в последовательном решателе. ^[15]

Одним из недостатков параллельных портфелей является объем дублирующей работы. Если обучение предложениям используется в последовательных решателях, совместное использование изученных предложений между параллельно работающими решателями может сократить дублирующую работу и повысить производительность. Тем не менее, даже простое параллельное выполнение портфеля лучших решателей делает параллельный решатель конкурентоспособным. Примером такого решателя является PPfolio. ^{[16] [17]} Он был разработан для поиска нижней границы производительности, которую параллельный решатель SAT должен быть в состоянии обеспечить. Несмотря на большой объем дублирующей работы из-за отсутствия оптимизаций, он хорошо показал себя на машине с общей памятью. HordeSat ^[18] — это параллельный решатель портфеля для больших кластеров вычислительных узлов. Он использует по-разному настроенные экземпляры одного и того же последовательного решателя в своей основе. В частности, для жестких экземпляров SAT HordeSat может обеспечить линейное ускорение и, следовательно, значительно сократить время выполнения.

В последние годы решатели SAT с параллельным портфелем доминировали на параллельном треке Международных конкурсов решателей SAT. Известными примерами таких решателей являются Plingeling и painless-mcomsps. ^[19]

Разделяй и властвуй

В отличие от параллельных портфелей, параллельный «разделяй и властвуй» пытается разделить пространство поиска между элементами обработки. Алгоритмы «разделяй и властвуй», такие как последовательный DPLL, уже применяют технику разделения пространства поиска, поэтому их расширение в сторону параллельного алгоритма является прямым. Однако из-за таких техник, как распространение единиц, после деления частичные проблемы могут значительно отличаться по сложности. Таким образом, алгоритм DPLL обычно не обрабатывает каждую часть пространства поиска за одинаковое время, что приводит к сложной проблеме балансировки нагрузки . ^[14]

Фаза куба для формулы . Эвристика принятия решений выбирает, какие переменные (круги) назначить. После того, как эвристика отсечения решает прекратить дальнейшее ветвление, частичные проблемы (прямоугольники) решаются независимо с помощью CDCL. ${\displaystyle F}$

Из-за нехронологического возврата параллелизация обучения на основе конфликта затруднена. Одним из способов преодоления этого является парадигма «Cube-and-Conquer». ^[20] Она предполагает решение в два этапа. На этапе «куба» задача делится на многие тысячи, вплоть до миллионов, разделов. Это делается решателем с предварительным просмотром, который находит набор частичных конфигураций, называемых «кубами». Куб также можно рассматривать как конъюнкцию подмножества переменных исходной формулы. В сочетании с формулой каждый из кубов образует новую формулу. Эти формулы могут быть решены независимо и одновременно решателями, управляемыми конфликтом. Поскольку дизъюнкция этих формул эквивалентна исходной формуле, задача считается выполнимой, если одна из формул выполнима. Решатель с предварительным просмотром подходит для небольших, но сложных задач, ^[21] поэтому он используется для постепенного разделения задачи на несколько подзадач. Эти подзадачи проще, но все еще велики, что является идеальной формой для решателя, управляемого конфликтом. Кроме того, решатели с опережением рассматривают всю проблему, тогда как решатели, управляемые конфликтом, принимают решения на основе информации, которая является гораздо более локальной. В фазе куба задействованы три эвристики. Переменные в кубах выбираются эвристикой принятия решения. Эвристика направления решает, какое назначение переменных (истина или ложь) исследовать в первую очередь. В удовлетворяемых случаях проблемы выбор удовлетворяемой ветви первым является полезным. Эвристика отсечения решает, когда следует прекратить расширение куба и вместо этого направить его в последовательный решатель, управляемый конфликтом. Предпочтительно, чтобы кубы были одинаково сложными для решения. ^[20]

Treengeling — пример параллельного решателя, который применяет парадигму Cube-and-Conquer. С момента своего появления в 2012 году он имел множество успехов на Международном конкурсе решателей SAT. Cube-and-Conquer использовался для решения задачи булевых пифагорейских троек . ^[22]

Cube-and-Conquer — это модификация или обобщение подхода «разделяй и властвуй» на основе DPLL, который использовался для вычисления чисел Ван дер Вардена w(2;3,17) и w(2;3,18) в 2010 году ^[23] , где обе фазы (разделение и решение частичных задач) выполнялись с использованием DPLL.

Локальный поиск

Одна из стратегий в направлении параллельного локального алгоритма поиска для решения SAT заключается в попытке одновременного переключения нескольких переменных на разных процессорах. ^[24] Другая стратегия заключается в применении вышеупомянутого подхода портфеля, однако совместное использование положений невозможно, поскольку решатели локального поиска не создают положений. В качестве альтернативы можно совместно использовать конфигурации, которые создаются локально. Эти конфигурации могут использоваться для руководства созданием новой начальной конфигурации, когда локальный решатель решает перезапустить свой поиск. ^[25]

Рандомизированные подходы

Алгоритмы, не входящие в семейство DPLL, включают стохастические алгоритмы локального поиска . Одним из примеров является WalkSAT . Стохастические методы пытаются найти удовлетворяющую интерпретацию, но не могут сделать вывод о том, что экземпляр SAT невыполним, в отличие от полных алгоритмов, таких как DPLL. ^[4]

Напротив, рандомизированные алгоритмы, такие как алгоритм PPSZ Патури, Пудлака, Сакса и Зане, устанавливают переменные в случайном порядке в соответствии с некоторыми эвристиками, например, разрешением ограниченной ширины . Если эвристика не может найти правильную настройку, переменная назначается случайным образом. Алгоритм PPSZ имеет время выполнения ^{[ уточнить ]} для 3-SAT. Это было самое известное время выполнения для этой задачи до 2019 года, когда Хансен, Каплан, Замир и Цвик опубликовали модификацию этого алгоритма со временем выполнения для 3-SAT. Последний в настоящее время является самым быстрым известным алгоритмом для k-SAT при всех значениях k. В условиях со многими удовлетворяющими назначениями рандомизированный алгоритм Шенинга имеет лучшую границу. ^{[26] [27] [28]} ${\displaystyle O(1.308^{n})}$ ${\displaystyle O(1.307^{n})}$

Приложения

В математике

Решатели SAT использовались для помощи в доказательстве математических теорем с помощью компьютерного доказательства . В теории Рамсея несколько ранее неизвестных чисел Ван дер Вардена были вычислены с помощью специализированных решателей SAT, работающих на ПЛИС . ^{[29] [30]} В 2016 году Марийн Хойл , Оливер Куллманн и Виктор Марек решили задачу о булевых пифагорейских тройках, используя решатель SAT, чтобы показать, что нет способа раскрасить целые числа до 7825 требуемым образом. ^{[31] [32]} Малые значения чисел Шура также были вычислены Хойлом с помощью решателей SAT. ^[33]

В проверке программного обеспечения

Решатели SAT используются для формальной проверки оборудования и программного обеспечения . При проверке моделей (в частности, при проверке ограниченной модели) решатели SAT используются для проверки того, удовлетворяет ли конечная система спецификации ее предполагаемого поведения. ^[34] [ ^35]

Решатели SAT являются основным компонентом, на котором строятся решатели теорий выполнимости по модулю (SMT), которые используются для таких задач, как планирование заданий , символьное выполнение , проверка моделей программ , верификация программ на основе логики Хоара и других приложений. ^[36] Эти методы также тесно связаны с программированием в ограничениях и логическим программированием .

В других областях

В исследовании операций решатели SAT применялись для решения задач оптимизации и планирования. ^[37]

В теории общественного выбора решатели SAT использовались для доказательства теорем о невозможности. ^[38] Тан и Линь использовали решатели SAT для доказательства теоремы Эрроу и других классических теорем о невозможности. Гейст и Эндрисс использовали его для поиска новых невозможностей, связанных с расширениями множеств. Брандт и Гейст использовали этот подход для доказательства невозможности относительно стратегически защищенных турнирных решений . Другие авторы использовали эту технологию для доказательства новых невозможностей относительно парадокса неявки , половинчатой ​​монотонности и вероятностных правил голосования . Брандл, Брандт, Питерс и Стрикер использовали его для доказательства невозможности стратегически защищенного, эффективного и справедливого правила для дробного общественного выбора . ^[39]

Смотрите также

• Категория:SAT решатели
• Компьютерное доказательство
• Выполнимость по модулю теории

Ссылки

1. Охрименко, Ольга; Стаки, Питер Дж.; Кодиш, Майкл (2007), «Распространение = ленивая генерация предложений», Принципы и практика программирования ограничений – CP 2007 , Конспект лекций по информатике, т. 4741, стр. 544–558, CiteSeerX  10.1.1.70.5471 , doi :10.1007/978-3-540-74970-7_39, ISBN 978-3-540-74969-1Современные решатели SAT часто могут решать задачи с миллионами ограничений и сотнями тысяч переменных.
2. Дэвис, М.; Патнэм, Х. (1960). «Вычислительная процедура для теории квантификации». Журнал ACM . 7 (3): 201. doi :10.1145/321033.321034. S2CID  31888376.
3. Дэвис, М.; Логеманн, Г.; Лавленд, Д. (1962). «Машинная программа для доказательства теорем» (PDF) . Сообщения ACM . 5 (7): 394–397. doi :10.1145/368273.368557. hdl : 2027/mdp.39015095248095 . S2CID  15866917.
4. Чжан, Линтао; Малик, Шарад (2002), «Поиск эффективных решателей булевой выполнимости», Computer Aided Verification , Lecture Notes in Computer Science, т. 2404, Springer Berlin Heidelberg, стр. 17–36, doi : 10.1007/3-540-45657-0_2 , ISBN 978-3-540-43997-4
5. Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). «Решатели булевой выполнимости и их применение в проверке моделей». Труды IEEE . 103 (11): 2021–2035. doi :10.1109/JPROC.2015.2455034. S2CID  10190144.
6. Möhle, Sibylle; Biere, Armin (2019). "Обратный откат". Теория и применение тестирования выполнимости – SAT 2019 (PDF) . Конспект лекций по информатике. Том 11628. С. 250–266. doi :10.1007/978-3-030-24258-9_18. ISBN 978-3-030-24257-2. S2CID  195755607.
7. Moskewicz, MW; Madigan, CF; Zhao, Y.; Zhang, L.; Malik, S. (2001). "Chaff: Engineering an Efficient SAT Solver" (PDF) . Труды 38-й конференции по автоматизации проектирования (DAC) . стр. 530. doi :10.1145/378239.379017. ISBN 1581132972. S2CID  9292941.
8. Marques-Silva, JP; Sakallah, KA (1999). "GRASP: алгоритм поиска пропозициональной выполнимости" (PDF) . IEEE Transactions on Computers . 48 (5): 506. doi :10.1109/12.769433. Архивировано из оригинала (PDF) 2016-11-04 . Получено 2015-08-28 .
9. http://www.cril.univ-artois.fr/~jabbour/manysat.htm ^{[ пустой URL ]}
10. "Веб-страница международных соревнований SAT" . Получено 2007-11-15 .
11. "Конкурс SAT 2016". baldur.iti.kit.edu . Получено 2020-02-13 .
12. "Конкурс SAT 2017". baldur.iti.kit.edu . Получено 13.02.2020 .
13. "Конкурс SAT 2018". sat2018.forsyte.tuwien.ac.at . Получено 2020-02-13 .
14. Balyo, Tomáš; Sinz, Carsten (2018), «Параллельная выполнимость», Справочник по параллельным рассуждениям с ограничениями , Springer International Publishing, стр. 3–29, doi : 10.1007/978-3-319-63516-3_1, ISBN 978-3-319-63515-6
15. Бьер, Армин. «Lingeling, Plingeling, PicoSAT и PrecoSAT на SAT Race 2010» (PDF) . САТ-ГОНКА 2010 .
16. "ppfolio resolver". www.cril.univ-artois.fr . Получено 29.12.2019 .
17. "SAT 2011 Competition: 32 cores track: рейтинг решателей". www.cril.univ-artois.fr . Получено 2020-02-13 .
18. Балио, Томаш; Сандерс, Питер; Синц, Карстен (2015), «HordeSat: Массовый параллельный решатель портфеля SAT», Теория и применение тестирования выполнимости — SAT 2015 , Конспект лекций по информатике, т. 9340, Springer International Publishing, стр. 156–172, arXiv : 1505.03340 , doi : 10.1007/978-3-319-24318-4_12, ISBN 978-3-319-24317-7, S2CID  11507540
19. "Конкурс SAT 2018". sat2018.forsyte.tuwien.ac.at . Получено 2020-02-13 .
20. Heule, Marijn JH ; Kullmann, Oliver; Wieringa, Siert; Biere, Armin (2012), "Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads", Hardware and Software: Verification and Testing , Lecture Notes in Computer Science, т. 7261, Springer Berlin Heidelberg, стр. 50–65, doi :10.1007/978-3-642-34188-5_8, ISBN 978-3-642-34187-8
21. Хойле, Марин Дж. Х .; ван Маарен, Ганс (2009). «Решатели SAT на основе прогноза» (PDF) . Справочник по выполнимости . ИОС Пресс. стр. 155–184. ISBN 978-1-58603-929-5.
22. Heule, Marijn JH ; Kullmann, Oliver; Marek, Victor W. (2016), «Решение и проверка задачи булевых пифагорейских троек с помощью метода Cube-and-Conquer», Theory and Applications of Satisfiability Testing – SAT 2016 , Lecture Notes in Computer Science, т. 9710, Springer International Publishing, стр. 228–245, arXiv : 1605.00723 , doi : 10.1007/978-3-319-40970-2_15, ISBN 978-3-319-40969-6, S2CID  7912943
23. Ахмед, Танбир (2010). «Два новых числа Ван дер Вардена w(2;3,17) и w(2;3,18)». Целые числа . 10 (4): 369–377. doi :10.1515/integ.2010.032. MR  2684128. S2CID  124272560.
24. Роли, Андреа (2002), «Критичность и параллелизм в структурированных экземплярах SAT», Принципы и практика программирования в ограничениях - CP 2002 , Конспект лекций по информатике, т. 2470, Springer Berlin Heidelberg, стр. 714–719, doi :10.1007/3-540-46135-3_51, ISBN 978-3-540-44120-5
25. Арбелаес, Алехандро; Хамади, Юсеф (2011), «Улучшение параллельного локального поиска для SAT», Обучение и интеллектуальная оптимизация , Конспект лекций по информатике, т. 6683, Springer Berlin Heidelberg, стр. 46–60, doi :10.1007/978-3-642-25566-3_4, ISBN 978-3-642-25565-6, S2CID  14735849
26. Шёнинг, Уве (октябрь 1999 г.). «Вероятностный алгоритм для k-SAT и проблем удовлетворения ограничений» (PDF) . 40-й ежегодный симпозиум по основам компьютерной науки (Кат. № 99CB37039) . стр. 410–414. doi :10.1109/SFFCS.1999.814612. ISBN 0-7695-0409-4. S2CID  123177576.
27. "Улучшенный алгоритм экспоненциального времени для k-SAT", Патури, Пудлак, Сакс, Зани
28. «Более быстрые алгоритмы k-SAT с использованием biased-PPSZ», Хансен, Каплан, Замир, Цвик
29. Курил, Михал; Пол, Джером Л. (2008). «Число Ван дер Вардена $W(2,6)$ равно 1132». Экспериментальная математика . 17 (1): 53–61. дои : 10.1080/10586458.2008.10129025. ISSN  1058-6458. S2CID  1696473.
30. Курил, Михал (2012). «Вычисление числа Ван дер Вардена W (3,4) = 293». Целые числа . 12 : А46. МР  3083419.
31. Heule, Marijn JH; Kullmann, Oliver; Marek, Victor W. (2016), «Решение и проверка задачи булевых пифагорейских троек с помощью Cube-and-Conquer», Теория и применение тестирования выполнимости – SAT 2016 , Конспект лекций по информатике, т. 9710, стр. 228–245, arXiv : 1605.00723 , doi : 10.1007/978-3-319-40970-2_15, ISBN 978-3-319-40969-6, S2CID  7912943
32. Лэмб, Эвелин (01.06.2016). «Двухсоттерабайтное математическое доказательство — самое большое из когда-либо существовавших». Nature . 534 (7605): 17–18. Bibcode :2016Natur.534...17L. doi : 10.1038/nature.2016.19990 . ISSN  1476-4687. PMID  27251254. S2CID  5528978.
33. "Schur Number Five". www.cs.utexas.edu . Получено 2023-10-26 .
34. Кларк, Эдмунд; Бир, Армин; Райми, Ричард; Чжу, Юньшань (2001-07-01). «Проверка ограниченной модели с использованием решения выполнимости». Формальные методы в проектировании систем . 19 (1): 7–34. doi :10.1023/A:1011276507260. ISSN  1572-8102. S2CID  2484208.
35. Бире, Армин; Чиматти, Алессандро; Кларк, Эдмунд М.; Стрихман, Офер; Чжу, Юньшань (2003). "Bounded Model Checking" (PDF) . Advances in Computers . 58 (2003): 117–148. doi :10.1016/S0065-2458(03)58003-2. ISBN 9780120121588– через Academic Press.
36. Де Моура, Леонардо; Бьёрнер, Николай (2011-09-01). «Выполнимость по модулю теорий: введение и приложения». Сообщения ACM . 54 (9): 69–77. doi :10.1145/1995376.1995394. ISSN  0001-0782. S2CID  11621980.
37. Коэльо, Хосе; Ванхоук, Марио (16 августа 2011 г.). «Многорежимное планирование проектов с ограниченными ресурсами с использованием решателей RCPSP и SAT». Европейский журнал операционных исследований . 213 (1): 73–82. doi :10.1016/j.ejor.2011.03.019. ISSN  0377-2217.
38. Питерс, Доминик (2021). «Пропорциональность и стратегическая защищенность в выборах с несколькими победителями». arXiv : 2104.08594 [cs.GT].
39. Брандл, Флориан; Брандт, Феликс; Питерс, Доминик; Стрикер, Кристиан (18 июля 2021 г.). «Правила распределения при дихотомических предпочтениях: два из трех — это не так уж плохо». Труды 22-й конференции ACM по экономике и вычислениям . EC '21. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 158–179. doi : 10.1145/3465456.3467653. ISBN 978-1-4503-8554-1. S2CID  232109303.

Внешние ссылки

• Обзор соревнований Sat с 2002 года