我正在做一个项目，我必须创建一个使用 SAT 求解器解决 N 皇后问题的程序。我已经将约束转换为联合范式，现在正在编写 DIMACS 文件的代码。然而，我有一个问题。我打算给用户 2 个选项：
第一个选项是让用户给出某些皇后的位置，然后让 SAT 求解器找到该特定设置的解决方案。
第二个选项是 SAT 求解器打印问题的所有解决方案。例如，对于 n=4，它将打印两个解决方案，对于 n=5，所有 10 个解决方案，依此类推
我的问题是第二个选项。有没有办法通过循环多次调用 SAT 求解器以找到所有解决方案？
您的第二个问题的答案是可以使用 SAT 求解器来查找所有解决方案吗？
在http://andrew.gibiansky.com/blog/verification/writing-a-sat-solver/中概述了 SAT 求解器背后的算法理论（约束满足问题 （arc-consistency, backtracking - look-ahead, AC3-算法 ...）https://en.wikipedia.org/wiki/Constraint_satisfaction_problem，https://en.wikipedia.org/wiki/Boolean_satisfiability_problem ） ，今天许多SAT求解器使用改进的回溯算法，DPLL算法（Davis– Putnam-Logemann-Loveland 算法）
在https://www.geeksforgeeks.org/printing-solutions-n-queen-problem/中是一种简单的回溯方法，可以将所有解决方案打印到N-Queens
最后，有效的方法是对先前解决方案的简单否定。我的意思是我创建了一个循环，该循环仅在 SAT 求解器返回“UNSAT”时停止，并且每次我得到一个新的解决方案时，我都会否定该解决方案，然后将其作为新约束存储到 DIMACS 文件中。然后循环将重新开始，直到没有其他解决方案。