使用SAT求解器打印N-Queens问题的所有解

Question

我正在做一个项目，我必须创建一个使用SAT解算器解决N个皇后问题的程序。我已经将约束转换为合取范式，现在正在为DIMACS文件编写代码。然而，我有一个问题。我打算给用户提供两个选项：

第一个选项是用户给出某些皇后的位置，然后让SAT求解器找到该特定设置的解决方案。

第二种选择是让SAT求解器打印问题的所有解决方案。例如，对于n=4，它将打印两个解决方案；对于n=5，它将打印所有10个解决方案，依此类推

我的问题是第二种选择。有没有办法通过一个循环多次调用SAT求解器来找到所有的解？

Answer 1

第二个问题的答案在Can a SAT solver be used to find all solutions?中

在http://andrew.gibiansky.com/blog/verification/writing-a-sat-solver/中概述了SAT求解器背后的算法理论(约束满足问题(弧-一致性，回溯-前瞻，ac3-算法...) https://en.wikipedia.org/wiki/Constraint_satisfaction_problem，https://en.wikipedia.org/wiki/Boolean_satisfiability_problem )，今天许多SAT求解器使用一种改进的回溯算法，DPLL算法(Davis-Putnam-Logemann-Loveland算法)

在中有一种简单的回溯方法，可以将所有解打印到N-Queens

另请参阅https://www.researchgate.net/post/What_is_the_best_SAT-solver_with_option_to_find_all_solutions_satisfied_given_CNF

Answer 2

最后，起作用的事情是对以前的解决方案的简单否定。我的意思是，我创建了一个仅当SAT求解器返回"UNSAT“时才停止的循环，每次我获得新的解时，我都会否定该解，然后将其作为新的约束存储到DIMACS文件中。然后，循环将重新启动，直到没有其他解决方案。