always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

sat: NQueensSat in all languages

Browse Source
This commit is contained in:
Corentin Le Molgat
2021-10-21 15:12:49 +02:00
parent f317305497
commit 0d6e2a9169
5 changed files with 389 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
makefiles/Makefile.python.mk
View File

@@ -662,6 +662,7 @@ test_python_sat_samples: \
rpy_literal_sample_sat \
rpy_minimal_jobshop_sat \
rpy_no_overlap_sample_sat \
rpy_nqueens_sat \
rpy_nurses_sat \
rpy_optional_interval_sample_sat \
rpy_rabbits_and_pheasants_sat \
@@ -856,7 +857,6 @@ test_python_python: \
rpy_linear_assignment_api \
rpy_linear_programming \
rpy_magic_sequence_distribute \
rpy_nqueens_sat \
rpy_pyflow_example \
rpy_reallocate_sat \
rpy_rcpsp_sat \

123
ortools/sat/samples/NQueensSat.cs Normal file
View File

@@ -0,0 +1,123 @@
// Copyright 2010-2021 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
// OR-Tools solution to the N-queens problem.
// [START import]
using System;
using Google.OrTools.Sat;
// [END import]
public class NQueensSat
{
// [START solution_printer]
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_;
}
// [END solution_printer]
static void Main()
{
// Constraint programming engine
// [START model]
CpModel model = new CpModel();
// [START model]
// [START variables]
int BoardSize = 8;
IntVar[] queens = new IntVar[BoardSize];
for (int i = 0; i < BoardSize; ++i)
{
queens[i] = model.NewIntVar(0, BoardSize - 1, $"x{i}");
}
// [END variables]
// Define constraints.
// [START constraints]
// All rows must be different.
model.AddAllDifferent(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)
{
IntVar tmp1 = model.NewIntVar(0, BoardSize * 2, $"x{i}");
model.Add(LinearExpr.Sum(new IntVar[]{queens[i], model.NewConstant(i)}) == tmp1);
diag1[i] = tmp1;
IntVar tmp2 = model.NewIntVar(-BoardSize, BoardSize, $"x{i}");
model.Add(LinearExpr.Sum(new IntVar[]{queens[i], model.NewConstant(-i)}) == tmp2);
diag2[i] = tmp2;
}
model.AddAllDifferent(diag1);
model.AddAllDifferent(diag2);
// [END constraints]
// [START solve]
// 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);
// [END solve]
// [START statistics]
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()}");
// [END statistics]
}
}
// [END program]

120
ortools/sat/samples/NQueensSat.java Normal file
View File

@@ -0,0 +1,120 @@
// Copyright 2010-2021 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
package com.google.ortools.sat.samples;
// [START import]
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;
// [END import]
/** OR-Tools solution to the N-queens problem. */
public final class NQueensSat {
// [START solution_printer]
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;
}
// [END solution_printer]
public static void main(String[] args) throws Exception {
Loader.loadNativeLibraries();
// Create the model.
// [START model]
CpModel model = new CpModel();
// [END model]
// [START variables]
int boardSize = 8;
IntVar[] queens = new IntVar[boardSize];
for (int i = 0; i < boardSize; ++i) {
queens[i] = model.newIntVar(0, boardSize - 1, "x" + i);
}
// [END variables]
// Define constraints.
// [START constraints]
// All rows must be different.
model.addAllDifferent(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] = model.newIntVar(0, boardSize * 2, "x" + i);
model.addEquality(LinearExpr.sum(new IntVar[]{queens[i], model.newConstant(i)}), diag1[i]);
diag2[i] = model.newIntVar(-boardSize, boardSize, "x" + i);
model.addEquality(LinearExpr.sum(new IntVar[]{queens[i], model.newConstant(-i)}), diag2[i]);
}
model.addAllDifferent(diag1);
model.addAllDifferent(diag2);
// [END constraints]
// Create a solver and solve the model.
// [START solve]
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);
// [END solve]
// Statistics.
// [START 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());
// [END statistics]
}
private NQueensSat() {}
}
// [END program]

117
ortools/sat/samples/nqueens_sat.cc Normal file
View File

@@ -0,0 +1,117 @@
// Copyright 2010-2021 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// [START program]
// OR-Tools solution to the N-queens problem.
// [START import]
#include <cstdint>
#include <vector>
#include "ortools/sat/cp_model.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
// [END import]
namespace operations_research {
namespace sat {
void NQueensSat(const int board_size) {
// Instantiate the solver.
// [START model]
CpModelBuilder cp_model;
// [END model]
// [START variables]
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)));
}
// [END variables]
// Define constraints.
// [START constraints]
// The following sets the constraint that all queens are in different rows.
cp_model.AddAllDifferent(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) {
IntVar tmp_1 = cp_model.NewIntVar(Domain(0, board_size * 2)).WithName("x" + std::to_string(i));
cp_model.AddEquality(LinearExpr::Sum({queens[i], cp_model.NewConstant(i)}), tmp_1);
diag_1.push_back(tmp_1);
IntVar tmp_2 = cp_model.NewIntVar(Domain(-board_size, board_size)).WithName("x" + std::to_string(i));
cp_model.AddEquality(LinearExpr::Sum({queens[i], cp_model.NewConstant(-i)}), tmp_2);
diag_2.push_back(tmp_2);
}
cp_model.AddAllDifferent(diag_1);
cp_model.AddAllDifferent(diag_2);
// [END constraints]
// [START solution_printer]
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++;
}));
// [END solution_printer]
// [START solve]
// 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;
// [END solve]
// Statistics.
// [START statistics]
LOG(INFO) << "Statistics";
LOG(INFO) << CpSolverResponseStats(response);
// [END statistics]
}
} // namespace sat
} // namespace operations_research
int main(int argc, char** argv) {
int board_size = 8;
if (argc > 1) {
board_size = std::atoi(argv[1]);
}
operations_research::sat::NQueensSat(board_size);
return EXIT_SUCCESS;
}
// [END program]

39
examples/python/nqueens_sat.py → ortools/sat/samples/nqueens_sat.py
View File

@@ -1,3 +1,4 @@
#!/usr/bin/env python3
# Copyright 2010-2021 Google LLC
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
@@ -10,12 +11,16 @@
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
# [START program]
"""OR-Tools solution to the N-queens problem."""
# [START import]
import time
import sys
from ortools.sat.python import cp_model
# [END import]
# [START solution_printer]
class NQueenSolutionPrinter(cp_model.CpSolverSolutionCallback):
"""Print intermediate solutions."""
@@ -44,18 +49,25 @@ class NQueenSolutionPrinter(cp_model.CpSolverSolutionCallback):
print('_', end=' ')
print()
print()
# [END solution_printer]
def main(board_size):
# Creates the solver.
# [START model]
model = cp_model.CpModel()
# [END model]
# Creates the variables.
# [START variables]
# The array index is the column, and the value is the row.
queens = [
model.NewIntVar(0, board_size - 1, 'x%i' % i) for i in range(board_size)
]
# Creates the constraints.
# [END variables]
# Creates the constraints.
# [START constraints]
# All rows must be different.
model.AddAllDifferent(queens)
@@ -74,25 +86,30 @@ def main(board_size):
model.Add(q2 == queens[i] - i)
model.AddAllDifferent(diag1)
model.AddAllDifferent(diag2)
# [END constraints]
### Solve model.
# Solve the model.
# [START solve]
solver = cp_model.CpSolver()
solution_printer = NQueenSolutionPrinter(queens)
solver.parameters.enumerate_all_solutions = True
status = solver.Solve(model, solution_printer)
# [END solve]
print()
print('Statistics')
print(' - conflicts : %i' % solver.NumConflicts())
print(' - branches : %i' % solver.NumBranches())
print(' - wall time : %f s' % solver.WallTime())
print(' - solutions found : %i' % solution_printer.solution_count())
# Statistics.
# [START statistics]
print('\nStatistics')
print(f' conflicts : {solver.NumConflicts()}')
print(f' branches : {solver.NumBranches()}')
print(f' wall time : {solver.WallTime()} s')
print(f' solutions found: {solution_printer.solution_count()}')
# [END statistics]
# By default, solve the 8x8 problem.
board_size = 8
if __name__ == '__main__':
# By default, solve the 8x8 problem.
board_size = 8
if len(sys.argv) > 1:
board_size = int(sys.argv[1])
main(board_size)
# [END program]