Trong các phần sau, chúng tôi sẽ minh hoạ quy trình lập trình ràng buộc (CP) bằng một bài toán tổ hợp dựa trên trò chơi cờ vua. Trong cờ vua, quân hậu có thể tấn công theo chiều ngang, chiều dọc và đường chéo. Bài toán N-queens đặt câu hỏi:
Làm thế nào có thể xếp N Hậu trên một bàn cờ NxN để không có 2 nữ hoàng nào tấn công nhau?
Dưới đây, bạn có thể thấy một giải pháp khả thi cho bài toán N-queens với N = 4.
Không có 2 nữ hoàng trên cùng một hàng, cột hoặc đường chéo.
Hãy lưu ý rằng đây không phải là vấn đề tối ưu hoá: chúng ta muốn tìm mọi giải pháp khả thi thay vì một giải pháp tối ưu, khiến giải pháp này trở thành đề xuất tự nhiên để lập trình ràng buộc. Các phần sau mô tả cách tiếp cận CP cho bài toán N-queens, đồng thời trình bày các chương trình giải quyết vấn đề đó bằng cách sử dụng cả trình giải CP-SAT và trình phân giải CP ban đầu.
Cách tiếp cận của CP đối với bài toán N-queens
Trình phân giải CP hoạt động bằng cách thử tất cả các phép gán giá trị có thể có cho các biến trong một bài toán một cách có hệ thống để tìm ra giải pháp khả thi. Trong bài toán 4 nữ hoàng, trình giải quyết bắt đầu ở cột ngoài cùng bên trái và liên tiếp đặt một nữ hoàng vào mỗi cột, tại một vị trí không bị bất kỳ nữ hoàng nào đã đặt trước đó tấn công.
Truyền và theo dõi ngược
Có hai phần tử chính của một nội dung tìm kiếm lập trình ràng buộc:
- Pagation – Mỗi khi trình phân giải gán một giá trị cho một biến, các điều kiện ràng buộc sẽ thêm các hạn chế đối với những giá trị có thể có của các biến chưa được chỉ định. Những quy tắc hạn chế này áp dụng đến các lượt chỉ định biến trong tương lai. Ví dụ: trong bài toán 4 nữ hoàng, mỗi lần trình giải quyết đặt một nữ hoàng khác, nó không thể đặt bất kỳ nữ hoàng nào khác trên hàng và theo các đường chéo mà nữ hoàng hiện tại đang bật. Việc truyền tải có thể tăng tốc độ tìm kiếm đáng kể bằng cách giảm tập hợp các giá trị biến mà trình giải phải khám phá.
- Tính năng Theo dõi ngược xảy ra khi trình giải quyết không thể chỉ định giá trị cho biến tiếp theo, do các quy tắc ràng buộc hoặc do trình phân giải tìm thấy giải pháp. Trong cả hai trường hợp, trình giải quyết quay lại giai đoạn trước và thay đổi giá trị của biến ở giai đoạn đó thành một giá trị chưa được thử. Trong ví dụ 4 nữ hoàng, điều này có nghĩa là di chuyển một Queen sang một hình vuông mới trên cột hiện tại.
Tiếp theo, bạn sẽ thấy cách lập trình ràng buộc sử dụng tính năng truyền và theo dõi ngược để giải quyết vấn đề 4-queens.
Giả sử trình giải toán bắt đầu bằng cách tuỳ ý đặt một nữ hoàng ở góc trên bên trái. Đấy là một giả thuyết; có lẽ sẽ cho thấy rằng không có giải pháp nào tồn tại với một nữ hoàng ở góc trên bên trái.
Với giả thuyết này, chúng ta có thể tuyên truyền những hạn chế nào? Một quy tắc ràng buộc là chỉ có thể có một nữ hoàng trong một cột (dấu X màu xám bên dưới) và một quy tắc ràng buộc khác cấm hai nữ hoàng trên cùng một đường chéo (dấu X màu đỏ ở bên dưới).
Quy tắc ràng buộc thứ ba của chúng tôi cấm các nữ hoàng trên cùng một hàng:
Đã lan truyền các điều kiện ràng buộc, chúng ta có thể thử nghiệm một giả thuyết khác và đặt nữ hoàng thứ hai trên một trong các hình vuông còn lại. Trình giải toán của chúng tôi có thể quyết định đặt vào ô vuông đầu tiên có sẵn trong cột thứ hai:
Sau khi lan truyền quy tắc ràng buộc theo đường chéo, chúng ta có thể thấy rằng không có hình vuông nào có sẵn trong cột thứ ba hoặc hàng cuối cùng:
Nếu không có giải pháp nào khả thi ở giai đoạn này, chúng tôi cần phải theo dõi lại. Một phương án là để trình giải quyết chọn hình vuông khác có sẵn trong cột thứ hai. Tuy nhiên, việc truyền bá quy tắc ràng buộc sau đó buộc một Hậu trang vào hàng thứ hai của cột thứ ba, khiến không có vị trí hợp lệ nào cho Hậu tố thứ tư:
Và trình giải toán phải quay ngược lại, lần này cho đến tận vị trí của nữ hoàng đầu tiên. Giờ đây, chúng tôi đã chứng minh được rằng không có giải pháp nào cho vấn đề về ảnh Queen sẽ chiếm một góc vuông.
Vì không thể có nữ hoàng ở góc, nên trình giải quyết di chuyển nữ hoàng thứ nhất xuống một vị trí rồi truyền, chỉ để lại một vị trí cho nữ hoàng thứ hai:
Việc truyền bá một lần nữa cho thấy chỉ còn lại một vị trí cho Nữ hoàng thứ ba:
Và lần thứ tư cũng là nữ hoàng cuối cùng:
Chúng tôi đã có giải pháp đầu tiên! Nếu chúng tôi hướng dẫn trình giải toán của mình dừng lại sau khi tìm thấy giải pháp đầu tiên, thì giải pháp đầu tiên sẽ kết thúc ở đây. Nếu không, quá trình này sẽ đảo ngược một lần nữa và đặt nữ hoàng đầu tiên vào hàng thứ ba của cột đầu tiên.
Giải pháp sử dụng CP-SAT
Bài toán N-queens phù hợp lý tưởng với lập trình ràng buộc. Trong phần này, chúng ta sẽ tìm hiểu một chương trình Python ngắn sử dụng trình giải CP-SAT để tìm tất cả giải pháp cho vấn đề.
Nhập thư viện
Mã sau đây nhập thư viện bắt buộc.
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;
Khai báo mô hình
Đoạn mã sau đây khai báo mô hình 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()}");
}
}
Tạo các biến
Trình giải toán sẽ tạo các biến cho bài toán dưới dạng một mảng có tên là 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}");
}
Ở đây, chúng ta giả định rằng queens[j] là số hàng của Queen trong cột j.
Nói cách khác, queens[j] = i có nghĩa là có một nữ hoàng trong hàng i và cột j.
Tạo các điều kiện ràng buộc
Dưới đây là mã tạo ra các điều kiện ràng buộc cho bài toán này.
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);
Mã này sử dụng phương thức AddAllDifferent. Phương thức này yêu cầu tất cả các phần tử của một mảng biến phải khác nhau.
Hãy xem cách những điều kiện ràng buộc này đảm bảo 3 điều kiện cho vấn đề N-queens (các nữ hoàng trên các hàng, cột và đường chéo khác nhau).
Không có hai nữ hoàng trên cùng một hàng
Việc áp dụng phương thức AllDifferent của trình giải cho queens sẽ buộc các giá trị của queens[j] khác nhau đối với mỗi j, nghĩa là tất cả các Queen phải nằm ở các hàng khác nhau.
Không có hai nữ hoàng trên cùng một cột
Quy tắc ràng buộc này được ngầm ẩn trong định nghĩa của queens.
Vì không có hai phần tử nào của queens có thể có cùng một chỉ mục, nên không thể có hai hậu tố ở trong cùng một cột.
Không có hai nữ hoàng trên cùng một đường chéo
Giới hạn đường chéo phức tạp hơn một chút so với giới hạn hàng và cột. Trước tiên, nếu 2 Queen nằm trên cùng một đường chéo, thì một trong các điều kiện sau phải đúng:
- Số hàng cộng với số cột của từng nữ hoàng bằng nhau.
Nói cách khác,
queens(j) + jcó cùng một giá trị với hai chỉ mụcjkhác nhau. - Số hàng trừ đi số cột của từng nữ hoàng bằng nhau.
Trong trường hợp này,
queens(j) - jcó cùng một giá trị cho hai chỉ mụcjkhác nhau.
Một trong những điều kiện này có nghĩa là các Queen nằm trên cùng một đường chéo tăng dần (từ trái sang phải), trong khi điều kiện còn lại có nghĩa là chúng nằm trên cùng một đường chéo giảm dần. Điều kiện nào tương ứng với tăng dần và giảm dần tuỳ thuộc vào cách bạn sắp xếp các hàng và cột. Như đã đề cập trong phần trước, thứ tự không ảnh hưởng đến tập hợp giải pháp mà chỉ ảnh hưởng đến cách bạn trực quan hoá các giải pháp.
Vì vậy, giới hạn đường chéo là giá trị của queens(j) + j phải khác nhau và tất cả giá trị của queens(j) - j phải khác nhau cho j khác nhau.
Để áp dụng phương thức AddAllDifferent cho queens(j) + j, chúng ta đặt N thực thể của biến (cho j) từ 0 đến N-1 vào một mảng diag1 như sau:
q1 = model.NewIntVar(0, 2 * board_size, 'diag1_%i' % i) diag1.append(q1) model.Add(q1 == queens[j] + j)
Sau đó, chúng ta áp dụng AddAllDifferent cho diag1.
model.AddAllDifferent(diag1)
Quy tắc ràng buộc cho queens(j) - j được tạo ra tương tự.
Tạo máy in giải pháp
Để in tất cả lời giải cho bài toán N-queens, bạn cần truyền lệnh gọi lại (còn gọi là máy in giải pháp) đến trình giải CP-SAT. Lệnh gọi lại sẽ in từng giải pháp mới khi trình phân giải tìm thấy giải pháp đó. Mã sau đây sẽ tạo một trình in giải pháp.
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_;
}
Lưu ý rằng máy in giải pháp phải được viết dưới dạng một lớp Python, do giao diện Python dành cho trình giải mã C++ cơ bản.
Các giải pháp được in bằng các dòng sau trên máy in giải pháp.
for v in self.__variables:
print('%s = %i' % (v, self.Value(v)), end = ' ')
Trong ví dụ này, self.__variables là biến queens và mỗi v tương ứng với một trong 8 mục của queens. Thao tác này sẽ in giải pháp ở dạng sau: x0 = queens(0) x1 = queens(1) ... x7 = queens(7), trong đó xi là số cột của Queen trong hàng i.
Phần tiếp theo sẽ trình bày ví dụ về một giải pháp.
Gọi trình giải và hiện kết quả
Mã sau đây chạy trình giải và hiển thị các giải pháp.
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);
Chương trình sẽ tìm được 92 giải pháp khác nhau cho một bảng 8x8. Mời bạn nghe tin đầu tiên.
Q _ _ _ _ _ _ _
_ _ _ _ _ _ Q _
_ _ _ _ Q _ _ _
_ _ _ _ _ _ _ Q
_ Q _ _ _ _ _ _
_ _ _ Q _ _ _ _
_ _ _ _ _ Q _ _
_ _ Q _ _ _ _ _
...91 other solutions displayed...
Solutions found: 92
Bạn có thể giải bài toán này cho một bảng có kích thước khác bằng cách truyền vào N dưới dạng đối số dòng lệnh. Ví dụ: nếu chương trình có tên là queens, python nqueens_sat.py 6 sẽ giải quyết vấn đề cho bảng 6x6.
Toàn bộ chương trình
Đây là toàn bộ chương trình của chương trình 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()}");
}
}
Giải pháp sử dụng trình giải CP gốc
Các phần sau đây trình bày một chương trình Python giải quyết N-queen bằng trình phân giải CP ban đầu. (Tuy nhiên, bạn nên dùng trình giải CP-SAT mới)
Nhập thư viện
Mã sau đây nhập thư viện bắt buộc.
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;
Khai báo trình giải
Mã sau đây khai báo trình giải CP gốc.
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");
Tạo các biến
Phương thức IntVar của trình giải toán sẽ tạo các biến cho bài toán dưới dạng một mảng có tên là 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}");
}
Đối với mọi đáp án, queens[j] = i có nghĩa là có một nữ hoàng trong cột j và hàng i.
Tạo các điều kiện ràng buộc
Dưới đây là mã tạo ra các điều kiện ràng buộc cho bài toán này.
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());
Các điều kiện ràng buộc này đảm bảo 3 điều kiện cho bài toán N-queens (các nữ hoàng trên nhiều hàng, cột và đường chéo).
Không có hai nữ hoàng trên cùng một hàng
Việc áp dụng phương thức AllDifferent của trình giải cho queens sẽ buộc các giá trị của queens[j] phải khác nhau đối với mỗi j, tức là tất cả các Queen phải ở các hàng khác nhau.
Không có hai nữ hoàng trên cùng một cột
Quy tắc ràng buộc này được ngầm ẩn trong định nghĩa của queens.
Vì không có hai phần tử nào của queens có thể có cùng một chỉ mục, nên không thể có hai hậu tố ở trong cùng một cột.
Không có hai nữ hoàng trên cùng một đường chéo
Giới hạn đường chéo phức tạp hơn một chút so với giới hạn hàng và cột. Đầu tiên, nếu hai Hậu nữ nằm trên cùng một đường chéo, một trong các điều sau phải là đúng:
- Nếu đường chéo giảm dần (từ trái sang phải), thì số hàng và số cột của từng 2 Hậu bằng nhau. Vì vậy,
queens(i) + icó cùng một giá trị cho hai chỉ mụcikhác nhau. - Nếu đường chéo tăng dần, số hàng trừ đi số cột của từng 2 Hậu trang bằng nhau. Trong trường hợp này,
queens(i) - icó cùng giá trị cho hai chỉ mụcikhác nhau.
Vì vậy, điều kiện ràng buộc theo đường chéo là các giá trị của queens(i) + i phải khác nhau và tương tự như vậy, tất cả giá trị của queens(i) - i phải khác nhau cho i khác nhau.
Đoạn mã ở trên thêm quy tắc ràng buộc này bằng cách áp dụng phương thức AllDifferent cho queens[j] + j và queens[j] - j cho mỗi i.
Thêm trình tạo quyết định
Bước tiếp theo là tạo trình tạo quyết định, việc này sẽ đặt chiến lược tìm kiếm cho vấn đề. Chiến lược tìm kiếm có thể có tác động lớn đến thời gian tìm kiếm, do việc truyền các giới hạn, giúp làm giảm số lượng giá trị biến mà trình giải toán phải khám phá. Bạn đã thấy một ví dụ về việc này trong ví dụ về 4-queens.
Mã sau đây tạo một trình tạo quyết định bằng phương thức Phase của trình giải.
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);
Hãy xem Trình tạo quyết định để biết thông tin chi tiết về các đối số đầu vào cho phương thức Phase.
Cách hoạt động của trình tạo quyết định trong ví dụ 4 nữ hoàng
Hãy xem cách trình tạo quyết định hướng hoạt động tìm kiếm trong
ví dụ 4-queens.
Trình phân giải bắt đầu bằng queens[0], biến đầu tiên trong mảng, theo chỉ dẫn của CHOOSE_FIRST_UNBOUND. Sau đó, trình phân giải sẽ chỉ định queens[0] giá trị nhỏ nhất chưa được thử. Giá trị này là 0 ở giai đoạn này, theo chỉ dẫn của ASSIGN_MIN_VALUE. Thao tác này sẽ đặt Hậu đầu tiên ở góc trên bên trái của bảng.
Tiếp theo, trình giải quyết chọn queens[1], hiện là biến không liên kết đầu tiên trong queens. Sau khi truyền các quy tắc ràng buộc, có thể có 2 hàng cho một nữ hoàng trong cột 1: hàng 2 hoặc hàng 3. Tuỳ chọn ASSIGN_MIN_VALUE hướng dẫn trình giải quyết gán queens[1] = 2. (Nếu bạn đặt IntValueStrategy thành ASSIGN_MAX_VALUE, trình giải toán sẽ chỉ định queens[1] = 3.)
Bạn có thể kiểm tra để đảm bảo rằng các nội dung tìm kiếm còn lại đều tuân theo các quy tắc tương tự.
Gọi trình giải và hiện kết quả
Mã sau đây chạy trình giải và hiển thị giải pháp.
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();
Dưới đây là giải pháp đầu tiên mà chương trình tìm thấy cho bảng 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
Bạn có thể giải bài toán này cho một bảng có kích thước khác bằng cách truyền vào N dưới dạng đối số dòng lệnh. Ví dụ: python nqueens_cp.py 6 giải quyết vấn đề cho bảng 6x6.
Toàn bộ chương trình
Chương trình hoàn chỉnh được hiển thị dưới đây.
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}");
}
}
Số lượng giải pháp
Số lượng nghiệm tăng lên gần theo cấp số nhân với kích thước của bảng:
| Kích thước bảng | Giải pháp | Thời gian để tìm tất cả nghiệm (mili giây) |
|---|---|---|
| 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 |
Nhiều giải pháp chỉ là sự xoay của những giải pháp khác và một kỹ thuật có tên là phá đối xứng có thể được dùng để giảm khối lượng tính toán cần thiết. Chúng tôi không sử dụng giải pháp đó ở đây; giải pháp của chúng tôi ở trên không nhằm mục đích nhanh chóng, chỉ là đơn giản. Tất nhiên, chúng ta có thể làm cho quá trình này nhanh hơn nhiều nếu chỉ muốn tìm một giải pháp thay vì tất cả các giải pháp: không quá vài mili giây đối với kích thước bảng lên tới 50.