Minisat — это инструмент программирования/удовлетворения ограничений. Существует версия Minisat, которая работает в браузере http://www.msoos.org/2013/09/minisat-in-your-browser/ Как я могу выразить проблему планирования с Minisat? Есть ли язык...

Я придумал алгоритм решения проблемы 3SAT с помощью следующего подхода: 1) Возьмите все предложения в уравнении cnf, которые имеют хотя бы одну общую переменную. Найдите все такие комбинации и поместите их в список под названием «Пересечение»....

Я совершенно новичок в решателе sat4j и исследую логические выполнимые задачи; и я застрял. Я хочу сделать программу, которая решает целые переменные, которые находятся в логической формуле, например; x1 ‹ x2 + x3 пользователь вводит эту формулу,...

Для проекта, который я начинаю, мне понадобится решатель SAT. Я использовал некоторые из них раньше, но в основном для экспериментов, а здесь основным ограничением для проекта является хорошая производительность. Я пытаюсь искать альтернативы и...

Я использую привязки Python для программы доказательства теорем Z3 (Z3Py). У меня есть N логических переменных, x1, .., xN. Я хочу выразить ограничение, согласно которому ровно K из N из них должны быть истинными. Как я могу это сделать в Z3Py?...

SAT BASED MOTION PLANNING ALGORITHM Простую задачу планирования движения можно преобразовать в задачу решения SAT . Кто-нибудь может объяснить, как это возможно? В этой задаче мы должны найти путь без столкновений от...

Я только что узнал о DPLL(T) и алгоритм DPLL по отношению к решателям SMT. Я видел ссылки на z3 в нескольких местах, касающихся решателей SMT. Интересно, что z3 использует для своих алгоритмов на высоком уровне для реализации решения SMT....

У меня есть школьный проект, где я должен найти решения игры "Lights Out" ( https://en.wikipedia.org/wiki/Lights_Out_(game) ) с помощью SAT Solver, но у меня возникают проблемы при попытке установить конъюнктивную нормальную форму игры. Игра...

Я хотел бы спросить, можно ли получить доступ к исходному коду C ++ для программы main (). Я просмотрел каталоги и не нашел. Причина в том, что я хотел бы отследить код, чтобы увидеть, как SCIP обрабатывает проблемы SAT, и, возможно, изменить код,...

k-SAT — это частный случай SAT. Поскольку SAT является NP-полным, я не понимаю, почему у нас нет k-SAT, являющегося NP-полным для любых значений k. На занятии мой профессор использовал полиномиальную редукцию из SAT, чтобы доказать, что 3-SAT...

Мои проблемы - большие проблемы с SAT. В SCIP7.0.0 есть множество правил ветвления на выбор. Если я отправлю проблему в SCIP, и SCIP решит ее, можно ли использовать полученную информацию в процессе решения, например, плоскости резки, ограничения...

Меня интересует подсчет количества решений проблемы (не перечисление решений). Для этого у меня есть инструменты, использующие файлы CNF . Я хочу преобразовать файлы Minizinc (формат mzn или Flatzinc fzn) и преобразовать их в CNF. Я узнал, что...