1

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?

Sotiris Kettenis
  • 51
  • 1
  • 6
  • Maybe of interest [queens puzzle with z3](https://stackoverflow.com/questions/48031462/z3-solve-the-eight-queens-puzzle/48033237) and [all solutions with z3](https://stackoverflow.com/questions/60866787/getting-all-solutions-of-a-boolean-expression-in-z3py-never-ends) -- SMT solvers like `z3` are built on top of a SAT solver so they can also be used as such -- Search for the keywords *incremental SAT solver* for your second question. – Patrick Trentin Mar 31 '20 at 13:49

2 Answers2

0

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

ralf htp
  • 9,149
  • 4
  • 22
  • 34
0

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.

Sotiris Kettenis
  • 51
  • 1
  • 6