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

fix sat bugs found by new examples; improve gitignore

Browse Source
This commit is contained in:
Laurent Perron
2017-10-11 03:05:13 -07:00
parent 48837ce11f
commit 20ba8015bc
8 changed files with 285 additions and 24 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
.gitignore vendored
View File

@@ -27,8 +27,9 @@ lib/
examples/csharp/solution/*.csproj
examples/csharp/*.sln
src/bazel-*
ortools/bazel-*
examples/bazel-*
bazel-*
tools/docker/export

172
examples/python/hidato_sat.py Normal file
View File

@@ -0,0 +1,172 @@
from ortools.sat.python import cp_model
def BuildPairs(rows, cols):
"""Build closeness pairs for consecutive numbers.
Build set of allowed pairs such that two consecutive numbers touch
each other in the grid.
Returns:
A list of pairs for allowed consecutive position of numbers.
Args:
rows: the number of rows in the grid
cols: the number of columns in the grid
"""
return [(x * cols + y, (x + dx) * cols + (y + dy))
for x in range(rows) for y in range(cols)
for dx in (-1, 0, 1) for dy in (-1, 0, 1)
if (x + dx >= 0 and x + dx < rows and
y + dy >= 0 and y + dy < cols and (dx != 0 or dy != 0))]
def PrintSolution(positions, rows, cols):
"""Print a current solution."""
# Create empty board.
board = []
for _ in range(rows):
board.append([0] * cols)
# Fill board with solution value.
for k in range(rows * cols):
position = positions[k]
board[position // cols][position % cols] = k + 1
# Print the board.
print('Solution')
PrintMatrix(board)
def PrintMatrix(game):
"""Pretty print of a matrix."""
rows = len(game)
cols = len(game[0])
for i in range(rows):
line = ''
for j in range(cols):
if game[i][j] == 0:
line += ' .'
else:
line += '% 3s' % game[i][j]
print(line)
def SolveHidato(problem):
"""Solve the given hidato table."""
# Create the model.
model = cp_model.CpModel()
#
# models, a 0 indicates an open cell which number is not yet known.
#
#
puzzle = None
if problem == 1:
# Simple problem
puzzle = [[6, 0, 9],
[0, 2, 8],
[1, 0, 0]]
elif problem == 2:
puzzle = [[0, 44, 41, 0, 0, 0, 0],
[0, 43, 0, 28, 29, 0, 0],
[0, 1, 0, 0, 0, 33, 0],
[0, 2, 25, 4, 34, 0, 36],
[49, 16, 0, 23, 0, 0, 0],
[0, 19, 0, 0, 12, 7, 0],
[0, 0, 0, 14, 0, 0, 0]]
elif problem == 3:
# Problems from the book:
# Gyora Bededek: "Hidato: 2000 Pure Logic Puzzles"
# Problem 1 (Practice)
puzzle = [[0, 0, 20, 0, 0],
[0, 0, 0, 16, 18],
[22, 0, 15, 0, 0],
[23, 0, 1, 14, 11],
[0, 25, 0, 0, 12]]
elif problem == 4:
# problem 2 (Practice)
puzzle = [[0, 0, 0, 0, 14],
[0, 18, 12, 0, 0],
[0, 0, 17, 4, 5],
[0, 0, 7, 0, 0],
[9, 8, 25, 1, 0]]
elif problem == 5:
# problem 3 (Beginner)
puzzle = [[0, 26, 0, 0, 0, 18],
[0, 0, 27, 0, 0, 19],
[31, 23, 0, 0, 14, 0],
[0, 33, 8, 0, 15, 1],
[0, 0, 0, 5, 0, 0],
[35, 36, 0, 10, 0, 0]]
elif problem == 6:
# Problem 15 (Intermediate)
puzzle = [[64, 0, 0, 0, 0, 0, 0, 0],
[1, 63, 0, 59, 15, 57, 53, 0],
[0, 4, 0, 14, 0, 0, 0, 0],
[3, 0, 11, 0, 20, 19, 0, 50],
[0, 0, 0, 0, 22, 0, 48, 40],
[9, 0, 0, 32, 23, 0, 0, 41],
[27, 0, 0, 0, 36, 0, 46, 0],
[28, 30, 0, 35, 0, 0, 0, 0]]
r = len(puzzle)
c = len(puzzle[0])
print(('Initial game (%i x %i)' % (r, c)))
PrintMatrix(puzzle)
#
# declare variables
#
positions = [model.NewIntVar(0, r * c - 1, 'p[%i]' % i)
for i in range(r * c)]
#
# constraints
#
model.AddAllDifferent(positions)
#
# Fill in the clues
#
for i in range(r):
for j in range(c):
if puzzle[i][j] > 0:
model.Add(positions[puzzle[i][j] - 1] == i * c + j)
# Consecutive numbers much touch each other in the grid.
# We use an allowed assignment constraint to model it.
close_tuples = BuildPairs(r, c)
for k in range(0, r * c - 1):
model.AddAllowedAssignments([positions[k], positions[k + 1]], close_tuples)
#
# solution and search
#
solver = cp_model.CpSolver()
status = solver.Solve(model)
if status == cp_model.MODEL_SAT:
PrintSolution([solver.Value(x) for x in positions], r, c,)
print('Statistics')
print(' - conflicts : %i' % solver.NumConflicts())
print(' - branches : %i' % solver.NumBranches())
print(' - wall time : %f ms' % solver.WallTime())
def main():
for table in range(1, 7):
print('')
print('----- Solving problem %i -----' % table)
print('')
SolveHidato(table)
if __name__ == '__main__':
main()

70
examples/python/jobshop_ft06_sat.py Normal file
View File

@@ -0,0 +1,70 @@
from ortools.sat.python import cp_model
def main():
# Creates the solver.
model = cp_model.CpModel()
machines_count = 6
jobs_count = 6
all_machines = range(0, machines_count)
all_jobs = range(0, jobs_count)
durations = [[1, 3, 6, 7, 3, 6],
[8, 5, 10, 10, 10, 4],
[5, 4, 8, 9, 1, 7],
[5, 5, 5, 3, 8, 9],
[9, 3, 5, 4, 3, 1],
[3, 3, 9, 10, 4, 1]]
machines = [[2, 0, 1, 3, 5, 4],
[1, 2, 4, 5, 0, 3],
[2, 3, 5, 0, 1, 4],
[1, 0, 2, 3, 4, 5],
[2, 1, 4, 5, 0, 3],
[1, 3, 5, 0, 4, 2]]
# Computes horizon dynamically.
horizon = sum([sum(durations[i]) for i in all_jobs])
# Creates jobs.
all_tasks = {}
for i in all_jobs:
for j in all_machines:
start = model.NewIntVar(0, horizon, 'start_%i_%i' % (i, j))
duration = durations[i][j]
end = model.NewIntVar(0, horizon, 'end_%i_%i' % (i, j))
interval = model.NewIntervalVar(start, duration, end,
'interval_%i_%i' % (i, j))
all_tasks[(i, j)] = (start, end, interval)
# Create disjuctive constraints.
machine_to_jobs = {}
for i in all_machines:
machines_jobs = []
for j in all_jobs:
for k in all_machines:
if machines[j][k] == i:
machines_jobs.append(all_tasks[(j, k)][2])
machine_to_jobs[i] = machines_jobs
model.AddNoOverlap(machines_jobs)
# Precedences inside a job.
for i in all_jobs:
for j in range(0, machines_count - 1):
model.Add(all_tasks[(i, j + 1)][0] >= all_tasks[(i, j)][1])
# Makespan objective.
obj_var = model.NewIntVar(0, horizon, 'makespan')
model.AddMaxEquality(
obj_var, [all_tasks[(i, machines_count - 1)][1] for i in all_jobs])
model.Minimize(obj_var)
# Solve model.
solver = cp_model.CpSolver()
response = solver.Solve(model)
print(solver.ObjectiveValue())
if __name__ == '__main__':
main()

19
ortools/sat/cp_model_solver.cc
View File

@@ -1917,14 +1917,8 @@ IntegerVariable AddLPConstraints(const CpModelProto& model_proto,
}
}
IntegerVariable main_objective_var;
if (m->GetOrCreate<SatSolver>()->parameters().optimize_with_core()) {
main_objective_var =
GetOrCreateVariableWithTightBound(top_level_cp_terms, m->model());
} else {
main_objective_var = GetOrCreateVariableGreaterOrEqualToSumOf(
top_level_cp_terms, m->model());
}
const IntegerVariable main_objective_var =
GetOrCreateVariableGreaterOrEqualToSumOf(top_level_cp_terms, m->model());
// Register LP constraints. Note that this needs to be done after all the
// constraints have been added.
@@ -2085,12 +2079,7 @@ CpSolverResponse SolveCpModelInternal(
for (int i = 0; i < obj.vars_size(); ++i) {
terms.push_back(std::make_pair(m.Integer(obj.vars(i)), obj.coeffs(i)));
}
if (parameters.optimize_with_core()) {
objective_var = GetOrCreateVariableWithTightBound(terms, m.model());
} else {
objective_var =
GetOrCreateVariableGreaterOrEqualToSumOf(terms, m.model());
}
objective_var = GetOrCreateVariableGreaterOrEqualToSumOf(terms, m.model());
}
// Intersect the objective domain with the given one if any.
@@ -2112,7 +2101,7 @@ CpSolverResponse SolveCpModelInternal(
// Make sure the sum take a value inside the objective domain by adding
// the other side: objective <= sum terms.
//
// TODO(user): Use a better condidtion to detect when this is not usefull.
// TODO(user): Use a better condition to detect when this is not usefull.
if (user_domain != automatic_domain) {
std::vector<IntegerVariable> vars;
std::vector<int64> coeffs;

5
ortools/sat/linear_programming_constraint.cc
View File

@@ -277,8 +277,11 @@ bool LinearProgrammingConstraint::Propagate() {
// it past our current objective upper-bound (we will already fail as soon
// as we pass it). Note that this limit is properly transformed using the
// objective scaling factor and offset stored in lp_data_.
//
// Note that we use a bigger epsilon here to be sure that if we abort
// because of this, we will report a conflict.
parameters.set_objective_upper_limit(static_cast<double>(
integer_trail_->UpperBound(objective_cp_).value() + kEpsilon));
integer_trail_->UpperBound(objective_cp_).value() + 100.0 * kEpsilon));
}
// Put an iteration limit on the work we do in the simplex for this call. Note

19
ortools/sat/python/cp_model.py
View File

@@ -34,6 +34,13 @@ from ortools.sat import pywrapsat
INT_MIN = -9223372036854775808 # hardcoded to be platform independent.
INT_MAX = 9223372036854775807
# Cp Solver status (exported to avoid importing cp_model_cp2).
UNKNOWN = cp_model_pb2.UNKNOWN
MODEL_INVALID = cp_model_pb2.MODEL_INVALID
MODEL_SAT = cp_model_pb2.MODEL_SAT
MODEL_UNSAT = cp_model_pb2.MODEL_UNSAT
OPTIMAL = cp_model_pb2.OPTIMAL
def AssertIsInt64(x):
if not isinstance(x, numbers.Integral):
@@ -868,3 +875,15 @@ class CpSolver(object):
def StatusName(self, status):
return cp_model_pb2.CpSolverStatus.Name(status)
def NumBooleans(self):
return self.__solution.num_booleans
def NumConflicts(self):
return self.__solution.num_conflicts
def NumBranches(self):
return self.__solution.num_branches
def WallTime(self):
return self.__solution.wall_time

15
ortools/sat/table.cc
View File

@@ -89,9 +89,13 @@ void ProcessOneColumn(const std::vector<Literal>& line_literals,
// is false too (i.e not possible).
for (int i = 0; i < values.size(); ++i) {
const IntegerValue v = values[i];
value_to_list_of_line_literals[v].push_back(line_literals[i]);
model->Add(Implication(FindOrDie(encoding, v).Negated(),
line_literals[i].Negated()));
if (!ContainsKey(encoding, v)) {
model->Add(ClauseConstraint({line_literals[i].Negated()}));
} else {
value_to_list_of_line_literals[v].push_back(line_literals[i]);
model->Add(Implication(FindOrDie(encoding, v).Negated(),
line_literals[i].Negated()));
}
}
// If all the tuples containing a value are false, then this value must be
@@ -159,7 +163,6 @@ std::function<void(Model*)> TableConstraint(
// Fully encode the variables using all the values appearing in the tuples.
IntegerTrail* interger_trail = model->GetOrCreate<IntegerTrail>();
std::unordered_map<IntegerValue, Literal> encoding;
const std::vector<std::vector<int64>> tr_tuples = Transpose(new_tuples);
for (int i = 0; i < n; ++i) {
const int64 first = tr_tuples[i].front();
@@ -170,11 +173,10 @@ std::function<void(Model*)> TableConstraint(
interger_trail->UpdateInitialDomain(
vars[i], SortedDisjointIntervalsFromValues(tr_tuples[i]));
model->Add(FullyEncodeVariable(vars[i]));
encoding = GetEncoding(vars[i], model);
ProcessOneColumn(
tuple_literals,
std::vector<IntegerValue>(tr_tuples[i].begin(), tr_tuples[i].end()),
encoding, model);
GetEncoding(vars[i], model), model);
}
}
};
@@ -223,7 +225,6 @@ std::function<void(Model*)> NegatedTableConstraintWithoutFullEncoding(
const int64 value = tuple[i];
const int64 lb = model->Get(LowerBound(vars[i]));
const int64 ub = model->Get(UpperBound(vars[i]));
CHECK_LT(lb, ub);
// TODO(user): test the full initial domain instead of just checking
// the bounds.
if (value < lb || value > ub) {

6
tools/docker/Makefile
View File

@@ -56,6 +56,9 @@ ubuntu-14.04-archive: export ubuntu-14.04-image
ubuntu-14.04-test: export ubuntu-14.04-image
docker run -w /root/or-tools -v `pwd`/export:/export or-tools-ubuntu-14.04-image:latest /bin/bash -c "git pull; make clean; make all -j 5; make test"
ubuntu-14.04-bash: export ubuntu-14.04-image
docker run -it or-tools-ubuntu-14.04-image:latest /bin/bash
# Ubuntu 16.06 images
ubuntu-16.04-image:
@@ -70,6 +73,9 @@ ubuntu-16.04-archive: export ubuntu-16.04-image
ubuntu-16.04-test: export ubuntu-16.04-image
docker run -w /root/or-tools -v `pwd`/export:/export or-tools-ubuntu-16.04-image:latest /bin/bash -c "git pull; make clean; make all -j 5; make test"
ubuntu-16.04-bash: export ubuntu-16.04-image
docker run -it or-tools-ubuntu-16.04-image:latest /bin/bash
# Ubuntu 17.04 images
ubuntu-17.04-image: