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

Question

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

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

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

我的问题是第二个选项。有没有办法通过循环多次调用 SAT 求解器以找到所有解决方案？

标签： csatconjunctive-normal-form

Answer 1

您的第二个问题的答案是可以使用 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

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