Print all solutions of the N-Queens problem using a SAT solver

Question

I'm doing a project were I have to create a program who solves the N queens problem using a SAT solver. I have already transformed the constraints into conjunctive normal form and I'm now writing the code for the DIMACS file. I however have a question. I was planning to give the user 2 options:

The 1st option would be for the user to give the positions of certain queens, and then having the SAT solver find a solution to that specific set-up.

The 2nd option would be for the SAT solver to print all solutions of the problem. For example, for n=4 it would print both solutions, for n=5 all 10 solutions and so on

My question is for the 2nd option. Is there a way to call the SAT solver multiple times through a loop to find all solutions?

Answer 1

The answer to your second question is in Can a SAT solver be used to find all solutions?

In http://andrew.gibiansky.com/blog/verification/writing-a-sat-solver/ is an overview over the algorithmic theory behind SAT solvers (Constrained Satisfaction Problem (arc-consistency, backtracking - look-ahead, AC3-algorithm ...) https://en.wikipedia.org/wiki/Constraint_satisfaction_problem , https://en.wikipedia.org/wiki/Boolean_satisfiability_problem ), today many SAT solvers use an improved backtracking algortihm, the DPLL algorithm (Davis–Putnam–Logemann–Loveland algorithm)

In https://www.geeksforgeeks.org/printing-solutions-n-queen-problem/ is a plain backtracking approach to print all solutions to N-Queens

Also see https://www.researchgate.net/post/What_is_the_best_SAT-solver_with_option_to_find_all_solutions_satisfied_given_CNF

Answer 2

At the end the thing that worked, was a simple negation of the previous solution. By this I mean that I created a loop that stopped only if the SAT solver returned "UNSAT" and every time I got a new solution, I would negate that solution and then store it to the DIMACS file as a new constraint. Then the loop would restart until there are no other solutions left.