In den folgenden Abschnitten veranschaulichen wir die Einschränkungsprogrammierung (CP) anhand eines ein kombinatorisches Problem beim Schachspiel. Beim Schach kann eine Königin angreifen. horizontal, vertikal und diagonal sein. Das Problem der N-Königinnen fragt:
Wie kann ein NxN-Schachbrett mit N Queens platziert werden, damit keine zwei angreifen miteinander kommunizieren?
Unten sehen Sie eine mögliche Lösung für das Problem der N-Queens bei N = 4.
Es dürfen sich keine zwei Queens in derselben Zeile, Spalte oder Diagonale befinden.
Hierbei handelt es sich nicht um ein Optimierungsproblem. Wir möchten alle möglichen anstatt einer optimalen Lösung, die sie zu einem natürlichen Kandidaten macht, Einschränkungsprogrammierung. In den folgenden Abschnitten wird der CP-Ansatz für das N-Queens-Problem beschrieben. Präsentiere Programme, die es sowohl mit dem CP-SAT-Rechner als auch mit dem ursprünglichen CP lösen. Solver.
CP-Ansatz für das n-Queens-Problem
Ein CP-Löser testet systematisch alle möglichen Zuweisungen von Werten zu den Variablen in einem Problem, realisierbaren Lösungen. Bei der Aufgabe der 4 Königinnen beginnt der Löser ganz links und platziert nacheinander in jeder Spalte eine Queen, an einer Position, nicht von zuvor platzierten Queens angegriffen werden.
Weitergabe und Rückverfolgung
Es gibt zwei Schlüsselelemente einer Suche mit Einschränkungsprogrammierung:
- Weitergabe: Jedes Mal, wenn der Rechner einer Variablen einen Wert zuweist, Einschränkungen fügen den möglichen Werten der nicht zugewiesenen Variablen. Diese Einschränkungen gelten für zukünftige Variablenzuweisungen. Beim Vier-Königinnen-Problem wird jedes Mal, wenn der Löser eine Königin platziert, kann keine anderen Königinnen in die Reihe und die Diagonalen der aktuellen Königin aufnehmen. Die Weitergabe kann die Suche erheblich beschleunigen, da weniger Variablenwerte, die der Matherechner untersuchen muss.
- Ein Backtracking tritt auf, wenn der Matherechner dem nächsten Variable zu sein, weil es Einschränkungen gibt, oder es findet eine Lösung. In beiden Fällen Solver kehrt zu einer vorherigen Phase zurück und ändert den Wert der Variablen bis zu einem Wert, der noch nicht ausprobiert wurde. Im Beispiel mit den 4 Queens Das bedeutet, dass eine Queen in ein neues Quadrat in der aktuellen Spalte verschoben wird.
Als Nächstes sehen Sie, wie die Einschränkungsprogrammierung Propagierung und Backtracking nutzt, um das 4-Queens-Problem lösen.
Nehmen wir an, der Rechner beginnt mit willkürlich einer Königin oben links . Das ist eine Art Hypothese: stellt sich vielleicht heraus, dass keine Lösung mit einer Königin in der oberen linken Ecke.
Welche Einschränkungen können wir angesichts dieser Hypothese propagieren? Eine Einschränkung besteht darin, eine Spalte darf nur eine Königin enthalten (das graue X unten) und eine andere Beschränkung zweier Queens auf derselben Diagonalen (die roten Xs unten).
Die dritte Einschränkung verbietet Queens in derselben Zeile:
Nachdem unsere Beschränkungen übertragen wurden, können wir eine weitere Hypothese testen und eine die zweite Königin auf einem der verbleibenden Plätze. Unser Matherechner könnte entscheiden, um das erste verfügbare Quadrat in die zweite Spalte einzufügen:
Nach dem Übertragen der diagonalen Fixierung lässt sich verfügbaren Quadraten entweder in der dritten Spalte oder in der letzten Zeile:
Da es in dieser Phase keine Lösungsmöglichkeiten gibt, müssen wir den Fortschritt zurückverfolgen. Eine Möglichkeit ist, damit der Rechner das andere verfügbare Quadrat in der zweiten Spalte auswählt. Durch die Einschränkungspropagierung wird jedoch eine Queen in die zweite Zeile des Spalte und lassen Sie keine gültigen Plätze für die vierte Königin übrig:
Also muss der Matherechner diesmal bis zum die Platzierung der ersten Queen. Wir haben gezeigt, dass keine Lösung ein Quadrat in der Ecke einnimmt.
Da es keine Königin in der Ecke geben kann, zieht der Solver die erste Königin nach unten. und propagiert, wobei nur ein Platz für die zweite Königin übrig bleibt:
Wenn sich die Königin noch einmal verbreitet, ist nur noch ein Platz für die dritte Königin sichtbar:
Und für die vierte und letzte Queen:
Wir haben unsere erste Lösung! Wenn wir unseren Matherechner angewiesen hätten, nach der die erste Lösung wäre, würde sie hier enden. Andernfalls würde es wieder rückwirkend die erste Queen in die dritte Zeile der ersten Spalte.
Lösung mit CP-SAT
Das N-Queens-Problem eignet sich ideal für die Einschränkungsprogrammierung. In dieser sehen wir uns ein kurzes Python-Programm an, alle Lösungen für das Problem zu finden.
Bibliotheken importieren
Mit dem folgenden Code wird die erforderliche Bibliothek importiert.
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;
Modell deklarieren
Mit dem folgenden Code wird das CP-SAT-Modell deklariert.
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()}"); } }
Variablen erstellen
Der Solver erstellt die Variablen für die Aufgabe als Array mit dem Namen 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}"); }
Hier wird davon ausgegangen, dass queens[j]
die Zeilennummer für die Queen in Spalte j
ist.
Mit anderen Worten: queens[j] = i
bedeutet, dass sich in Zeile i
und Spalte j
eine Queen befindet.
Einschränkungen erstellen
Hier ist der Code, der die Einschränkungen für das Problem erstellt.
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);
Im Code wird die Methode AddAllDifferent
verwendet, bei der alle Elemente einer
unterschiedlich sein.
Sehen wir uns an, wie diese Einschränkungen die drei Bedingungen für die N-Queens garantieren. Problem (Queens auf verschiedenen Zeilen, Spalten und Diagonalen).
Keine zwei Queens in derselben Reihe
Bei Anwendung der AllDifferent
-Methode des Solver für queens
werden die Werte von
queens[j]
für jede j
unterschiedlich sein, was bedeutet, dass alle Queens in
in verschiedenen Zeilen.
Keine zwei Queens in derselben Spalte
Diese Einschränkung ist in der Definition von queens
implizit enthalten.
Da zwei Elemente von queens
nicht denselben Index haben dürfen, können keine zwei Queens
in derselben Spalte.
Keine zwei Königinnen auf derselben Diagonalen
Die diagonale Einschränkung ist etwas schwieriger als die Zeilen- und Spalteneinschränkungen. Wenn zwei Königinnen auf derselben Diagonalen liegen, gilt Folgendes: muss wahr sein:
- Die Zeilennummer plus die Spaltennummer für jede der beiden Queens sind gleich.
Mit anderen Worten:
queens(j) + j
hat für zwei verschiedene Indizes denselben Wertj
. - Die Zeilennummer minus die Spaltennummer für jede der beiden Queens ist gleich.
In diesem Fall hat
queens(j) - j
denselben Wert für zwei verschiedene Indizesj
.
Eine dieser Bedingungen bedeutet, dass die Königinnen auf derselben aufsteigenden Diagonale liegen ( von links nach rechts), während die anderen bedeutet, dass sie auf demselben Punkt (absteigend) liegen diagonal sein. Welche Bedingung der aufsteigenden und welche der absteigenden Bedingung entspricht hängt davon ab, wie Sie die Zeilen und Spalten anordnen. Wie in den im vorherigen Abschnitt angegeben haben, hat die Reihenfolge keine Auswirkungen auf die wie Sie sie visualisieren.
Die diagonale Einschränkung besagt, dass die Werte von queens(j) + j
alle gleich
und die Werte von queens(j) - j
müssen alle unterschiedlich sein,
unterschiedlichen j
.
Um die Methode AddAllDifferent
auf queens(j) + j
anzuwenden, setzen wir die N Instanzen
der Variablen für j
von 0
bis N-1
in das Array diag1
ein:
q1 = model.NewIntVar(0, 2 * board_size, 'diag1_%i' % i) diag1.append(q1) model.Add(q1 == queens[j] + j)
Dann wenden wir AddAllDifferent
auf diag1
an.
model.AddAllDifferent(diag1)
Die Einschränkung für queens(j) - j
wird auf ähnliche Weise erstellt.
Lösungsdrucker erstellen
Um alle Lösungen für das Problem der n-queens auszudrucken, müssen Sie einen Callback senden, als Lösungsdrucker bezeichnet, zum CP-SAT-Löser. Der Callback druckt alle sobald der Rechner sie findet. Mit dem folgenden Code wird eine Lösung Drucker.
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_; }
Beachten Sie, dass der Lösungsdrucker als Python-Klasse geschrieben werden muss, da der Python-Schnittstelle zum zugrunde liegenden C++-Resolver.
Die Lösungen werden anhand der folgenden Zeilen im Lösungsdrucker gedruckt.
for v in self.__variables: print('%s = %i' % (v, self.Value(v)), end = ' ')
In diesem Beispiel ist self.__variables
die Variable queens
und jede v
entspricht einem der acht Einträge von queens
. Dies druckt eine Lösung in
das folgende Format: x0 = queens(0) x1 = queens(1) ... x7 = queens(7)
, wobei
xi
ist die Spaltennummer der Queen in Zeile i
.
Der nächste Abschnitt zeigt ein Beispiel für eine Lösung.
Solver aufrufen und die Ergebnisse anzeigen
Mit dem folgenden Code wird der Löser ausgeführt und die Lösungen werden angezeigt.
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);
Das Programm umfasst 92 verschiedene Lösungen für ein 8x8-Board. Hier ist deine erste Frage.
Q _ _ _ _ _ _ _ _ _ _ _ _ _ Q _ _ _ _ _ Q _ _ _ _ _ _ _ _ _ _ Q _ Q _ _ _ _ _ _ _ _ _ Q _ _ _ _ _ _ _ _ _ Q _ _ _ _ Q _ _ _ _ _ ...91 other solutions displayed... Solutions found: 92
Sie können das Problem für ein Board mit einer anderen Größe lösen, indem Sie N als ein
Befehlszeilenargument. Wenn das Programm beispielsweise den Namen queens
hat,
python nqueens_sat.py 6
löst das Problem für ein 6x6-Board.
Das gesamte Programm
Hier ist das gesamte Programm für das N-Queens-Programm.
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()}"); } }
Lösung mit ursprünglichem CP-Löser
In den folgenden Abschnitten wird ein Python-Programm vorgestellt, das N-Quenns mithilfe der Methode ursprünglicher CP-Löser. Wir empfehlen jedoch die Verwendung des neueren CP-SAT-Lösers.
Bibliotheken importieren
Mit dem folgenden Code wird die erforderliche Bibliothek importiert.
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;
Löser deklarieren
Mit dem folgenden Code wird der ursprüngliche CP-Löser deklariert.
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");
Variablen erstellen
Mit der Methode IntVar
des Matherechners werden die Variablen für die Aufgabe als Array erstellt.
mit dem Namen 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}"); }
Bei jeder Lösung bedeutet queens[j] = i
, dass sich in Spalte j
und Zeile eine Queen befindet.
i
Einschränkungen erstellen
Hier ist der Code, der die Einschränkungen für das Problem erstellt.
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());
Diese Einschränkungen garantieren die drei Bedingungen für das Problem der n-queens ( Queens auf verschiedenen Zeilen, Spalten und Diagonalen).
Keine zwei Queens in derselben Reihe
Bei Anwendung der AllDifferent
-Methode des Solver für queens
werden die Werte von
queens[j]
für jede j
unterschiedlich sein, was bedeutet, dass alle Queens in
in verschiedenen Zeilen.
Keine zwei Queens in derselben Spalte
Diese Einschränkung ist in der Definition von queens
implizit enthalten.
Da zwei Elemente von queens
nicht denselben Index haben dürfen, können keine zwei Queens
in derselben Spalte.
Keine zwei Königinnen auf derselben Diagonalen
Die diagonale Einschränkung ist etwas schwieriger als die Zeilen- und Spalteneinschränkungen. Erstens: Wenn zwei Königinnen auf derselben Diagonalen liegen, muss eine der folgenden Aussagen zutreffen:
- Ist die Diagonale absteigend, also von links nach rechts, wird die Zeilennummer plus
Spaltennummer für jede der beiden Queens gleich ist.
queens(i) + i
hat also die denselben Wert für zwei verschiedene Indizesi
. - Ist die Diagonale aufsteigend, wird die Zeilennummer abzüglich der Spaltennummer jedes
der beiden Queens gleich sind. In diesem Fall hat
queens(i) - i
denselben Wert für zwei verschiedene Indizesi
.
Die diagonale Einschränkung besagt, dass die Werte von queens(i) + i
alle gleich
und auch die Werte von queens(i) - i
müssen alle unterschiedlich sein,
unterschiedlichen i
.
Der obige Code fügt diese Einschränkung hinzu, indem der
AllDifferent
queens[j] + j
und queens[j] - j
für jeden i
hinzu.
Entscheidungsträger hinzufügen
Im nächsten Schritt erstellen Sie einen Entscheidungsträger, der die Suchstrategie festlegt. für das Problem. Die Suchstrategie kann einen großen Einfluss auf die Suchdauer haben, aufgrund der Weitergabe von Einschränkungen, wodurch sich die Anzahl der Variablenwerte verringert. mit dem Matherechner erforschen muss. Ein Beispiel hierfür haben Sie bereits Beispiel für 4 Queens.
Mit dem folgenden Code wird mithilfe der Funktion
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);
Weitere Informationen
Eingabeargumente für die Methode Phase
.
So funktioniert der Entscheidungsträger im „4-Queens-Beispiel“
Sehen wir uns an, wie Entscheidungsträger die Suche
Beispiel für 4 Queens.
Der Matherechner beginnt mit queens[0]
, der ersten Variable im Array,
von CHOOSE_FIRST_UNBOUND
Der Matherechner weist dann queens[0]
den kleinsten Wert zu
Wert, der noch nicht ausprobiert wurde, also 0 in dieser Phase, wie von
ASSIGN_MIN_VALUE
. Dadurch wird die erste Queen in die obere linke Ecke des
Board.
Als Nächstes wählt der Solver queens[1]
aus. Dies ist jetzt die erste ungebundene Variable in
queens
. Nach der Weitergabe der Einschränkungen gibt es zwei mögliche Zeilen für eine
in Spalte 1: Zeile 2 oder Zeile 3. Mit der Option ASSIGN_MIN_VALUE
wird der
um queens[1] = 2
zuzuweisen. (Wenn Sie stattdessen IntValueStrategy
auf
ASSIGN_MAX_VALUE
verwendet, weist der Matherechner queens[1] = 3
zu.)
Sie können prüfen, ob der Rest der Suche denselben Regeln folgt.
Solver aufrufen und die Ergebnisse anzeigen
Mit dem folgenden Code wird der Matherechner ausgeführt.
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();
Hier ist die erste vom Programm gefundene Lösung für ein 8x8-Board.
Q _ _ _ _ _ _ _ _ _ _ _ _ _ Q _ _ _ _ _ Q _ _ _ _ _ _ _ _ _ _ Q _ Q _ _ _ _ _ _ _ _ _ Q _ _ _ _ _ _ _ _ _ Q _ _ _ _ Q _ _ _ _ _ ...91 other solutions displayed... Statistics failures: 304 branches: 790 wall time: 5 ms Solutions found: 92
Sie können das Problem für ein Board mit einer anderen Größe lösen, indem Sie N als
Befehlszeilenargument. Beispiel: python nqueens_cp.py 6
löst das Problem.
für ein 6x6-Board.
Das gesamte Programm
Das vollständige Programm finden Sie unten.
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}"); } }
Anzahl der Lösungen
Die Anzahl der Lösungen erhöht sich in etwa exponentiell mit der Größe der Tafel:
Größe des Spielfelds | Lösungen | Zeit zum Ermitteln aller Lösungen (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 |
Viele Lösungen sind Drehungen anderer und eine Technik, die als Symmetrie bezeichnet wird. kann verwendet werden, um den Rechenaufwand zu reduzieren. Wir verwenden keine das hier; unsere Lösung oben nicht schnell, sondern einfach zu sein. Natürlich Wir könnten es viel schneller machen, wenn wir nur eine Lösung finden wollten, anstatt alle: höchstens ein paar Millisekunden für Boardgrößen bis 50.