Распечатайте все решения задачи N-Queens с помощью SAT-решателя - PullRequest
Новая
       59

Распечатайте все решения задачи N-Queens с помощью SAT-решателя

1 голос
/ 31 марта 2020

Я делаю проект, в котором мне нужно было создать программу, которая решает проблему N королев с помощью SAT-решателя. Я уже преобразовал ограничения в конъюнктивную нормальную форму и сейчас пишу код для файла DIMACS. У меня, однако, есть вопрос. Я планировал предоставить пользователю 2 варианта:

1-й вариант - пользователь может указать позиции определенных королев, а затем с помощью решателя SAT найти решение для этой конкретной настройки c. .

Второй вариант - для решателя SAT распечатать все решения проблемы. Например, для n = 4 будет напечатано оба решения, для n = 5 для всех 10 решений и т. Д.

Мой вопрос касается второго варианта. Можно ли несколько раз вызвать SAT-решатель через al oop, чтобы найти все решения?

1 Ответ

0 голосов
/ 31 марта 2020

Ответ на ваш второй вопрос: Можно ли использовать SAT-решатель для поиска всех решений?

В http://andrew.gibiansky.com/blog/verification/writing-a-sat-solver/ - обзор алгоритмов c теория, стоящая за решателями SAT ( Проблема ограниченного удовлетворения (ar c -согласованность, возврат в прошлое - прогноз, алгоритм AC3 ...) https://en.wikipedia.org/wiki/Constraint_satisfaction_problem, https://en.wikipedia.org/wiki/Boolean_satisfiability_problem), сегодня многие решатели SAT используют улучшенный алгоритм обратного отслеживания, алгоритм DPLL (алгоритм Дэвиса-Путнама-Логемана-Лавленда)

In https://www.geeksforgeeks.org/printing-solutions-n-queen-problem/ - это простой способ возврата для печати всех решений для N-Queens

Также см. https://www.researchgate.net/post/What_is_the_best_SAT-solver_with_option_to_find_all_solutions_satisfied_given_CNF

...