Nas seções a seguir, vamos ilustrar a programação de restrições (CP) um problema combinatório baseado no jogo de xadrez. No xadrez, uma rainha pode atacar horizontal, vertical e diagonalmente. O problema do N-queens pergunta:
Como N rainhas podem ser colocadas em um tabuleiro de xadrez NxN para que duas não ataquem uns aos outros?
Abaixo, é mostrada uma possível solução para o problema das N-queens para N = 4.
Não há duas rainhas na mesma linha, coluna ou diagonal.
Esse não é um problema de otimização: queremos encontrar todas as opções em vez de uma solução ideal, o que a torna um candidato natural programação restrita. As seções a seguir descrevem a abordagem do PC para o problema do N-queens e apresenta programas que o resolvem usando tanto o solucionador CP-SAT quanto o CP original solucionador.
Abordagem CP para o problema das N-queens
Um solucionador de CP funciona tentando sistematicamente possíveis atribuições de valores às variáveis em um problema, para encontrar a soluções viáveis. No problema das 4 queens, o solucionador começa na extremidade esquerda coluna e sucessivamente coloca uma rainha em cada coluna, em um local que é não foram atacados por rainhas colocadas anteriormente.
Propagação e retrocesso
Há dois elementos principais em uma pesquisa de programação restrita:
- Propagação: sempre que o solucionador atribui um valor a uma variável, a restrições adicionam restrições aos possíveis valores do atributo não atribuído variáveis. Essas restrições se propagam para futuras atribuições de variáveis. Por exemplo, no problema das quatro rainhas, cada vez que o solucionador coloca uma rainha, ela não pode colocar outras rainhas na linha e diagonais em que a rainha atual está. A propagação pode acelerar a pesquisa significativamente, reduzindo o conjunto de de variáveis que o solucionador precisa explorar.
- O backtracking ocorre quando o solucionador não consegue atribuir um valor ao próximo variável, devido às restrições, ou encontra uma solução. Em ambos os casos, o solucionador retorna ao estágio anterior e altera o valor da variável para um valor que ainda não foi testado. No exemplo das 4 queens, isso significa mover uma rainha para um novo quadrado na coluna atual.
A seguir, você vai ver como a programação de restrições usa propagação e retrocesso para resolver o problema das quatro queens.
Vamos supor que o solucionador começa colocando uma rainha no canto superior esquerdo arbitrariamente direito. Isso é uma espécie de hipótese; talvez descubra que nenhuma solução com uma rainha no canto superior esquerdo.
Dada essa hipótese, quais restrições podemos propagar? Uma restrição é que pode haver apenas uma rainha em uma coluna (os Xs cinza abaixo) e outra restrição proíbe duas rainhas na mesma diagonal (os X vermelhos abaixo).
Nossa terceira restrição proíbe rainhas na mesma fileira:
Nossas restrições se propagaram, podemos testar outra hipótese e colocar segunda rainha em um dos quadrados restantes disponíveis. Nosso solucionador pode decidir para colocar nele o primeiro quadrado disponível na segunda coluna:
Depois de propagar a restrição diagonal, vemos que ela não deixa quadrados disponíveis na terceira coluna ou na última linha:
Sem soluções possíveis nesta fase, precisamos recuar. Uma opção é para o solucionador escolher o outro quadrado disponível na segunda coluna. No entanto, a propagação de restrição força uma rainha a entrar na segunda linha do terceira coluna, não deixando espaços válidos para a quarta rainha:
Assim, o solucionador precisa voltar de novo, desta vez de volta posicionamento da primeira rainha. Já mostramos que nenhuma solução para as rainhas problema ocupará um quadrado de canto.
Como não pode haver rainha no canto, o solucionador move a primeira rainha para baixo por um e se propaga, deixando apenas um lugar para a segunda rainha:
A propagação novamente revela apenas um lugar restante para a terceira rainha:
E para a quarta e última rainha:
Nós já temos nossa primeira solução. Se instruíssemos nosso solucionador a parar depois de encontrar a primeira solução, ele terminaria aqui. Caso contrário, ele recuaria de novo colocar a primeira rainha na terceira linha da primeira coluna.
Solução que usa CP-SAT
O problema das N-queens é ideal para a programação restrita. Neste abordaremos um pequeno programa em Python que usa o solucionador CP-SAT para encontrar todas as soluções para o problema.
Importar as bibliotecas
O código a seguir importa a biblioteca necessária.
Python
import sys import time from ortools.sat.python import cp_model
C++
#include <stdlib.h> #include <sstream> #include <string> #include <vector> #include "absl/strings/numbers.h" #include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/sorted_interval_list.h"
Java
import com.google.ortools.Loader; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.CpSolverSolutionCallback; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.LinearExpr;
C#
using System; using Google.OrTools.Sat;
Declarar o modelo
O código a seguir declara o modelo CP-SAT.
Python
model = cp_model.CpModel()
C++
CpModelBuilder cp_model;
Java
CpModel model = new CpModel();
C#
CpModel model = new CpModel(); int BoardSize = 8; // There are `BoardSize` number of variables, one for a queen in each // column of the board. The value of each variable is the row that the // queen is in. IntVar[] queens = new IntVar[BoardSize]; for (int i = 0; i < BoardSize; ++i) { queens[i] = model.NewIntVar(0, BoardSize - 1, $"x{i}"); } // Define constraints. // All rows must be different. model.AddAllDifferent(queens); // No two queens can be on the same diagonal. LinearExpr[] diag1 = new LinearExpr[BoardSize]; LinearExpr[] diag2 = new LinearExpr[BoardSize]; for (int i = 0; i < BoardSize; ++i) { diag1[i] = LinearExpr.Affine(queens[i], /*coeff=*/1, /*offset=*/i); diag2[i] = LinearExpr.Affine(queens[i], /*coeff=*/1, /*offset=*/-i); } model.AddAllDifferent(diag1); model.AddAllDifferent(diag2); // Creates a solver and solves the model. CpSolver solver = new CpSolver(); SolutionPrinter cb = new SolutionPrinter(queens); // Search for all solutions. solver.StringParameters = "enumerate_all_solutions:true"; // And solve. solver.Solve(model, cb); Console.WriteLine("Statistics"); Console.WriteLine($" conflicts : {solver.NumConflicts()}"); Console.WriteLine($" branches : {solver.NumBranches()}"); Console.WriteLine($" wall time : {solver.WallTime()} s"); Console.WriteLine($" number of solutions found: {cb.SolutionCount()}"); } }
Criar as variáveis
O solucionador cria as variáveis para o problema como uma matriz chamada queens
.
Python
# There are `board_size` number of variables, one for a queen in each column # of the board. The value of each variable is the row that the queen is in. queens = [model.new_int_var(0, board_size - 1, f"x_{i}") for i in range(board_size)]
C++
// There are `board_size` number of variables, one for a queen in each column // of the board. The value of each variable is the row that the queen is in. std::vector<IntVar> queens; queens.reserve(board_size); Domain range(0, board_size - 1); for (int i = 0; i < board_size; ++i) { queens.push_back( cp_model.NewIntVar(range).WithName("x" + std::to_string(i))); }
Java
int boardSize = 8; // There are `BoardSize` number of variables, one for a queen in each column of the board. The // value of each variable is the row that the queen is in. IntVar[] queens = new IntVar[boardSize]; for (int i = 0; i < boardSize; ++i) { queens[i] = model.newIntVar(0, boardSize - 1, "x" + i); }
C#
int BoardSize = 8; // There are `BoardSize` number of variables, one for a queen in each // column of the board. The value of each variable is the row that the // queen is in. IntVar[] queens = new IntVar[BoardSize]; for (int i = 0; i < BoardSize; ++i) { queens[i] = model.NewIntVar(0, BoardSize - 1, $"x{i}"); }
Aqui, presumimos que queens[j]
é o número da linha da rainha na coluna j
.
Em outras palavras, queens[j] = i
significa que há uma rainha na linha i
e na coluna j
.
Criar as restrições
Aqui está o código que cria as restrições para o problema.
Python
# All rows must be different. model.add_all_different(queens) # No two queens can be on the same diagonal. model.add_all_different(queens[i] + i for i in range(board_size)) model.add_all_different(queens[i] - i for i in range(board_size))
C++
// The following sets the constraint that all queens are in different rows. cp_model.AddAllDifferent(queens); // No two queens can be on the same diagonal. std::vector<LinearExpr> diag_1; diag_1.reserve(board_size); std::vector<LinearExpr> diag_2; diag_2.reserve(board_size); for (int i = 0; i < board_size; ++i) { diag_1.push_back(queens[i] + i); diag_2.push_back(queens[i] - i); } cp_model.AddAllDifferent(diag_1); cp_model.AddAllDifferent(diag_2);
Java
// All rows must be different. model.addAllDifferent(queens); // No two queens can be on the same diagonal. LinearExpr[] diag1 = new LinearExpr[boardSize]; LinearExpr[] diag2 = new LinearExpr[boardSize]; for (int i = 0; i < boardSize; ++i) { diag1[i] = LinearExpr.newBuilder().add(queens[i]).add(i).build(); diag2[i] = LinearExpr.newBuilder().add(queens[i]).add(-i).build(); } model.addAllDifferent(diag1); model.addAllDifferent(diag2);
C#
// All rows must be different. model.AddAllDifferent(queens); // No two queens can be on the same diagonal. LinearExpr[] diag1 = new LinearExpr[BoardSize]; LinearExpr[] diag2 = new LinearExpr[BoardSize]; for (int i = 0; i < BoardSize; ++i) { diag1[i] = LinearExpr.Affine(queens[i], /*coeff=*/1, /*offset=*/i); diag2[i] = LinearExpr.Affine(queens[i], /*coeff=*/1, /*offset=*/-i); } model.AddAllDifferent(diag1); model.AddAllDifferent(diag2);
O código usa o método AddAllDifferent
, que requer todos os elementos de uma
matriz de variáveis seja diferente.
Vamos ver como essas restrições garantem as três condições para as N-queens problema (queens em diferentes linhas, colunas e diagonais).
Não há duas rainhas na mesma fileira
Aplicar o método AllDifferent
do solucionador a queens
força os valores de
queens[j]
sejam diferentes para cada j
, o que significa que todas as rainhas precisam estar em
linhas diferentes.
Não há duas rainhas na mesma coluna
Essa restrição está implícita na definição de queens
.
Como dois elementos de queens
não podem ter o mesmo índice, duas queens não podem ser
na mesma coluna.
Não há duas rainhas na mesma diagonal
A restrição diagonal é um pouco mais complicada do que as de linha e coluna. Primeiro, se duas rainhas estão na mesma diagonal, uma das condições abaixo precisa ser verdadeiro:
- O número da linha mais o número da coluna de cada uma das duas rainhas são iguais.
Em outras palavras,
queens(j) + j
tem o mesmo valor para dois índices diferentesj
. - O número da linha menos o número da coluna de cada uma das duas queens são iguais.
Nesse caso,
queens(j) - j
tem o mesmo valor para dois índicesj
diferentes.
Uma dessas condições significa que as rainhas estão na mesma diagonal crescente ( indo da esquerda para a direita), enquanto o outro significa que elas estão na mesma ordem decrescente na diagonal. Qual condição corresponde à ordem crescente e à decrescente depende de como você ordena as linhas e colunas. Como mencionado no seção anterior, a ordem não terá efeito sobre o conjunto de soluções, apenas no modo como elas são visualizadas.
Portanto, a restrição diagonal é que os valores de queens(j) + j
precisam ser todos
diferentes, e os valores de queens(j) - j
devem ser todos diferentes, para
j
diferente.
Para aplicar o método AddAllDifferent
a queens(j) + j
, colocamos as instâncias N
da variável, para j
de 0
a N-1
, em uma matriz, diag1
, da seguinte maneira:
q1 = model.NewIntVar(0, 2 * board_size, 'diag1_%i' % i) diag1.append(q1) model.Add(q1 == queens[j] + j)
Em seguida, aplicamos AddAllDifferent
a diag1
.
model.AddAllDifferent(diag1)
A restrição para queens(j) - j
é criada de forma semelhante.
Criar uma impressora de solução
Para imprimir todas as soluções do problema do N-queens, você precisa transmitir um callback, chamada de impressora de solução, para o solucionador CP-SAT. O callback imprime cada nova solução à medida que o solucionador a encontra. O código a seguir cria uma solução impressora
Python
class NQueenSolutionPrinter(cp_model.CpSolverSolutionCallback): """Print intermediate solutions.""" def __init__(self, queens: list[cp_model.IntVar]): cp_model.CpSolverSolutionCallback.__init__(self) self.__queens = queens self.__solution_count = 0 self.__start_time = time.time() @property def solution_count(self) -> int: return self.__solution_count def on_solution_callback(self): current_time = time.time() print( f"Solution {self.__solution_count}, " f"time = {current_time - self.__start_time} s" ) self.__solution_count += 1 all_queens = range(len(self.__queens)) for i in all_queens: for j in all_queens: if self.value(self.__queens[j]) == i: # There is a queen in column j, row i. print("Q", end=" ") else: print("_", end=" ") print() print()
C++
int num_solutions = 0; Model model; model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& response) { LOG(INFO) << "Solution " << num_solutions; for (int i = 0; i < board_size; ++i) { std::stringstream ss; for (int j = 0; j < board_size; ++j) { if (SolutionIntegerValue(response, queens[j]) == i) { // There is a queen in column j, row i. ss << "Q"; } else { ss << "_"; } if (j != board_size - 1) ss << " "; } LOG(INFO) << ss.str(); } num_solutions++; }));
Java
static class SolutionPrinter extends CpSolverSolutionCallback { public SolutionPrinter(IntVar[] queensIn) { solutionCount = 0; queens = queensIn; } @Override public void onSolutionCallback() { System.out.println("Solution " + solutionCount); for (int i = 0; i < queens.length; ++i) { for (int j = 0; j < queens.length; ++j) { if (value(queens[j]) == i) { System.out.print("Q"); } else { System.out.print("_"); } if (j != queens.length - 1) { System.out.print(" "); } } System.out.println(); } solutionCount++; } public int getSolutionCount() { return solutionCount; } private int solutionCount; private final IntVar[] queens; }
C#
public class SolutionPrinter : CpSolverSolutionCallback { public SolutionPrinter(IntVar[] queens) { queens_ = queens; } public override void OnSolutionCallback() { Console.WriteLine($"Solution {SolutionCount_}"); for (int i = 0; i < queens_.Length; ++i) { for (int j = 0; j < queens_.Length; ++j) { if (Value(queens_[j]) == i) { Console.Write("Q"); } else { Console.Write("_"); } if (j != queens_.Length - 1) Console.Write(" "); } Console.WriteLine(""); } SolutionCount_++; } public int SolutionCount() { return SolutionCount_; } private int SolutionCount_; private IntVar[] queens_; }
A impressora da solução precisa ser escrita como uma classe Python, devido ao Interface Python para o solucionador C++.
As soluções são impressas pelas seguintes linhas na impressora da solução.
for v in self.__variables: print('%s = %i' % (v, self.Value(v)), end = ' ')
Neste exemplo, self.__variables
é a variável queens
, e cada v
corresponde a uma das oito entradas de queens
. Isso gera uma solução
o seguinte formato: x0 = queens(0) x1 = queens(1) ... x7 = queens(7)
, em que
xi
é o número da coluna da rainha na linha i
.
A próxima seção mostra um exemplo de solução.
Chamar o solucionador e exibir os resultados
O código a seguir executa o solucionador e exibe as soluções.
Python
solver = cp_model.CpSolver() solution_printer = NQueenSolutionPrinter(queens) solver.parameters.enumerate_all_solutions = True solver.solve(model, solution_printer)
C++
// Tell the solver to enumerate all solutions. SatParameters parameters; parameters.set_enumerate_all_solutions(true); model.Add(NewSatParameters(parameters)); const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model); LOG(INFO) << "Number of solutions found: " << num_solutions;
Java
CpSolver solver = new CpSolver(); SolutionPrinter cb = new SolutionPrinter(queens); // Tell the solver to enumerate all solutions. solver.getParameters().setEnumerateAllSolutions(true); // And solve. solver.solve(model, cb);
C#
// Creates a solver and solves the model. CpSolver solver = new CpSolver(); SolutionPrinter cb = new SolutionPrinter(queens); // Search for all solutions. solver.StringParameters = "enumerate_all_solutions:true"; // And solve. solver.Solve(model, cb);
O programa encontra 92 soluções diferentes para um quadro 8x8. Lá vai a primeira pergunta.
Q _ _ _ _ _ _ _ _ _ _ _ _ _ Q _ _ _ _ _ Q _ _ _ _ _ _ _ _ _ _ Q _ Q _ _ _ _ _ _ _ _ _ Q _ _ _ _ _ _ _ _ _ Q _ _ _ _ Q _ _ _ _ _ ...91 other solutions displayed... Solutions found: 92
Você pode resolver o problema de uma placa de tamanho diferente passando N como um
argumento de linha de comando. Por exemplo, se o nome do programa for queens
,
python nqueens_sat.py 6
resolve o problema de uma placa 6x6.
Todo o programa
Aqui está o programa completo do N-queens.
Python
"""OR-Tools solution to the N-queens problem.""" import sys import time from ortools.sat.python import cp_model class NQueenSolutionPrinter(cp_model.CpSolverSolutionCallback): """Print intermediate solutions.""" def __init__(self, queens: list[cp_model.IntVar]): cp_model.CpSolverSolutionCallback.__init__(self) self.__queens = queens self.__solution_count = 0 self.__start_time = time.time() @property def solution_count(self) -> int: return self.__solution_count def on_solution_callback(self): current_time = time.time() print( f"Solution {self.__solution_count}, " f"time = {current_time - self.__start_time} s" ) self.__solution_count += 1 all_queens = range(len(self.__queens)) for i in all_queens: for j in all_queens: if self.value(self.__queens[j]) == i: # There is a queen in column j, row i. print("Q", end=" ") else: print("_", end=" ") print() print() def main(board_size: int) -> None: # Creates the solver. model = cp_model.CpModel() # Creates the variables. # There are `board_size` number of variables, one for a queen in each column # of the board. The value of each variable is the row that the queen is in. queens = [model.new_int_var(0, board_size - 1, f"x_{i}") for i in range(board_size)] # Creates the constraints. # All rows must be different. model.add_all_different(queens) # No two queens can be on the same diagonal. model.add_all_different(queens[i] + i for i in range(board_size)) model.add_all_different(queens[i] - i for i in range(board_size)) # Solve the model. solver = cp_model.CpSolver() solution_printer = NQueenSolutionPrinter(queens) solver.parameters.enumerate_all_solutions = True solver.solve(model, solution_printer) # Statistics. print("\nStatistics") print(f" conflicts : {solver.num_conflicts}") print(f" branches : {solver.num_branches}") print(f" wall time : {solver.wall_time} s") print(f" solutions found: {solution_printer.solution_count}") if __name__ == "__main__": # By default, solve the 8x8 problem. size = 8 if len(sys.argv) > 1: size = int(sys.argv[1]) main(size)
C++
// OR-Tools solution to the N-queens problem. #include <stdlib.h> #include <sstream> #include <string> #include <vector> #include "absl/strings/numbers.h" #include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { void NQueensSat(const int board_size) { // Instantiate the solver. CpModelBuilder cp_model; // There are `board_size` number of variables, one for a queen in each column // of the board. The value of each variable is the row that the queen is in. std::vector<IntVar> queens; queens.reserve(board_size); Domain range(0, board_size - 1); for (int i = 0; i < board_size; ++i) { queens.push_back( cp_model.NewIntVar(range).WithName("x" + std::to_string(i))); } // Define constraints. // The following sets the constraint that all queens are in different rows. cp_model.AddAllDifferent(queens); // No two queens can be on the same diagonal. std::vector<LinearExpr> diag_1; diag_1.reserve(board_size); std::vector<LinearExpr> diag_2; diag_2.reserve(board_size); for (int i = 0; i < board_size; ++i) { diag_1.push_back(queens[i] + i); diag_2.push_back(queens[i] - i); } cp_model.AddAllDifferent(diag_1); cp_model.AddAllDifferent(diag_2); int num_solutions = 0; Model model; model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& response) { LOG(INFO) << "Solution " << num_solutions; for (int i = 0; i < board_size; ++i) { std::stringstream ss; for (int j = 0; j < board_size; ++j) { if (SolutionIntegerValue(response, queens[j]) == i) { // There is a queen in column j, row i. ss << "Q"; } else { ss << "_"; } if (j != board_size - 1) ss << " "; } LOG(INFO) << ss.str(); } num_solutions++; })); // Tell the solver to enumerate all solutions. SatParameters parameters; parameters.set_enumerate_all_solutions(true); model.Add(NewSatParameters(parameters)); const CpSolverResponse response = SolveCpModel(cp_model.Build(), &model); LOG(INFO) << "Number of solutions found: " << num_solutions; // Statistics. LOG(INFO) << "Statistics"; LOG(INFO) << CpSolverResponseStats(response); } } // namespace sat } // namespace operations_research int main(int argc, char** argv) { int board_size = 8; if (argc > 1) { if (!absl::SimpleAtoi(argv[1], &board_size)) { LOG(INFO) << "Cannot parse '" << argv[1] << "', using the default value of 8."; board_size = 8; } } operations_research::sat::NQueensSat(board_size); return EXIT_SUCCESS; }
Java
package com.google.ortools.sat.samples; import com.google.ortools.Loader; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; import com.google.ortools.sat.CpSolverSolutionCallback; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.LinearExpr; /** OR-Tools solution to the N-queens problem. */ public final class NQueensSat { static class SolutionPrinter extends CpSolverSolutionCallback { public SolutionPrinter(IntVar[] queensIn) { solutionCount = 0; queens = queensIn; } @Override public void onSolutionCallback() { System.out.println("Solution " + solutionCount); for (int i = 0; i < queens.length; ++i) { for (int j = 0; j < queens.length; ++j) { if (value(queens[j]) == i) { System.out.print("Q"); } else { System.out.print("_"); } if (j != queens.length - 1) { System.out.print(" "); } } System.out.println(); } solutionCount++; } public int getSolutionCount() { return solutionCount; } private int solutionCount; private final IntVar[] queens; } public static void main(String[] args) { Loader.loadNativeLibraries(); // Create the model. CpModel model = new CpModel(); int boardSize = 8; // There are `BoardSize` number of variables, one for a queen in each column of the board. The // value of each variable is the row that the queen is in. IntVar[] queens = new IntVar[boardSize]; for (int i = 0; i < boardSize; ++i) { queens[i] = model.newIntVar(0, boardSize - 1, "x" + i); } // Define constraints. // All rows must be different. model.addAllDifferent(queens); // No two queens can be on the same diagonal. LinearExpr[] diag1 = new LinearExpr[boardSize]; LinearExpr[] diag2 = new LinearExpr[boardSize]; for (int i = 0; i < boardSize; ++i) { diag1[i] = LinearExpr.newBuilder().add(queens[i]).add(i).build(); diag2[i] = LinearExpr.newBuilder().add(queens[i]).add(-i).build(); } model.addAllDifferent(diag1); model.addAllDifferent(diag2); // Create a solver and solve the model. CpSolver solver = new CpSolver(); SolutionPrinter cb = new SolutionPrinter(queens); // Tell the solver to enumerate all solutions. solver.getParameters().setEnumerateAllSolutions(true); // And solve. solver.solve(model, cb); // Statistics. System.out.println("Statistics"); System.out.println(" conflicts : " + solver.numConflicts()); System.out.println(" branches : " + solver.numBranches()); System.out.println(" wall time : " + solver.wallTime() + " s"); System.out.println(" solutions : " + cb.getSolutionCount()); } private NQueensSat() {} }
C#
// OR-Tools solution to the N-queens problem. using System; using Google.OrTools.Sat; public class NQueensSat { public class SolutionPrinter : CpSolverSolutionCallback { public SolutionPrinter(IntVar[] queens) { queens_ = queens; } public override void OnSolutionCallback() { Console.WriteLine($"Solution {SolutionCount_}"); for (int i = 0; i < queens_.Length; ++i) { for (int j = 0; j < queens_.Length; ++j) { if (Value(queens_[j]) == i) { Console.Write("Q"); } else { Console.Write("_"); } if (j != queens_.Length - 1) Console.Write(" "); } Console.WriteLine(""); } SolutionCount_++; } public int SolutionCount() { return SolutionCount_; } private int SolutionCount_; private IntVar[] queens_; } static void Main() { // Constraint programming engine CpModel model = new CpModel(); int BoardSize = 8; // There are `BoardSize` number of variables, one for a queen in each // column of the board. The value of each variable is the row that the // queen is in. IntVar[] queens = new IntVar[BoardSize]; for (int i = 0; i < BoardSize; ++i) { queens[i] = model.NewIntVar(0, BoardSize - 1, $"x{i}"); } // Define constraints. // All rows must be different. model.AddAllDifferent(queens); // No two queens can be on the same diagonal. LinearExpr[] diag1 = new LinearExpr[BoardSize]; LinearExpr[] diag2 = new LinearExpr[BoardSize]; for (int i = 0; i < BoardSize; ++i) { diag1[i] = LinearExpr.Affine(queens[i], /*coeff=*/1, /*offset=*/i); diag2[i] = LinearExpr.Affine(queens[i], /*coeff=*/1, /*offset=*/-i); } model.AddAllDifferent(diag1); model.AddAllDifferent(diag2); // Creates a solver and solves the model. CpSolver solver = new CpSolver(); SolutionPrinter cb = new SolutionPrinter(queens); // Search for all solutions. solver.StringParameters = "enumerate_all_solutions:true"; // And solve. solver.Solve(model, cb); Console.WriteLine("Statistics"); Console.WriteLine($" conflicts : {solver.NumConflicts()}"); Console.WriteLine($" branches : {solver.NumBranches()}"); Console.WriteLine($" wall time : {solver.WallTime()} s"); Console.WriteLine($" number of solutions found: {cb.SolutionCount()}"); } }
Solução usando o solucionador de CP original
As seções a seguir apresentam um programa em Python que resolve N-queens usando a solucionador de CP original. No entanto, recomendamos usar o solucionador de problemas CP-SAT mais recente.
Importar as bibliotecas
O código a seguir importa a biblioteca necessária.
Python
import sys from ortools.constraint_solver import pywrapcp
C++
#include <cstdint> #include <cstdlib> #include <sstream> #include <vector> #include "ortools/base/logging.h" #include "ortools/constraint_solver/constraint_solver.h"
Java
import com.google.ortools.Loader; import com.google.ortools.constraintsolver.DecisionBuilder; import com.google.ortools.constraintsolver.IntVar; import com.google.ortools.constraintsolver.Solver;
C#
using System; using Google.OrTools.ConstraintSolver;
Declarar o solucionador
O código a seguir declara o solucionador de CP original.
Python
solver = pywrapcp.Solver("n-queens")
C++
Solver solver("N-Queens");
Java
Solver solver = new Solver("N-Queens");
C#
Solver solver = new Solver("N-Queens");
Criar as variáveis
O método IntVar
do solucionador cria as variáveis para o problema como uma matriz
chamado queens
.
Python
# The array index is the column, and the value is the row. queens = [solver.IntVar(0, board_size - 1, f"x{i}") for i in range(board_size)]
C++
std::vector<IntVar*> queens; queens.reserve(board_size); for (int i = 0; i < board_size; ++i) { queens.push_back( solver.MakeIntVar(0, board_size - 1, absl::StrCat("x", i))); }
Java
int boardSize = 8; IntVar[] queens = new IntVar[boardSize]; for (int i = 0; i < boardSize; ++i) { queens[i] = solver.makeIntVar(0, boardSize - 1, "x" + i); }
C#
const int BoardSize = 8; IntVar[] queens = new IntVar[BoardSize]; for (int i = 0; i < BoardSize; ++i) { queens[i] = solver.MakeIntVar(0, BoardSize - 1, $"x{i}"); }
Em qualquer solução, queens[j] = i
significa que há uma rainha na linha e na coluna j
.
i
Criar as restrições
Aqui está o código que cria as restrições para o problema.
Python
# All rows must be different. solver.Add(solver.AllDifferent(queens)) # No two queens can be on the same diagonal. solver.Add(solver.AllDifferent([queens[i] + i for i in range(board_size)])) solver.Add(solver.AllDifferent([queens[i] - i for i in range(board_size)]))
C++
// The following sets the constraint that all queens are in different rows. solver.AddConstraint(solver.MakeAllDifferent(queens)); // All columns must be different because the indices of queens are all // different. No two queens can be on the same diagonal. std::vector<IntVar*> diag_1; diag_1.reserve(board_size); std::vector<IntVar*> diag_2; diag_2.reserve(board_size); for (int i = 0; i < board_size; ++i) { diag_1.push_back(solver.MakeSum(queens[i], i)->Var()); diag_2.push_back(solver.MakeSum(queens[i], -i)->Var()); } solver.AddConstraint(solver.MakeAllDifferent(diag_1)); solver.AddConstraint(solver.MakeAllDifferent(diag_2));
Java
// All rows must be different. solver.addConstraint(solver.makeAllDifferent(queens)); // All columns must be different because the indices of queens are all different. // No two queens can be on the same diagonal. IntVar[] diag1 = new IntVar[boardSize]; IntVar[] diag2 = new IntVar[boardSize]; for (int i = 0; i < boardSize; ++i) { diag1[i] = solver.makeSum(queens[i], i).var(); diag2[i] = solver.makeSum(queens[i], -i).var(); } solver.addConstraint(solver.makeAllDifferent(diag1)); solver.addConstraint(solver.makeAllDifferent(diag2));
C#
// All rows must be different. solver.Add(queens.AllDifferent()); // All columns must be different because the indices of queens are all different. // No two queens can be on the same diagonal. IntVar[] diag1 = new IntVar[BoardSize]; IntVar[] diag2 = new IntVar[BoardSize]; for (int i = 0; i < BoardSize; ++i) { diag1[i] = solver.MakeSum(queens[i], i).Var(); diag2[i] = solver.MakeSum(queens[i], -i).Var(); } solver.Add(diag1.AllDifferent()); solver.Add(diag2.AllDifferent());
Essas restrições garantem as três condições para o problema das N-queens ( rainhas em diferentes linhas, colunas e diagonais).
Não há duas rainhas na mesma fileira
Aplicar o método AllDifferent
do solucionador a queens
força os valores de
queens[j]
sejam diferentes para cada j
, o que significa que todas as rainhas precisam estar em
linhas diferentes.
Não há duas rainhas na mesma coluna
Essa restrição está implícita na definição de queens
.
Como dois elementos de queens
não podem ter o mesmo índice, duas queens não podem ser
na mesma coluna.
Não há duas rainhas na mesma diagonal
A restrição diagonal é um pouco mais complicada do que as de linha e coluna. Primeiro, se duas rainhas estiverem na mesma diagonal, uma das seguintes condições deve ser verdadeira:
- Se a diagonal for decrescente (da esquerda para a direita), o número da linha mais
número de coluna para cada uma das duas rainhas são iguais. Portanto,
queens(i) + i
tem mesmo valor para dois índicesi
diferentes. - Se a diagonal for crescente, o número da linha menos o número da coluna de cada
das duas rainhas são iguais. Neste caso,
queens(i) - i
tem o mesmo valor. para dois índices diferentesi
.
Portanto, a restrição diagonal é que os valores de queens(i) + i
precisam ser todos
diferentes, e da mesma forma os valores de queens(i) - i
devem ser todos diferentes, para
i
diferente.
O código acima adiciona essa restrição aplicando a
AllDifferent
como queens[j] + j
e queens[j] - j
para cada i
.
Adicionar o criador de decisões
A próxima etapa é criar um criador de decisões, que define a estratégia de pesquisa. para o problema. A estratégia de pesquisa pode ter um grande impacto no tempo de pesquisa, devido à propagação de restrições, o que reduz o número de valores variáveis que o solucionador precisa explorar. Você já viu um exemplo disso na exemplo do 4-queens.
O código a seguir cria um criador de decisões usando o
Phase
.
Python
db = solver.Phase(queens, solver.CHOOSE_FIRST_UNBOUND, solver.ASSIGN_MIN_VALUE)
C++
DecisionBuilder* const db = solver.MakePhase( queens, Solver::CHOOSE_FIRST_UNBOUND, Solver::ASSIGN_MIN_VALUE);
Java
// Create the decision builder to search for solutions. final DecisionBuilder db = solver.makePhase(queens, Solver.CHOOSE_FIRST_UNBOUND, Solver.ASSIGN_MIN_VALUE);
C#
// Create the decision builder to search for solutions. DecisionBuilder db = solver.MakePhase(queens, Solver.CHOOSE_FIRST_UNBOUND, Solver.ASSIGN_MIN_VALUE);
Consulte Criador de decisões para mais detalhes
argumentos de entrada para o método Phase
.
Como o criador de decisões funciona no exemplo das 4 queens
Vamos conferir como o criador de decisões direciona a pesquisa na
exemplo do 4-queens.
O solucionador começa com queens[0]
, a primeira variável na matriz, conforme indicado.
por CHOOSE_FIRST_UNBOUND
. Em seguida, o solucionador atribui ao queens[0]
o menor
um valor que ainda não foi testado, que é 0 nesta etapa, conforme direcionado por
ASSIGN_MIN_VALUE
. Isso coloca a primeira rainha no canto superior esquerdo do
tábua.
Em seguida, o solucionador seleciona queens[1]
, que agora é a primeira variável desvinculada em
queens
. Depois de propagar as restrições, há duas linhas possíveis para uma
queen da coluna 1: linha 2 ou linha 3. A opção ASSIGN_MIN_VALUE
direciona o
solucionador para atribuir queens[1] = 2
. Se em vez disso, você definir IntValueStrategy
como
ASSIGN_MAX_VALUE
, o solucionador atribuiria queens[1] = 3
.
É possível verificar se o restante da pesquisa segue as mesmas regras.
Chamar o solucionador e exibir os resultados
O código a seguir executa o solucionador e mostra a solução.
Python
# Iterates through the solutions, displaying each. num_solutions = 0 solver.NewSearch(db) while solver.NextSolution(): # Displays the solution just computed. for i in range(board_size): for j in range(board_size): if queens[j].Value() == i: # There is a queen in column j, row i. print("Q", end=" ") else: print("_", end=" ") print() print() num_solutions += 1 solver.EndSearch()
C++
// Iterates through the solutions, displaying each. int num_solutions = 0; solver.NewSearch(db); while (solver.NextSolution()) { // Displays the solution just computed. LOG(INFO) << "Solution " << num_solutions; for (int i = 0; i < board_size; ++i) { std::stringstream ss; for (int j = 0; j < board_size; ++j) { if (queens[j]->Value() == i) { // There is a queen in column j, row i. ss << "Q"; } else { ss << "_"; } if (j != board_size - 1) ss << " "; } LOG(INFO) << ss.str(); } num_solutions++; } solver.EndSearch();
Java
int solutionCount = 0; solver.newSearch(db); while (solver.nextSolution()) { System.out.println("Solution " + solutionCount); for (int i = 0; i < boardSize; ++i) { for (int j = 0; j < boardSize; ++j) { if (queens[j].value() == i) { System.out.print("Q"); } else { System.out.print("_"); } if (j != boardSize - 1) { System.out.print(" "); } } System.out.println(); } solutionCount++; } solver.endSearch();
C#
// Iterates through the solutions, displaying each. int SolutionCount = 0; solver.NewSearch(db); while (solver.NextSolution()) { Console.WriteLine("Solution " + SolutionCount); for (int i = 0; i < BoardSize; ++i) { for (int j = 0; j < BoardSize; ++j) { if (queens[j].Value() == i) { Console.Write("Q"); } else { Console.Write("_"); } if (j != BoardSize - 1) Console.Write(" "); } Console.WriteLine(""); } SolutionCount++; } solver.EndSearch();
Esta é a primeira solução encontrada pelo programa para uma placa 8x8.
Q _ _ _ _ _ _ _ _ _ _ _ _ _ Q _ _ _ _ _ Q _ _ _ _ _ _ _ _ _ _ Q _ Q _ _ _ _ _ _ _ _ _ Q _ _ _ _ _ _ _ _ _ Q _ _ _ _ Q _ _ _ _ _ ...91 other solutions displayed... Statistics failures: 304 branches: 790 wall time: 5 ms Solutions found: 92
Você pode resolver o problema de uma placa de tamanho diferente passando N como um
argumento de linha de comando. Por exemplo, python nqueens_cp.py 6
resolve o problema.
para uma placa de 6x6.
Todo o programa
O programa completo é mostrado abaixo.
Python
"""OR-Tools solution to the N-queens problem.""" import sys from ortools.constraint_solver import pywrapcp def main(board_size): # Creates the solver. solver = pywrapcp.Solver("n-queens") # Creates the variables. # The array index is the column, and the value is the row. queens = [solver.IntVar(0, board_size - 1, f"x{i}") for i in range(board_size)] # Creates the constraints. # All rows must be different. solver.Add(solver.AllDifferent(queens)) # No two queens can be on the same diagonal. solver.Add(solver.AllDifferent([queens[i] + i for i in range(board_size)])) solver.Add(solver.AllDifferent([queens[i] - i for i in range(board_size)])) db = solver.Phase(queens, solver.CHOOSE_FIRST_UNBOUND, solver.ASSIGN_MIN_VALUE) # Iterates through the solutions, displaying each. num_solutions = 0 solver.NewSearch(db) while solver.NextSolution(): # Displays the solution just computed. for i in range(board_size): for j in range(board_size): if queens[j].Value() == i: # There is a queen in column j, row i. print("Q", end=" ") else: print("_", end=" ") print() print() num_solutions += 1 solver.EndSearch() # Statistics. print("\nStatistics") print(f" failures: {solver.Failures()}") print(f" branches: {solver.Branches()}") print(f" wall time: {solver.WallTime()} ms") print(f" Solutions found: {num_solutions}") if __name__ == "__main__": # By default, solve the 8x8 problem. size = 8 if len(sys.argv) > 1: size = int(sys.argv[1]) main(size)
C++
// OR-Tools solution to the N-queens problem. #include <cstdint> #include <cstdlib> #include <sstream> #include <vector> #include "ortools/base/logging.h" #include "ortools/constraint_solver/constraint_solver.h" namespace operations_research { void NQueensCp(const int board_size) { // Instantiate the solver. Solver solver("N-Queens"); std::vector<IntVar*> queens; queens.reserve(board_size); for (int i = 0; i < board_size; ++i) { queens.push_back( solver.MakeIntVar(0, board_size - 1, absl::StrCat("x", i))); } // Define constraints. // The following sets the constraint that all queens are in different rows. solver.AddConstraint(solver.MakeAllDifferent(queens)); // All columns must be different because the indices of queens are all // different. No two queens can be on the same diagonal. std::vector<IntVar*> diag_1; diag_1.reserve(board_size); std::vector<IntVar*> diag_2; diag_2.reserve(board_size); for (int i = 0; i < board_size; ++i) { diag_1.push_back(solver.MakeSum(queens[i], i)->Var()); diag_2.push_back(solver.MakeSum(queens[i], -i)->Var()); } solver.AddConstraint(solver.MakeAllDifferent(diag_1)); solver.AddConstraint(solver.MakeAllDifferent(diag_2)); DecisionBuilder* const db = solver.MakePhase( queens, Solver::CHOOSE_FIRST_UNBOUND, Solver::ASSIGN_MIN_VALUE); // Iterates through the solutions, displaying each. int num_solutions = 0; solver.NewSearch(db); while (solver.NextSolution()) { // Displays the solution just computed. LOG(INFO) << "Solution " << num_solutions; for (int i = 0; i < board_size; ++i) { std::stringstream ss; for (int j = 0; j < board_size; ++j) { if (queens[j]->Value() == i) { // There is a queen in column j, row i. ss << "Q"; } else { ss << "_"; } if (j != board_size - 1) ss << " "; } LOG(INFO) << ss.str(); } num_solutions++; } solver.EndSearch(); // Statistics. LOG(INFO) << "Statistics"; LOG(INFO) << " failures: " << solver.failures(); LOG(INFO) << " branches: " << solver.branches(); LOG(INFO) << " wall time: " << solver.wall_time() << " ms"; LOG(INFO) << " Solutions found: " << num_solutions; } } // namespace operations_research int main(int argc, char** argv) { int board_size = 8; if (argc > 1) { board_size = std::atoi(argv[1]); } operations_research::NQueensCp(board_size); return EXIT_SUCCESS; }
Java
// OR-Tools solution to the N-queens problem. package com.google.ortools.constraintsolver.samples; import com.google.ortools.Loader; import com.google.ortools.constraintsolver.DecisionBuilder; import com.google.ortools.constraintsolver.IntVar; import com.google.ortools.constraintsolver.Solver; /** N-Queens Problem. */ public final class NQueensCp { public static void main(String[] args) { Loader.loadNativeLibraries(); // Instantiate the solver. Solver solver = new Solver("N-Queens"); int boardSize = 8; IntVar[] queens = new IntVar[boardSize]; for (int i = 0; i < boardSize; ++i) { queens[i] = solver.makeIntVar(0, boardSize - 1, "x" + i); } // Define constraints. // All rows must be different. solver.addConstraint(solver.makeAllDifferent(queens)); // All columns must be different because the indices of queens are all different. // No two queens can be on the same diagonal. IntVar[] diag1 = new IntVar[boardSize]; IntVar[] diag2 = new IntVar[boardSize]; for (int i = 0; i < boardSize; ++i) { diag1[i] = solver.makeSum(queens[i], i).var(); diag2[i] = solver.makeSum(queens[i], -i).var(); } solver.addConstraint(solver.makeAllDifferent(diag1)); solver.addConstraint(solver.makeAllDifferent(diag2)); // Create the decision builder to search for solutions. final DecisionBuilder db = solver.makePhase(queens, Solver.CHOOSE_FIRST_UNBOUND, Solver.ASSIGN_MIN_VALUE); int solutionCount = 0; solver.newSearch(db); while (solver.nextSolution()) { System.out.println("Solution " + solutionCount); for (int i = 0; i < boardSize; ++i) { for (int j = 0; j < boardSize; ++j) { if (queens[j].value() == i) { System.out.print("Q"); } else { System.out.print("_"); } if (j != boardSize - 1) { System.out.print(" "); } } System.out.println(); } solutionCount++; } solver.endSearch(); // Statistics. System.out.println("Statistics"); System.out.println(" failures: " + solver.failures()); System.out.println(" branches: " + solver.branches()); System.out.println(" wall time: " + solver.wallTime() + "ms"); System.out.println(" Solutions found: " + solutionCount); } private NQueensCp() {} }
C#
// OR-Tools solution to the N-queens problem. using System; using Google.OrTools.ConstraintSolver; public class NQueensCp { public static void Main(String[] args) { // Instantiate the solver. Solver solver = new Solver("N-Queens"); const int BoardSize = 8; IntVar[] queens = new IntVar[BoardSize]; for (int i = 0; i < BoardSize; ++i) { queens[i] = solver.MakeIntVar(0, BoardSize - 1, $"x{i}"); } // Define constraints. // All rows must be different. solver.Add(queens.AllDifferent()); // All columns must be different because the indices of queens are all different. // No two queens can be on the same diagonal. IntVar[] diag1 = new IntVar[BoardSize]; IntVar[] diag2 = new IntVar[BoardSize]; for (int i = 0; i < BoardSize; ++i) { diag1[i] = solver.MakeSum(queens[i], i).Var(); diag2[i] = solver.MakeSum(queens[i], -i).Var(); } solver.Add(diag1.AllDifferent()); solver.Add(diag2.AllDifferent()); // Create the decision builder to search for solutions. DecisionBuilder db = solver.MakePhase(queens, Solver.CHOOSE_FIRST_UNBOUND, Solver.ASSIGN_MIN_VALUE); // Iterates through the solutions, displaying each. int SolutionCount = 0; solver.NewSearch(db); while (solver.NextSolution()) { Console.WriteLine("Solution " + SolutionCount); for (int i = 0; i < BoardSize; ++i) { for (int j = 0; j < BoardSize; ++j) { if (queens[j].Value() == i) { Console.Write("Q"); } else { Console.Write("_"); } if (j != BoardSize - 1) Console.Write(" "); } Console.WriteLine(""); } SolutionCount++; } solver.EndSearch(); // Statistics. Console.WriteLine("Statistics"); Console.WriteLine($" failures: {solver.Failures()}"); Console.WriteLine($" branches: {solver.Branches()}"); Console.WriteLine($" wall time: {solver.WallTime()} ms"); Console.WriteLine($" Solutions found: {SolutionCount}"); } }
Número de soluções
O número de soluções aumenta de forma exponencial com o tamanho da placa:
Tamanho do tabuleiro | Soluções | Tempo para encontrar todas as soluções (ms) |
---|---|---|
1 | 1 | 0 |
2 | 0 | 0 |
3 | 0 | 0 |
4 | 2 | 0 |
5 | 10 | 0 |
6 | 4 | 0 |
7 | 40 | 3 |
8 | 92 | 9 |
9 | 352 | 35 |
10 | 724 | 95 |
11 | 2680 | 378 |
12 | 14200 | 2198 |
13 | 73712 | 11628 |
14 | 365596 | 62427 |
15 | 2279184 | 410701 |
Muitas soluções são apenas rotações de outras e uma técnica chamada simetria a quebra pode ser usada para reduzir a quantidade de computação necessária. Não usamos isso aqui; nossa solução acima não foi feita para ser rápida, apenas simples. Claro, poderíamos agilizar muito se quiséssemos encontrar apenas uma solução em vez de todos eles: não mais do que alguns milissegundos para tamanhos de placa de até 50.