From df333efbcdfdd54d8988b46a2c75f524aa4d38cb Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Thu, 3 May 2018 15:00:06 +0200 Subject: [PATCH] rewrite drat checker for sat; make fz presolve deterministic; more optims on sat internals --- makefiles/Makefile.gen.mk | 89 ++- ortools/flatzinc/parser.tab.cc | 13 + ortools/flatzinc/parser.yy.cc | 13 + ortools/flatzinc/presolve.cc | 37 +- ortools/flatzinc/presolve.h | 2 + ortools/glop/revised_simplex.cc | 49 +- ortools/linear_solver/linear_solver.cc | 1 - ortools/sat/clause.cc | 4 +- ortools/sat/clause.h | 8 +- ortools/sat/cp_model_solver.cc | 126 +++- ortools/sat/drat_checker.cc | 609 ++++++++++++++++++ ortools/sat/drat_checker.h | 340 ++++++++++ .../sat/{drat.cc => drat_proof_handler.cc} | 84 ++- ortools/sat/{drat.h => drat_proof_handler.h} | 67 +- ortools/sat/drat_writer.cc | 59 ++ ortools/sat/drat_writer.h | 64 ++ ortools/sat/integer.cc | 25 +- ortools/sat/integer.h | 5 +- ortools/sat/integer_search.cc | 3 + ortools/sat/optimization.cc | 102 +++ ortools/sat/optimization.h | 8 + ortools/sat/sat_parameters.proto | 41 +- ortools/sat/sat_solver.cc | 50 +- ortools/sat/sat_solver.h | 16 +- ortools/sat/simplification.cc | 55 +- ortools/sat/simplification.h | 15 +- 26 files changed, 1653 insertions(+), 232 deletions(-) create mode 100644 ortools/sat/drat_checker.cc create mode 100644 ortools/sat/drat_checker.h rename ortools/sat/{drat.cc => drat_proof_handler.cc} (53%) rename ortools/sat/{drat.h => drat_proof_handler.h} (59%) create mode 100644 ortools/sat/drat_writer.cc create mode 100644 ortools/sat/drat_writer.h diff --git a/makefiles/Makefile.gen.mk b/makefiles/Makefile.gen.mk index 26a83b7d4b..29e41d596c 100644 --- a/makefiles/Makefile.gen.mk +++ b/makefiles/Makefile.gen.mk @@ -597,7 +597,7 @@ $(OBJ_DIR)/util/xml_helper.$O: \ $(GEN_DIR)/ortools/util/optional_boolean.pb.cc: \ $(SRC_DIR)/ortools/util/optional_boolean.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/util/optional_boolean.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/util/optional_boolean.proto $(GEN_DIR)/ortools/util/optional_boolean.pb.h: $(GEN_DIR)/ortools/util/optional_boolean.pb.cc \ @@ -672,7 +672,7 @@ $(OBJ_DIR)/data/set_covering_parser.$O: \ $(GEN_DIR)/ortools/data/jobshop_scheduling.pb.cc: \ $(SRC_DIR)/ortools/data/jobshop_scheduling.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/data/jobshop_scheduling.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/data/jobshop_scheduling.proto $(GEN_DIR)/ortools/data/jobshop_scheduling.pb.h: $(GEN_DIR)/ortools/data/jobshop_scheduling.pb.cc \ @@ -681,7 +681,7 @@ $(OBJ_DIR)/data/jobshop_scheduling.pb.$O: $(GEN_DIR)/ortools/data/jobshop_schedu $(GEN_DIR)/ortools/data/rcpsp.pb.cc: \ $(SRC_DIR)/ortools/data/rcpsp.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/data/rcpsp.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/data/rcpsp.proto $(GEN_DIR)/ortools/data/rcpsp.pb.h: $(GEN_DIR)/ortools/data/rcpsp.pb.cc \ @@ -1223,7 +1223,7 @@ $(OBJ_DIR)/glop/variable_values.$O: \ $(GEN_DIR)/ortools/glop/parameters.pb.cc: \ $(SRC_DIR)/ortools/glop/parameters.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/glop/parameters.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/glop/parameters.proto $(GEN_DIR)/ortools/glop/parameters.pb.h: $(GEN_DIR)/ortools/glop/parameters.pb.cc \ @@ -1467,7 +1467,7 @@ $(OBJ_DIR)/graph/util.$O: \ $(GEN_DIR)/ortools/graph/flow_problem.pb.cc: \ $(SRC_DIR)/ortools/graph/flow_problem.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/graph/flow_problem.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/graph/flow_problem.proto $(GEN_DIR)/ortools/graph/flow_problem.pb.h: $(GEN_DIR)/ortools/graph/flow_problem.pb.cc \ @@ -1585,7 +1585,9 @@ SAT_DEPS = \ $(SRC_DIR)/ortools/sat/cp_model_utils.h \ $(SRC_DIR)/ortools/sat/cumulative.h \ $(SRC_DIR)/ortools/sat/disjunctive.h \ - $(SRC_DIR)/ortools/sat/drat.h \ + $(SRC_DIR)/ortools/sat/drat_checker.h \ + $(SRC_DIR)/ortools/sat/drat_proof_handler.h \ + $(SRC_DIR)/ortools/sat/drat_writer.h \ $(SRC_DIR)/ortools/sat/encoding.h \ $(SRC_DIR)/ortools/sat/integer_expr.h \ $(SRC_DIR)/ortools/sat/integer.h \ @@ -1627,7 +1629,9 @@ SAT_LIB_OBJS = \ $(OBJ_DIR)/sat/cp_model_utils.$O \ $(OBJ_DIR)/sat/cumulative.$O \ $(OBJ_DIR)/sat/disjunctive.$O \ - $(OBJ_DIR)/sat/drat.$O \ + $(OBJ_DIR)/sat/drat_checker.$O \ + $(OBJ_DIR)/sat/drat_proof_handler.$O \ + $(OBJ_DIR)/sat/drat_writer.$O \ $(OBJ_DIR)/sat/encoding.$O \ $(OBJ_DIR)/sat/integer.$O \ $(OBJ_DIR)/sat/integer_expr.$O \ @@ -1691,7 +1695,7 @@ $(SRC_DIR)/ortools/sat/clause.h: \ $(SRC_DIR)/ortools/base/int_type_indexed_vector.h \ $(SRC_DIR)/ortools/base/macros.h \ $(SRC_DIR)/ortools/base/span.h \ - $(SRC_DIR)/ortools/sat/drat.h \ + $(SRC_DIR)/ortools/sat/drat_proof_handler.h \ $(SRC_DIR)/ortools/sat/sat_base.h \ $(GEN_DIR)/ortools/sat/sat_parameters.pb.h \ $(SRC_DIR)/ortools/util/bitset.h \ @@ -1755,12 +1759,24 @@ $(SRC_DIR)/ortools/sat/disjunctive.h: \ $(SRC_DIR)/ortools/sat/sat_base.h \ $(SRC_DIR)/ortools/sat/theta_tree.h -$(SRC_DIR)/ortools/sat/drat.h: \ - $(SRC_DIR)/ortools/base/file.h \ +$(SRC_DIR)/ortools/sat/drat_checker.h: \ + $(SRC_DIR)/ortools/base/int_type.h \ $(SRC_DIR)/ortools/base/int_type_indexed_vector.h \ $(SRC_DIR)/ortools/base/span.h \ $(SRC_DIR)/ortools/sat/sat_base.h +$(SRC_DIR)/ortools/sat/drat_proof_handler.h: \ + $(SRC_DIR)/ortools/base/int_type_indexed_vector.h \ + $(SRC_DIR)/ortools/base/span.h \ + $(SRC_DIR)/ortools/sat/drat_checker.h \ + $(SRC_DIR)/ortools/sat/drat_writer.h \ + $(SRC_DIR)/ortools/sat/sat_base.h + +$(SRC_DIR)/ortools/sat/drat_writer.h: \ + $(SRC_DIR)/ortools/base/file.h \ + $(SRC_DIR)/ortools/base/span.h \ + $(SRC_DIR)/ortools/sat/sat_base.h + $(SRC_DIR)/ortools/sat/encoding.h: \ $(SRC_DIR)/ortools/base/integral_types.h \ $(SRC_DIR)/ortools/base/int_type.h \ @@ -1929,7 +1945,7 @@ $(SRC_DIR)/ortools/sat/sat_solver.h: \ $(SRC_DIR)/ortools/base/span.h \ $(SRC_DIR)/ortools/base/timer.h \ $(SRC_DIR)/ortools/sat/clause.h \ - $(SRC_DIR)/ortools/sat/drat.h \ + $(SRC_DIR)/ortools/sat/drat_proof_handler.h \ $(SRC_DIR)/ortools/sat/model.h \ $(SRC_DIR)/ortools/sat/pb_constraint.h \ $(SRC_DIR)/ortools/sat/restart.h \ @@ -1947,7 +1963,7 @@ $(SRC_DIR)/ortools/sat/simplification.h: \ $(SRC_DIR)/ortools/base/int_type_indexed_vector.h \ $(SRC_DIR)/ortools/base/macros.h \ $(SRC_DIR)/ortools/base/span.h \ - $(SRC_DIR)/ortools/sat/drat.h \ + $(SRC_DIR)/ortools/sat/drat_proof_handler.h \ $(SRC_DIR)/ortools/sat/sat_base.h \ $(GEN_DIR)/ortools/sat/sat_parameters.pb.h \ $(SRC_DIR)/ortools/sat/sat_solver.h \ @@ -2173,14 +2189,31 @@ $(OBJ_DIR)/sat/disjunctive.$O: \ $(SRC_DIR)/ortools/sat/sat_solver.h $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sdisjunctive.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdisjunctive.$O -$(OBJ_DIR)/sat/drat.$O: \ - $(SRC_DIR)/ortools/sat/drat.cc \ +$(OBJ_DIR)/sat/drat_checker.$O: \ + $(SRC_DIR)/ortools/sat/drat_checker.cc \ + $(SRC_DIR)/ortools/base/numbers.h \ + $(SRC_DIR)/ortools/base/split.h \ + $(SRC_DIR)/ortools/base/stl_util.h \ + $(SRC_DIR)/ortools/base/time_support.h \ + $(SRC_DIR)/ortools/sat/drat_checker.h \ + $(SRC_DIR)/ortools/util/time_limit.h + $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sdrat_checker.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdrat_checker.$O + +$(OBJ_DIR)/sat/drat_proof_handler.$O: \ + $(SRC_DIR)/ortools/sat/drat_proof_handler.cc \ $(SRC_DIR)/ortools/base/int_type.h \ $(SRC_DIR)/ortools/base/logging.h \ + $(SRC_DIR)/ortools/base/memory.h \ + $(SRC_DIR)/ortools/sat/drat_proof_handler.h + $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sdrat_proof_handler.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdrat_proof_handler.$O + +$(OBJ_DIR)/sat/drat_writer.$O: \ + $(SRC_DIR)/ortools/sat/drat_writer.cc \ + $(SRC_DIR)/ortools/base/logging.h \ $(SRC_DIR)/ortools/base/status.h \ $(SRC_DIR)/ortools/base/stringprintf.h \ - $(SRC_DIR)/ortools/sat/drat.h - $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sdrat.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdrat.$O + $(SRC_DIR)/ortools/sat/drat_writer.h + $(CCC) $(CFLAGS) -c $(SRC_DIR)$Sortools$Ssat$Sdrat_writer.cc $(OBJ_OUT)$(OBJ_DIR)$Ssat$Sdrat_writer.$O $(OBJ_DIR)/sat/encoding.$O: \ $(SRC_DIR)/ortools/sat/encoding.cc \ @@ -2388,7 +2421,7 @@ $(OBJ_DIR)/sat/util.$O: \ $(GEN_DIR)/ortools/sat/boolean_problem.pb.cc: \ $(SRC_DIR)/ortools/sat/boolean_problem.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/sat/boolean_problem.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/sat/boolean_problem.proto $(GEN_DIR)/ortools/sat/boolean_problem.pb.h: $(GEN_DIR)/ortools/sat/boolean_problem.pb.cc \ @@ -2397,7 +2430,7 @@ $(OBJ_DIR)/sat/boolean_problem.pb.$O: $(GEN_DIR)/ortools/sat/boolean_problem.pb. $(GEN_DIR)/ortools/sat/cp_model.pb.cc: \ $(SRC_DIR)/ortools/sat/cp_model.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/sat/cp_model.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/sat/cp_model.proto $(GEN_DIR)/ortools/sat/cp_model.pb.h: $(GEN_DIR)/ortools/sat/cp_model.pb.cc \ @@ -2406,7 +2439,7 @@ $(OBJ_DIR)/sat/cp_model.pb.$O: $(GEN_DIR)/ortools/sat/cp_model.pb.cc $(GEN_DIR)/ortools/sat/sat_parameters.pb.cc: \ $(SRC_DIR)/ortools/sat/sat_parameters.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/sat/sat_parameters.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/sat/sat_parameters.proto $(GEN_DIR)/ortools/sat/sat_parameters.pb.h: $(GEN_DIR)/ortools/sat/sat_parameters.pb.cc \ @@ -2672,7 +2705,7 @@ $(OBJ_DIR)/bop/integral_solver.$O: \ $(GEN_DIR)/ortools/bop/bop_parameters.pb.cc: \ $(SRC_DIR)/ortools/bop/bop_parameters.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/bop/bop_parameters.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/bop/bop_parameters.proto $(GEN_DIR)/ortools/bop/bop_parameters.pb.h: $(GEN_DIR)/ortools/bop/bop_parameters.pb.cc \ @@ -2883,7 +2916,7 @@ $(OBJ_DIR)/linear_solver/scip_interface.$O: \ $(GEN_DIR)/ortools/linear_solver/linear_solver.pb.cc: \ $(SRC_DIR)/ortools/linear_solver/linear_solver.proto \ $(GEN_DIR)/ortools/util/optional_boolean.pb.cc - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/linear_solver/linear_solver.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/linear_solver/linear_solver.proto $(GEN_DIR)/ortools/linear_solver/linear_solver.pb.h: $(GEN_DIR)/ortools/linear_solver/linear_solver.pb.cc \ @@ -3571,7 +3604,7 @@ $(OBJ_DIR)/constraint_solver/visitor.$O: \ $(GEN_DIR)/ortools/constraint_solver/assignment.pb.cc: \ $(SRC_DIR)/ortools/constraint_solver/assignment.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/assignment.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/assignment.proto $(GEN_DIR)/ortools/constraint_solver/assignment.pb.h: $(GEN_DIR)/ortools/constraint_solver/assignment.pb.cc \ @@ -3580,7 +3613,7 @@ $(OBJ_DIR)/constraint_solver/assignment.pb.$O: $(GEN_DIR)/ortools/constraint_sol $(GEN_DIR)/ortools/constraint_solver/demon_profiler.pb.cc: \ $(SRC_DIR)/ortools/constraint_solver/demon_profiler.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/demon_profiler.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/demon_profiler.proto $(GEN_DIR)/ortools/constraint_solver/demon_profiler.pb.h: $(GEN_DIR)/ortools/constraint_solver/demon_profiler.pb.cc \ @@ -3590,7 +3623,7 @@ $(OBJ_DIR)/constraint_solver/demon_profiler.pb.$O: $(GEN_DIR)/ortools/constraint $(GEN_DIR)/ortools/constraint_solver/model.pb.cc: \ $(SRC_DIR)/ortools/constraint_solver/model.proto \ $(GEN_DIR)/ortools/constraint_solver/search_limit.pb.cc - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/model.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/model.proto $(GEN_DIR)/ortools/constraint_solver/model.pb.h: $(GEN_DIR)/ortools/constraint_solver/model.pb.cc \ @@ -3599,7 +3632,7 @@ $(OBJ_DIR)/constraint_solver/model.pb.$O: $(GEN_DIR)/ortools/constraint_solver/m $(GEN_DIR)/ortools/constraint_solver/routing_enums.pb.cc: \ $(SRC_DIR)/ortools/constraint_solver/routing_enums.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/routing_enums.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/routing_enums.proto $(GEN_DIR)/ortools/constraint_solver/routing_enums.pb.h: $(GEN_DIR)/ortools/constraint_solver/routing_enums.pb.cc \ @@ -3610,7 +3643,7 @@ $(GEN_DIR)/ortools/constraint_solver/routing_parameters.pb.cc: \ $(SRC_DIR)/ortools/constraint_solver/routing_parameters.proto \ $(GEN_DIR)/ortools/constraint_solver/routing_enums.pb.cc \ $(GEN_DIR)/ortools/constraint_solver/solver_parameters.pb.cc - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/routing_parameters.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/routing_parameters.proto $(GEN_DIR)/ortools/constraint_solver/routing_parameters.pb.h: $(GEN_DIR)/ortools/constraint_solver/routing_parameters.pb.cc \ @@ -3619,7 +3652,7 @@ $(OBJ_DIR)/constraint_solver/routing_parameters.pb.$O: $(GEN_DIR)/ortools/constr $(GEN_DIR)/ortools/constraint_solver/search_limit.pb.cc: \ $(SRC_DIR)/ortools/constraint_solver/search_limit.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/search_limit.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/search_limit.proto $(GEN_DIR)/ortools/constraint_solver/search_limit.pb.h: $(GEN_DIR)/ortools/constraint_solver/search_limit.pb.cc \ @@ -3628,7 +3661,7 @@ $(OBJ_DIR)/constraint_solver/search_limit.pb.$O: $(GEN_DIR)/ortools/constraint_s $(GEN_DIR)/ortools/constraint_solver/solver_parameters.pb.cc: \ $(SRC_DIR)/ortools/constraint_solver/solver_parameters.proto - $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_PROTOC_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/solver_parameters.proto + $(PROTOBUF_DIR)/bin/protoc --proto_path=$(INC_DIR) $(PROTOBUF_INC) --cpp_out=$(GEN_DIR) $(SRC_DIR)/ortools/constraint_solver/solver_parameters.proto $(GEN_DIR)/ortools/constraint_solver/solver_parameters.pb.h: $(GEN_DIR)/ortools/constraint_solver/solver_parameters.pb.cc \ diff --git a/ortools/flatzinc/parser.tab.cc b/ortools/flatzinc/parser.tab.cc index b703cb3aa5..f807dc6ec6 100644 --- a/ortools/flatzinc/parser.tab.cc +++ b/ortools/flatzinc/parser.tab.cc @@ -1,3 +1,16 @@ +// Copyright 2010-2017 Google +// 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. + /* A Bison parser, made by GNU Bison 3.0.4. */ /* Bison implementation for Yacc-like parsers in C diff --git a/ortools/flatzinc/parser.yy.cc b/ortools/flatzinc/parser.yy.cc index 3f43cc092e..cf3dd4c73f 100644 --- a/ortools/flatzinc/parser.yy.cc +++ b/ortools/flatzinc/parser.yy.cc @@ -1,3 +1,16 @@ +// Copyright 2010-2017 Google +// 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. + #line 2 "./ortools/flatzinc/parser.yy.cc" #line 4 "./ortools/flatzinc/parser.yy.cc" diff --git a/ortools/flatzinc/presolve.cc b/ortools/flatzinc/presolve.cc index e561a62135..ffb3314643 100644 --- a/ortools/flatzinc/presolve.cc +++ b/ortools/flatzinc/presolve.cc @@ -146,6 +146,16 @@ bool OverlapsAt(const Argument& array, int pos, const Argument& other) { return false; } } + +template +void AppendIfNotInSet(T* value, std::unordered_set* s, + std::vector* vec) { + if (s->insert(value).second) { + vec->push_back(value); + } + DCHECK_EQ(s->size(), vec->size()); +} + } // namespace // For the author's reference, here is an indicative list of presolve rules @@ -187,7 +197,7 @@ void Presolver::ApplyRule( } case CONSTRAINT_REWRITTEN: { AddConstraintToMapping(ct); - changed_constraints_.insert(ct); + AppendIfNotInSet(ct, &changed_constraints_, &changed_constraints_vector_); if (HASVLOG) { const std::string after = ct->DebugString(); if (after != before) { @@ -212,7 +222,7 @@ void Presolver::ApplyRule( } void Presolver::MarkChangedVariable(IntegerVariable* var) { - changed_variables_.insert(var); + AppendIfNotInSet(var, &changed_variables_, &changed_variables_vector_); } void Presolver::AddConstraintToMapping(Constraint* ct) { @@ -1540,7 +1550,7 @@ Presolver::RuleStatus Presolver::PropagatePositiveLinear(Constraint* ct, IntegerVariable* const var = ct->arguments[1].variables[i]; const int64 bound = rhs / coef; if (bound < var->domain.Max()) { - StringAppendF(log, + absl::StrAppendFormat(log, ", intersect %s with [0..%" GG_LL_FORMAT "d]", var->DebugString().c_str(), bound); IntersectVarWithInterval(var, 0, bound); @@ -1554,7 +1564,7 @@ Presolver::RuleStatus Presolver::PropagatePositiveLinear(Constraint* ct, IntegerVariable* const var = ct->arguments[1].variables[0]; const int64 bound = (rhs + coef - 1) / coef; if (bound > var->domain.Min()) { - StringAppendF( + absl::StrAppendFormat( log, ", intersect %s with [%" GG_LL_FORMAT "d .. INT_MAX]", var->DebugString().c_str(), bound); IntersectVarWithInterval(var, bound, kint64max); @@ -3362,7 +3372,7 @@ bool Presolver::Run(Model* model) { << model->constraints().size() << " constraints." << FZENDL; for (Constraint* const ct : model->constraints()) { if (ct->active) { - changed_constraints_.erase(ct); // Optim: remove from postponed queue. + // TODO(user): Optim: remove from postponed queue. PresolveOneConstraint(ct); if (!ct->active || ct->type == "false_constraint") { changed_since_start = true; @@ -3383,27 +3393,32 @@ bool Presolver::Run(Model* model) { FZVLOG << "--- loop " << loops << FZENDL; changed_since_start = true; std::unordered_set to_scan; + std::vector to_scan_vector; - for (IntegerVariable* var : changed_variables_) { + for (IntegerVariable* var : changed_variables_vector_) { for (Constraint* ct : var_to_constraints_[var]) { if (ct->active) { - to_scan.insert(ct); + AppendIfNotInSet(ct, &to_scan, &to_scan_vector); } } } - for (Constraint* ct : changed_constraints_) { + for (Constraint* ct : changed_constraints_vector_) { if (ct->active) { - to_scan.insert(ct); + AppendIfNotInSet(ct, &to_scan, &to_scan_vector); } } changed_variables_.clear(); changed_constraints_.clear(); + changed_variables_vector_.clear(); + changed_constraints_vector_.clear(); + var_representative_map_.clear(); FZVLOG << " - processing " << to_scan.size() << " constraints" << FZENDL; - for (Constraint* const ct : to_scan) { + for (Constraint* const ct : to_scan_vector) { if (!var_representative_map_.empty()) { - changed_constraints_.insert(ct); // Carry over to next round. + AppendIfNotInSet(ct, &changed_constraints_, + &changed_constraints_vector_); } else if (ct->active) { PresolveOneConstraint(ct); } diff --git a/ortools/flatzinc/presolve.h b/ortools/flatzinc/presolve.h index 8f8675008d..9c331099bb 100644 --- a/ortools/flatzinc/presolve.h +++ b/ortools/flatzinc/presolve.h @@ -233,7 +233,9 @@ class Presolver { // Store changed objects. std::unordered_set changed_variables_; + std::vector changed_variables_vector_; std::unordered_set changed_constraints_; + std::vector changed_constraints_vector_; }; } // namespace fz } // namespace operations_research diff --git a/ortools/glop/revised_simplex.cc b/ortools/glop/revised_simplex.cc index e554a450ea..141f21f979 100644 --- a/ortools/glop/revised_simplex.cc +++ b/ortools/glop/revised_simplex.cc @@ -485,20 +485,6 @@ VariableStatus RevisedSimplex::ComputeDefaultVariableStatus( return VariableStatus::FREE; } - // Special case for singleton column so UseSingletonColumnInInitialBasis() - // works better. We set the initial value of a boxed variable to its bound - // that minimizes the cost. - if (parameters_.exploit_singleton_column_in_initial_basis() && - matrix_with_slack_.column(col).num_entries() == 1) { - const Fractional objective = objective_[col]; - if (objective > 0 && IsFinite(lower_bound_[col])) { - return VariableStatus::AT_LOWER_BOUND; - } - if (objective < 0 && IsFinite(upper_bound_[col])) { - return VariableStatus::AT_UPPER_BOUND; - } - } - // Returns the bound with the lowest magnitude. Note that it must be finite // because the VariableStatus::FREE case was tested earlier. DCHECK(IsFinite(lower_bound_[col]) || IsFinite(upper_bound_[col])); @@ -954,7 +940,26 @@ Status RevisedSimplex::CreateInitialBasis() { // If possible, for the primal simplex we replace some slack variables with // some singleton columns present in the problem. - if (!parameters_.use_dual_simplex()) { + if (!parameters_.use_dual_simplex() && + parameters_.exploit_singleton_column_in_initial_basis()) { + // For UseSingletonColumnInInitialBasis() to work better, we change + // the value of the boxed singleton column with a non-zero cost to the best + // of their two bounds. + for (ColIndex col(0); col < num_cols_; ++col) { + if (matrix_with_slack_.column(col).num_entries() != 1) continue; + const VariableStatus status = variables_info_.GetStatusRow()[col]; + const Fractional objective = objective_[col]; + if (objective > 0 && IsFinite(lower_bound_[col]) && + status == VariableStatus::AT_UPPER_BOUND) { + SetNonBasicVariableStatusAndDeriveValue(col, + VariableStatus::AT_LOWER_BOUND); + } else if (objective < 0 && IsFinite(upper_bound_[col]) && + status == VariableStatus::AT_LOWER_BOUND) { + SetNonBasicVariableStatusAndDeriveValue(col, + VariableStatus::AT_UPPER_BOUND); + } + } + // Compute the primal infeasibility of the initial variable values in // error_. ComputeVariableValuesError(); @@ -965,15 +970,13 @@ Status RevisedSimplex::CreateInitialBasis() { // - At the end of phase I, restore the slack variable bounds and perform // the same algorithm to start with feasible and "optimal" values of the // singleton columns. - if (parameters_.exploit_singleton_column_in_initial_basis()) { - basis.assign(num_rows_, kInvalidCol); - UseSingletonColumnInInitialBasis(&basis); + basis.assign(num_rows_, kInvalidCol); + UseSingletonColumnInInitialBasis(&basis); - // Eventually complete the basis with fixed slack columns. - for (RowIndex row(0); row < num_rows_; ++row) { - if (basis[row] == kInvalidCol) { - basis[row] = SlackColIndex(row); - } + // Eventually complete the basis with fixed slack columns. + for (RowIndex row(0); row < num_rows_; ++row) { + if (basis[row] == kInvalidCol) { + basis[row] = SlackColIndex(row); } } } diff --git a/ortools/linear_solver/linear_solver.cc b/ortools/linear_solver/linear_solver.cc index 7b4aab6f0e..fbf9000a6d 100644 --- a/ortools/linear_solver/linear_solver.cc +++ b/ortools/linear_solver/linear_solver.cc @@ -68,7 +68,6 @@ DEFINE_bool(mpsolver_bypass_model_validation, false, // operations_research namespace in open_source/base). namespace operations_research { - double MPConstraint::GetCoefficient(const MPVariable* const var) const { DLOG_IF(DFATAL, !interface_->solver_->OwnsVariable(var)) << var; if (var == nullptr) return 0.0; diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 393adf3385..9618cce534 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -258,8 +258,8 @@ void LiteralWatchers::Attach(SatClause* clause, Trail* trail) { void LiteralWatchers::InternalDetach(SatClause* clause) { --num_watched_clauses_; const size_t size = clause->Size(); - if (drat_writer_ != nullptr && size > 2) { - drat_writer_->DeleteClause({clause->begin(), size}); + if (drat_proof_handler_ != nullptr && size > 2) { + drat_proof_handler_->DeleteClause({clause->begin(), size}); } clauses_info_.erase(clause); clause->LazyDetach(); diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h index b411d5f501..cfd4bccfc6 100644 --- a/ortools/sat/clause.h +++ b/ortools/sat/clause.h @@ -31,7 +31,7 @@ #include "ortools/base/int_type.h" #include "ortools/base/int_type_indexed_vector.h" #include "ortools/base/hash.h" -#include "ortools/sat/drat.h" +#include "ortools/sat/drat_proof_handler.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/bitset.h" @@ -218,7 +218,9 @@ class LiteralWatchers : public SatPropagator { // Number of clauses currently watched. int64 num_watched_clauses() const { return num_watched_clauses_; } - void SetDratWriter(DratWriter* drat_writer) { drat_writer_ = drat_writer; } + void SetDratProofHandler(DratProofHandler* drat_proof_handler) { + drat_proof_handler_ = drat_proof_handler; + } // Really basic algorithm to return a clause to try to minimize. We simply // loop over the clause that we keep forever, in creation order. This starts @@ -291,7 +293,7 @@ class LiteralWatchers : public SatPropagator { // Only contains removable clause. std::unordered_map clauses_info_; - DratWriter* drat_writer_ = nullptr; + DratProofHandler* drat_proof_handler_ = nullptr; DISALLOW_COPY_AND_ASSIGN(LiteralWatchers); }; diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 1019b891c1..d5f18012df 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -80,6 +80,15 @@ DEFINE_string( "If non-empty, a proof in DRAT format will be written to this file. " "This will only be used for pure-SAT problems."); +DEFINE_bool(drat_check, false, + "If true, a proof in DRAT format will be stored in memory and " + "checked if the problem is UNSAT. This will only be used for " + "pure-SAT problems."); + +DEFINE_double(max_drat_time_in_seconds, std::numeric_limits::infinity(), + "Maximum time in seconds to check the DRAT proof. This will only " + "be used is the drat_check flag is enabled."); + namespace operations_research { namespace sat { @@ -2014,9 +2023,19 @@ IntegerVariable AddLPConstraints(const CpModelProto& model_proto, } } + // Remove size one LP constraints, they are not useful. + const int num_extra_constraints = linear_constraints.size() - old_size; + { + int new_size = 0; + for (int i = 0; i < linear_constraints.size(); ++i) { + if (linear_constraints[i].vars.size() == 1) continue; + std::swap(linear_constraints[new_size++], linear_constraints[i]); + } + linear_constraints.resize(new_size); + } + VLOG(1) << "num_full_encoding_relaxations: " << num_full_encoding_relaxations; - VLOG(1) << "num_integer_encoding_constraints: " - << linear_constraints.size() - old_size; + VLOG(1) << "num_integer_encoding_constraints: " << num_extra_constraints; VLOG(1) << linear_constraints.size() << " constraints in the LP relaxation."; VLOG(1) << cut_generators.size() << " cuts generators."; @@ -2303,10 +2322,25 @@ CpSolverResponse SolveCpModelInternal( return response; } + model->GetOrCreate() + ->AddAllImplicationsBetweenAssociatedLiterals(); + model->GetOrCreate()->Propagate(); + + // Auto detect "at least one of" constraints in the PrecedencesPropagator. + // Note that we do that before we finish loading the problem (objective and LP + // relaxation), because propagation will be faster at this point and it should + // be enough for the purpose of this auto-detection. + const SatParameters& parameters = *(model->GetOrCreate()); + if (model->Mutable() != nullptr && + parameters.auto_detect_greater_than_at_least_one_of()) { + model->Mutable() + ->AddGreaterThanAtLeastOneOfConstraints(model); + model->GetOrCreate()->Propagate(); + } + // Create an objective variable and its associated linear constraint if // needed. IntegerVariable objective_var = kNoIntegerVariable; - const SatParameters& parameters = *(model->GetOrCreate()); if (is_real_solve && parameters.linearization_level() > 0) { // Linearize some part of the problem and register LP constraint(s). objective_var = @@ -2364,18 +2398,8 @@ CpSolverResponse SolveCpModelInternal( // Note that we do one last propagation at level zero once all the constraints // where added. - model->GetOrCreate() - ->AddAllImplicationsBetweenAssociatedLiterals(); model->GetOrCreate()->Propagate(); - // Auto detect "at least one of" constraints in the PrecedencesPropagator. - if (model->Mutable() != nullptr && - parameters.auto_detect_greater_than_at_least_one_of()) { - model->Mutable() - ->AddGreaterThanAtLeastOneOfConstraints(model); - model->GetOrCreate()->Propagate(); - } - // Probing Boolean variables. Because we don't have a good deterministic time // yet in the non-Boolean part of the problem, we disable it by default. // @@ -2501,9 +2525,16 @@ CpSolverResponse SolveCpModelInternal( next_decision, solution_observer, model); } } else { + if (parameters.binary_search_num_conflicts() >= 0) { + RestrictObjectiveDomainWithBinarySearch(objective_var, next_decision, + solution_observer, model); + } status = MinimizeIntegerVariableWithLinearScanAndLazyEncoding( /*log_info=*/false, objective_var, next_decision, solution_observer, model); + if (num_solutions > 0 && status == SatSolver::MODEL_UNSAT) { + status = SatSolver::MODEL_SAT; + } } if (status == SatSolver::LIMIT_REACHED) { @@ -2613,14 +2644,19 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto, solver->SetParameters(parameters); model->GetOrCreate()->ResetLimitFromParameters(parameters); - // Create a DratWriter? - std::unique_ptr drat_writer; + // Create a DratProofHandler? + std::unique_ptr drat_proof_handler; #if !defined(__PORTABLE_PLATFORM__) - if (!FLAGS_drat_output.empty()) { - File* output; - CHECK_OK(file::Open(FLAGS_drat_output, "w", &output, file::Defaults())); - drat_writer.reset(new DratWriter(/*in_binary_format=*/false, output)); - solver->SetDratWriter(drat_writer.get()); + if (!FLAGS_drat_output.empty() || FLAGS_drat_check) { + if (!FLAGS_drat_output.empty()) { + File* output; + CHECK_OK(file::Open(FLAGS_drat_output, "w", &output, file::Defaults())); + drat_proof_handler.reset(new DratProofHandler( + /*in_binary_format=*/false, output, FLAGS_drat_check)); + } else { + drat_proof_handler.reset(nullptr); + } + solver->SetDratProofHandler(drat_proof_handler.get()); } #endif // __PORTABLE_PLATFORM__ @@ -2638,7 +2674,9 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto, std::vector temp; const int num_variables = model_proto.variables_size(); solver->SetNumVariables(num_variables); - if (drat_writer != nullptr) drat_writer->SetNumVariables(num_variables); + if (drat_proof_handler != nullptr) { + drat_proof_handler->SetNumVariables(num_variables); + } for (const ConstraintProto& ct : model_proto.constraints()) { switch (ct.constraint_case()) { @@ -2648,6 +2686,9 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto, for (const int ref : ct.bool_and().literals()) { const Literal b = get_literal(ref); solver->AddProblemClause({not_a, b}); + if (drat_proof_handler != nullptr) { + drat_proof_handler->AddProblemClause({not_a, b}); + } } break; } @@ -2657,6 +2698,9 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto, temp.push_back(get_literal(ref)); } solver->AddProblemClause(temp); + if (drat_proof_handler != nullptr) { + drat_proof_handler->AddProblemClause(temp); + } break; default: LOG(FATAL) << "Not supported"; @@ -2668,10 +2712,11 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto, const auto domain = ReadDomain(model_proto.variables(ref)); CHECK_EQ(domain.size(), 1); if (domain[0].start == domain[0].end) { - if (domain[0].start == 0) { - solver->AddUnitClause(get_literal(ref).Negated()); - } else { - solver->AddUnitClause(get_literal(ref)); + const Literal ref_literal = + domain[0].start == 0 ? get_literal(ref).Negated() : get_literal(ref); + solver->AddUnitClause(ref_literal); + if (drat_proof_handler != nullptr) { + drat_proof_handler->AddProblemClause({ref_literal}); } } } @@ -2681,7 +2726,7 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto, if (parameters.cp_model_presolve()) { std::vector solution; status = SolveWithPresolve(&solver, model->GetOrCreate(), - &solution, drat_writer.get()); + &solution, drat_proof_handler.get()); if (status == SatSolver::MODEL_SAT) { response.clear_solution(); for (int ref = 0; ref < num_variables; ++ref) { @@ -2727,6 +2772,35 @@ CpSolverResponse SolvePureSatModel(const CpModelProto& model_proto, response.set_user_time(user_timer.Get()); response.set_deterministic_time( model->Get()->GetElapsedDeterministicTime()); + + if (status == SatSolver::MODEL_UNSAT && drat_proof_handler != nullptr) { + wall_timer.Restart(); + user_timer.Restart(); + DratChecker::Status drat_status = + drat_proof_handler->Check(FLAGS_max_drat_time_in_seconds); + switch (drat_status) { + case DratChecker::UNKNOWN: + LOG(INFO) << "DRAT status: UNKNOWN"; + break; + case DratChecker::VALID: + LOG(INFO) << "DRAT status: VALID"; + break; + case DratChecker::INVALID: + LOG(ERROR) << "DRAT status: INVALID"; + break; + default: + // Should not happen. + break; + } + LOG(INFO) << "DRAT wall time: " << wall_timer.Get(); + LOG(INFO) << "DRAT user time: " << user_timer.Get(); + } else if (drat_proof_handler != nullptr) { + // Always log a DRAT status to make it easier to extract it from a multirun + // result with awk. + LOG(INFO) << "DRAT status: NA"; + LOG(INFO) << "DRAT wall time: NA"; + LOG(INFO) << "DRAT user time: NA"; + } return response; } diff --git a/ortools/sat/drat_checker.cc b/ortools/sat/drat_checker.cc new file mode 100644 index 0000000000..862f9bbfa9 --- /dev/null +++ b/ortools/sat/drat_checker.cc @@ -0,0 +1,609 @@ +// Copyright 2010-2017 Google +// 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. + +#include "ortools/sat/drat_checker.h" + +#include +#include +#include "ortools/base/hash.h" +#include "ortools/base/numbers.h" +#include "ortools/base/split.h" +#include "ortools/base/time_support.h" +#include "ortools/base/stl_util.h" +#include "ortools/util/time_limit.h" + +namespace operations_research { +namespace sat { + +DratChecker::Clause::Clause(int first_literal_index, int num_literals) + : first_literal_index(first_literal_index), num_literals(num_literals) {} + +std::size_t DratChecker::ClauseHash::operator()( + const ClauseIndex clause_index) const { + size_t hash = 0; + for (Literal literal : checker->Literals(checker->clauses_[clause_index])) { + hash = Hash64NumWithSeed(hash, literal.Index().value()); + } + return hash; +} + +bool DratChecker::ClauseEquiv::operator()( + const ClauseIndex clause_index1, const ClauseIndex clause_index2) const { + return checker->Literals(checker->clauses_[clause_index1]) == + checker->Literals(checker->clauses_[clause_index2]); +} + +DratChecker::DratChecker() + : first_infered_clause_index_(kNoClauseIndex), + clause_set_(0, ClauseHash(this), ClauseEquiv(this)), + num_variables_(0) {} + +bool DratChecker::Clause::IsDeleted(ClauseIndex clause_index) const { + return deleted_index <= clause_index; +} + +void DratChecker::AddProblemClause(absl::Span clause) { + DCHECK_EQ(first_infered_clause_index_, kNoClauseIndex); + const ClauseIndex clause_index = AddClause(clause); + + const auto it = clause_set_.find(clause_index); + if (it != clause_set_.end()) { + clauses_[*it].num_copies += 1; + RemoveLastClause(); + } else { + clause_set_.insert(clause_index); + } +} + +void DratChecker::AddInferedClause(absl::Span clause) { + const ClauseIndex infered_clause_index = AddClause(clause); + if (first_infered_clause_index_ == kNoClauseIndex) { + first_infered_clause_index_ = infered_clause_index; + } + + const auto it = clause_set_.find(infered_clause_index); + if (it != clause_set_.end()) { + clauses_[*it].num_copies += 1; + if (*it >= first_infered_clause_index_ && !clause.empty()) { + CHECK_EQ(clauses_[*it].rat_literal_index, clause[0].Index()); + } + RemoveLastClause(); + } else { + clauses_[infered_clause_index].rat_literal_index = + clause.empty() ? kNoLiteralIndex : clause[0].Index(); + clause_set_.insert(infered_clause_index); + } +} + +ClauseIndex DratChecker::AddClause(absl::Span clause) { + const int first_literal_index = literals_.size(); + literals_.insert(literals_.end(), clause.begin(), clause.end()); + // Sort the input clause in strictly increasing order (by sorting and then + // removing the duplicate literals). + std::sort(literals_.begin() + first_literal_index, literals_.end()); + literals_.erase( + std::unique(literals_.begin() + first_literal_index, literals_.end()), + literals_.end()); + + for (int i = first_literal_index + 1; i < literals_.size(); ++i) { + CHECK(literals_[i] != literals_[i - 1].Negated()); + } + clauses_.push_back(Clause(first_literal_index, + literals_.size() - first_literal_index)); + if (!clause.empty()) { + num_variables_ = + std::max(num_variables_, literals_.back().Variable().value() + 1); + } + return ClauseIndex(clauses_.size() - 1); +} + +void DratChecker::DeleteClause(absl::Span clause) { + // Temporarily add 'clause' to find if it has been previously added. + const auto it = clause_set_.find(AddClause(clause)); + if (it != clause_set_.end()) { + Clause& existing_clause = clauses_[*it]; + existing_clause.num_copies -= 1; + if (existing_clause.num_copies == 0) { + DCHECK(existing_clause.deleted_index == std::numeric_limits::max()); + existing_clause.deleted_index = clauses_.size() - 1; + if (clauses_.back().num_literals >= 2) { + clauses_[ClauseIndex(clauses_.size() - 2)].deleted_clauses.push_back( + *it); + } + clause_set_.erase(it); + } + } else { + LOG(WARNING) << "Couldn't find deleted clause"; + } + // Delete 'clause' and its literals. + RemoveLastClause(); +} + +void DratChecker::RemoveLastClause() { + literals_.resize(clauses_.back().first_literal_index); + clauses_.pop_back(); +} + +// See Algorithm of Fig. 8 in 'Trimming while Checking Clausal Proofs'. +DratChecker::Status DratChecker::Check(double max_time_in_seconds) { + // First check that the last infered clause is empty (this implies there + // should be at least one infered clause), and mark it as needed for the + // proof. + if (clauses_.empty() || first_infered_clause_index_ == kNoClauseIndex || + clauses_.back().num_literals != 0) { + return Status::INVALID; + } + clauses_.back().is_needed_for_proof = true; + + // Checks the infered clauses in reversed order. The advantage of this order + // is that when checking a clause, one can mark all the clauses that are used + // to check it. In turn, only these marked clauses need to be checked (and so + // on recursively). By contrast, a forward iteration needs to check all the + // clauses. + const int64 start_time_nanos = absl::GetCurrentTimeNanos(); + TimeLimit time_limit(max_time_in_seconds); + Init(); + for (ClauseIndex i(clauses_.size() - 1); i >= first_infered_clause_index_; + --i) { + if (time_limit.LimitReached()) { + return Status::UNKNOWN; + } + const Clause& clause = clauses_[i]; + // Start watching the literals of the clauses that were deleted just after + // this one, and which are now no longer deleted. + for (const ClauseIndex j : clause.deleted_clauses) { + WatchClause(j); + } + if (!clause.is_needed_for_proof) { + continue; + } + // 'clause' must have either the Reverse Unit Propagation (RUP) property: + if (HasRupProperty(i, Literals(clause))) { + continue; + } + // or the Reverse Asymetric Tautology (RAT) property. This property is + // defined by the fact that all clauses which contain the negation of + // the RAT literal of 'clause', after resolution with 'clause', must have + // the RUP property. + // Note from 'DRAT-trim: Efficient Checking and Trimming Using Expressive + // Clausal Proofs': "[in order] to access to all clauses containing the + // negation of the resolution literal, one could build a literal-to-clause + // lookup table of the original formula and update it after each lemma + // addition and deletion step. However, these updates can be expensive and + // the lookup table potentially doubles the memory usage of the tool. + // Since most lemmas emitted by state-of-the-art SAT solvers can be + // validated using the RUP check, such a lookup table has been omitted." + if (clause.rat_literal_index == kNoLiteralIndex) return Status::INVALID; + ++num_rat_checks_; + std::vector resolvent; + for (ClauseIndex j(0); j < i; ++j) { + if (!clauses_[j].IsDeleted(i) && + ContainsLiteral(Literals(clauses_[j]), + Literal(clause.rat_literal_index).Negated())) { + // Check that the resolvent has the RUP property. + if (!Resolve(Literals(clause), Literals(clauses_[j]), + Literal(clause.rat_literal_index), &tmp_assignment_, + &resolvent) || + !HasRupProperty(i, resolvent)) { + return Status::INVALID; + } + } + } + } + LogStatistics(absl::GetCurrentTimeNanos() - start_time_nanos); + return Status::VALID; +} + +std::vector> DratChecker::GetUnsatSubProblem() const { + return GetClausesNeededForProof(ClauseIndex(0), first_infered_clause_index_); +} + +std::vector> DratChecker::GetOptimizedProof() const { + return GetClausesNeededForProof(first_infered_clause_index_, + ClauseIndex(clauses_.size())); +} + +std::vector> DratChecker::GetClausesNeededForProof( + ClauseIndex begin, ClauseIndex end) const { + std::vector> result; + for (ClauseIndex i = begin; i < end; ++i) { + const Clause& clause = clauses_[i]; + if (clause.is_needed_for_proof) { + const absl::Span& literals = Literals(clause); + result.emplace_back(literals.begin(), literals.end()); + if (clause.rat_literal_index != kNoLiteralIndex) { + const int rat_literal_clause_index = + std::find(literals.begin(), literals.end(), + Literal(clause.rat_literal_index)) - + literals.begin(); + std::swap(result.back()[0], result.back()[rat_literal_clause_index]); + } + } + } + return result; +} + +absl::Span DratChecker::Literals(const Clause& clause) const { + return absl::Span( + literals_.data() + clause.first_literal_index, clause.num_literals); +} + +void DratChecker::Init() { + assigned_.clear(); + assignment_.Resize(num_variables_); + assignment_source_.resize(num_variables_, kNoClauseIndex); + high_priority_literals_to_assign_.clear(); + low_priority_literals_to_assign_.clear(); + watched_literals_.clear(); + watched_literals_.resize(2 * num_variables_); + single_literal_clauses_.clear(); + unit_stack_.clear(); + tmp_assignment_.Resize(num_variables_); + num_rat_checks_ = 0; + + for (ClauseIndex clause_index(0); clause_index < clauses_.size(); + ++clause_index) { + Clause& clause = clauses_[clause_index]; + if (clause.num_literals >= 2) { + // Don't watch the literals of the deleted clauses right away, instead + // watch them when these clauses become 'undeleted' in backward checking. + if (clause.deleted_index == std::numeric_limits::max()) { + WatchClause(clause_index); + } + } else if (clause.num_literals == 1) { + single_literal_clauses_.push_back(clause_index); + } + } +} + +void DratChecker::WatchClause(ClauseIndex clause_index) { + const Literal* clause_literals = + literals_.data() + clauses_[clause_index].first_literal_index; + watched_literals_[clause_literals[0].Index()].push_back(clause_index); + watched_literals_[clause_literals[1].Index()].push_back(clause_index); +} + +bool DratChecker::HasRupProperty(ClauseIndex num_clauses, + absl::Span clause) { + ClauseIndex conflict = kNoClauseIndex; + for (const Literal literal : clause) { + conflict = + AssignAndPropagate(num_clauses, literal.Negated(), kNoClauseIndex); + if (conflict != kNoClauseIndex) { + break; + } + } + + for (const ClauseIndex clause_index : single_literal_clauses_) { + const Clause& clause = clauses_[clause_index]; + // TODO(user): consider ignoring the deletion of single literal clauses + // as done in drat-trim. + if (clause_index < num_clauses && !clause.IsDeleted(num_clauses)) { + if (clause.is_needed_for_proof) { + high_priority_literals_to_assign_.push_back( + {literals_[clause.first_literal_index], clause_index}); + } else { + low_priority_literals_to_assign_.push_back( + {literals_[clause.first_literal_index], clause_index}); + } + } + } + + while (!(high_priority_literals_to_assign_.empty() && + low_priority_literals_to_assign_.empty()) && + conflict == kNoClauseIndex) { + std::vector& stack = + high_priority_literals_to_assign_.empty() + ? low_priority_literals_to_assign_ + : high_priority_literals_to_assign_; + const LiteralToAssign literal_to_assign = stack.back(); + stack.pop_back(); + if (assignment_.LiteralIsAssigned(literal_to_assign.literal)) { + // If the literal to assign to true is already assigned to false, we found + // a conflict, with the source clause of this previous assignment. + if (assignment_.LiteralIsFalse(literal_to_assign.literal)) { + conflict = literal_to_assign.source_clause_index; + break; + } else { + continue; + } + } + DCHECK(literal_to_assign.source_clause_index != kNoClauseIndex); + unit_stack_.push_back(literal_to_assign.source_clause_index); + conflict = AssignAndPropagate(num_clauses, literal_to_assign.literal, + literal_to_assign.source_clause_index); + } + if (conflict != kNoClauseIndex) { + MarkAsNeededForProof(&clauses_[conflict]); + } + + for (const Literal literal : assigned_) { + assignment_.UnassignLiteral(literal); + } + assigned_.clear(); + high_priority_literals_to_assign_.clear(); + low_priority_literals_to_assign_.clear(); + unit_stack_.clear(); + + return conflict != kNoClauseIndex; +} + +ClauseIndex DratChecker::AssignAndPropagate(ClauseIndex num_clauses, + Literal literal, + ClauseIndex source_clause_index) { + assigned_.push_back(literal); + assignment_.AssignFromTrueLiteral(literal); + assignment_source_[literal.Variable()] = source_clause_index; + + const Literal false_literal = literal.Negated(); + std::vector& watched = watched_literals_[false_literal.Index()]; + int new_watched_size = 0; + ClauseIndex conflict_index = kNoClauseIndex; + for (const ClauseIndex clause_index : watched) { + if (clause_index >= num_clauses) { + // Stop watching the literals of clauses which cannot possibly be + // necessary to check the rest of the proof. + continue; + } + Clause& clause = clauses_[clause_index]; + DCHECK(!clause.IsDeleted(num_clauses)); + if (conflict_index != kNoClauseIndex) { + watched[new_watched_size++] = clause_index; + continue; + } + + Literal* clause_literals = literals_.data() + clause.first_literal_index; + const Literal other_watched_literal(LiteralIndex( + clause_literals[0].Index().value() ^ + clause_literals[1].Index().value() ^ false_literal.Index().value())); + if (assignment_.LiteralIsTrue(other_watched_literal)) { + watched[new_watched_size++] = clause_index; + continue; + } + + bool new_watched_literal_found = false; + for (int i = 2; i < clause.num_literals; ++i) { + if (!assignment_.LiteralIsFalse(clause_literals[i])) { + clause_literals[0] = other_watched_literal; + clause_literals[1] = clause_literals[i]; + clause_literals[i] = false_literal; + watched_literals_[clause_literals[1].Index()].push_back(clause_index); + new_watched_literal_found = true; + break; + } + } + + if (!new_watched_literal_found) { + if (assignment_.LiteralIsFalse(other_watched_literal)) { + // 'clause' is falsified with 'assignment_', we found a conflict. + // TODO(user): test moving the rest of the vector here and + // returning right away. + conflict_index = clause_index; + } else { + DCHECK(!assignment_.LiteralIsAssigned(other_watched_literal)); + // 'clause' is unit, push its unit literal on + // 'literals_to_assign_high_priority' or + // 'literals_to_assign_low_priority' to assign it to true and propagate + // it in a later call to AssignAndPropagate(). + if (clause.is_needed_for_proof) { + high_priority_literals_to_assign_.push_back( + {other_watched_literal, clause_index}); + } else { + low_priority_literals_to_assign_.push_back( + {other_watched_literal, clause_index}); + } + } + watched[new_watched_size++] = clause_index; + } + } + watched.resize(new_watched_size); + return conflict_index; +} + +void DratChecker::MarkAsNeededForProof(Clause* clause) { + const auto mark_clause_and_sources = [&](Clause* clause) { + clause->is_needed_for_proof = true; + for (const Literal literal : Literals(*clause)) { + const ClauseIndex source_clause_index = + assignment_source_[literal.Variable()]; + if (source_clause_index != kNoClauseIndex) { + clauses_[source_clause_index].tmp_is_needed_for_proof_step = true; + } + } + }; + mark_clause_and_sources(clause); + for (int i = unit_stack_.size() - 1; i >= 0; --i) { + Clause& unit_clause = clauses_[unit_stack_[i]]; + if (unit_clause.tmp_is_needed_for_proof_step) { + mark_clause_and_sources(&unit_clause); + // We can clean this flag here without risking missing clauses needed for + // the proof, because the clauses needed for a clause C are always lower + // than C in the stack. + unit_clause.tmp_is_needed_for_proof_step = false; + } + } +} + +void DratChecker::LogStatistics(int64 duration_nanos) const { + int problem_clauses_needed_for_proof = 0; + int infered_clauses_needed_for_proof = 0; + for (ClauseIndex i(0); i < clauses_.size(); ++i) { + if (clauses_[i].is_needed_for_proof) { + if (i < first_infered_clause_index_) { + ++problem_clauses_needed_for_proof; + } else { + ++infered_clauses_needed_for_proof; + } + } + } + LOG(INFO) << problem_clauses_needed_for_proof + << " problem clauses needed for proof, out of " + << first_infered_clause_index_; + LOG(INFO) << infered_clauses_needed_for_proof + << " infered clauses needed for proof, out of " + << clauses_.size() - first_infered_clause_index_; + LOG(INFO) << num_rat_checks_ << " RAT infered clauses"; + LOG(INFO) << "verification time: " << 1e-9 * duration_nanos << " s"; +} + +bool ContainsLiteral(absl::Span clause, Literal literal) { + return std::find(clause.begin(), clause.end(), literal) != clause.end(); +} + +bool Resolve(absl::Span clause, + absl::Span other_clause, + Literal complementary_literal, VariablesAssignment* assignment, + std::vector* resolvent) { + DCHECK(ContainsLiteral(clause, complementary_literal)); + DCHECK(ContainsLiteral(other_clause, complementary_literal.Negated())); + resolvent->clear(); + + for (const Literal literal : clause) { + if (literal != complementary_literal) { + // Temporary assignment used to do the checks below in linear time. + assignment->AssignFromTrueLiteral(literal); + resolvent->push_back(literal); + } + } + + bool result = true; + for (const Literal other_literal : other_clause) { + if (other_literal != complementary_literal.Negated()) { + if (assignment->LiteralIsFalse(other_literal)) { + result = false; + break; + } else if (!assignment->LiteralIsAssigned(other_literal)) { + resolvent->push_back(other_literal); + } + } + } + + // Revert the temporary assignment done above. + for (const Literal literal : clause) { + if (literal != complementary_literal) { + assignment->UnassignLiteral(literal); + } + } + return result; +} + +bool AddProblemClauses(const std::string& file_path, + DratChecker* drat_checker) { + int line_number = 0; + int num_variables = 0; + int num_clauses = 0; + std::vector literals; + std::ifstream file(file_path); + std::string line; + bool result = true; + while (std::getline(file, line)) { + line_number++; + std::vector words = + absl::StrSplit(line, absl::delimiter::AnyOf(" \t"), absl::SkipEmpty()); + if (words.empty() || words[0] == "c") { + // Ignore empty and comment lines. + continue; + } + if (words[0] == "p") { + if (num_clauses > 0 || words.size() != 4 || words[1] != "cnf" || + !strings::safe_strto32(words[2], &num_variables) || num_variables <= 0 || + !strings::safe_strto32(words[3], &num_clauses) || num_clauses <= 0) { + LOG(ERROR) << "Invalid content '" << line << "' at line " << line_number + << " of " << file_path; + result = false; + break; + } + continue; + } + literals.clear(); + for (int i = 0; i < words.size(); ++i) { + int signed_value; + if (!strings::safe_strto32(words[i], &signed_value) || + std::abs(signed_value) > num_variables || + (signed_value == 0 && i != words.size() - 1)) { + LOG(ERROR) << "Invalid content '" << line << "' at line " << line_number + << " of " << file_path; + result = false; + break; + } + if (signed_value != 0) { + literals.push_back(Literal(signed_value)); + } + } + drat_checker->AddProblemClause(literals); + } + file.close(); + return result; +} + +bool AddInferedAndDeletedClauses(const std::string& file_path, + DratChecker* drat_checker) { + int line_number = 0; + bool ends_with_empty_clause = false; + std::vector literals; + std::ifstream file(file_path); + std::string line; + bool result = true; + while (std::getline(file, line)) { + line_number++; + std::vector words = + absl::StrSplit(line, absl::delimiter::AnyOf(" \t"), absl::SkipEmpty()); + bool delete_clause = !words.empty() && words[0] == "d"; + literals.clear(); + for (int i = (delete_clause ? 1 : 0); i < words.size(); ++i) { + int signed_value; + if (!strings::safe_strto32(words[i], &signed_value) || + (signed_value == 0 && i != words.size() - 1)) { + LOG(ERROR) << "Invalid content '" << line << "' at line " << line_number + << " of " << file_path; + result = false; + break; + } + if (signed_value != 0) { + literals.push_back(Literal(signed_value)); + } + } + if (delete_clause) { + drat_checker->DeleteClause(literals); + ends_with_empty_clause = false; + } else { + drat_checker->AddInferedClause(literals); + ends_with_empty_clause = literals.empty(); + } + } + if (!ends_with_empty_clause) { + drat_checker->AddInferedClause({}); + } + file.close(); + return result; +} + +bool PrintClauses(const std::string& file_path, SatFormat format, + const std::vector>& clauses, + int num_variables) { + std::ofstream output_stream(file_path, std::ofstream::out); + if (format == DIMACS) { + output_stream << "p cnf " << num_variables << " " << clauses.size() << "\n"; + } + for (const auto& clause : clauses) { + for (Literal literal : clause) { + output_stream << literal.SignedValue() << " "; + } + output_stream << "0\n"; + } + output_stream.close(); + return output_stream.good(); +} + +} // namespace sat +} // namespace operations_research diff --git a/ortools/sat/drat_checker.h b/ortools/sat/drat_checker.h new file mode 100644 index 0000000000..b4fe02f6a9 --- /dev/null +++ b/ortools/sat/drat_checker.h @@ -0,0 +1,340 @@ +// Copyright 2010-2017 Google +// 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. + +#ifndef OR_TOOLS_SAT_DRAT_CHECKER_H_ +#define OR_TOOLS_SAT_DRAT_CHECKER_H_ + +#include +#include + +#include "ortools/base/span.h" +#include +#include "ortools/base/int_type.h" +#include "ortools/base/int_type_indexed_vector.h" +#include "ortools/sat/sat_base.h" + +namespace operations_research { +namespace sat { + +// Index of a clause (>= 0). +DEFINE_INT_TYPE(ClauseIndex, int); +const ClauseIndex kNoClauseIndex(-1); + +// DRAT is a SAT proof format that allows a simple program to check that a +// problem is really UNSAT. The description of the format and a checker are +// available at http://www.cs.utexas.edu/~marijn/drat-trim/. This class checks +// that a DRAT proof is valid. +// +// Note that DRAT proofs are often huge (can be GB), and can take about as much +// time to check as it takes to find the proof in the first place! +class DratChecker { + public: + DratChecker(); + ~DratChecker() {} + + // Returns the number of Boolean variables used in the problem and infered + // clauses. + int num_variables() const { return num_variables_; } + + // Adds a clause of the problem that must be checked. The problem clauses must + // be added first, before any infered clause. The given clause must not + // contain a literal and its negation. Must not be called after Check(). + void AddProblemClause(absl::Span clause); + + // Adds a clause which is infered from the problem clauses and the previously + // infered clauses (that are have not been deleted). Infered clauses must be + // added after the problem clauses. Clauses with the Reverse Asymetric + // Tautology (RAT) property for literal l must start with this literal. The + // given clause must not contain a literal and its negation. Must not be + // called after Check(). + void AddInferedClause(absl::Span clause); + + // Deletes a problem or infered clause. The order of the literals does not + // matter. In particular, it can be different from the order that was used + // when the clause was added. Must not be called after Check(). + void DeleteClause(absl::Span clause); + + // Checks that the infered clauses form a DRAT proof that the problem clauses + // are UNSAT. For this the last added infered clause must be the empty clause + // and each infered clause must have either the Reverse Unit Propagation (RUP) + // or the Reverse Asymetric Tautology (RAT) property with respect to the + // problem clauses and the previously infered clauses which are not deleted. + // Returns VALID if the proof is valid, INVALID if it is not, and UNKNOWN if + // the check timed out. + // WARNING: no new clause must be added or deleted after this method has been + // called. + enum Status { + UNKNOWN, + VALID, + INVALID, + }; + Status Check(double max_time_in_seconds); + + // Returns a subproblem of the original problem that is already UNSAT. The + // result is undefined if Check() was not previously called, or did not return + // true. + std::vector> GetUnsatSubProblem() const; + + // Returns a DRAT proof that GetUnsatSubProblem() is UNSAT. The result is + // undefined if Check() was not previously called, or did not return true. + std::vector> GetOptimizedProof() const; + + private: + // A problem or infered clause. The literals are specified as a subrange of + // 'literals_' (namely the subrange from 'first_literal_index' to + // 'first_literal_index' + 'num_literals' - 1), and are sorted in increasing + // order *before Check() is called*. + struct Clause { + // The index of the first literal of this clause in 'literals_'. + int first_literal_index; + // The number of literals of this clause. + int num_literals; + + // The clause literal to use to check the RAT property, or kNoLiteralIndex + // for problem clauses and empty infered clauses. + LiteralIndex rat_literal_index = kNoLiteralIndex; + + // The *current* number of copies of this clause. This number is incremented + // each time a copy of the clause is added, and decremented each time a copy + // is deleted. When this number reaches 0, the clause is actually marked as + // deleted (see 'deleted_index'). If other copies are added after this + // number reached 0, a new clause is added (because a Clause lifetime is a + // single interval of ClauseIndex values; therefore, in order to represent a + // lifetime made of several intervals, several Clause are used). + int num_copies = 1; + + // The index in 'clauses_' from which this clause is deleted (inclusive). + // For instance, with AddProblemClause(c0), AddProblemClause(c1), + // DeleteClause(c0), AddProblemClause(c2), ... if c0's index is 0, then its + // deleted_index is 2. Meaning that when checking a clause whose index is + // larger than or equal to 2 (e.g. c2), c0 can be ignored. + ClauseIndex deleted_index = ClauseIndex(std::numeric_limits::max()); + + // The indices of the clauses (with at least two literals) which are deleted + // just after this clause. + std::vector deleted_clauses; + + // Whether this clause is actually needed to check the DRAT proof. + bool is_needed_for_proof = false; + // Whether this clause is actually needed to check the current step (i.e. an + // infered clause) of the DRAT proof. This bool is always false, except in + // MarkAsNeededForProof() that uses it temporarily. + bool tmp_is_needed_for_proof_step = false; + + Clause(int first_literal_index, int num_literals); + + // Returns true if this clause is deleted before the given clause. + bool IsDeleted(ClauseIndex clause_index) const; + }; + + // A literal to assign to true during boolean constraint propagation. When a + // literal is assigned, new literals can be found that also need to be + // assigned to true (via unit clauses). In this case they are pushed on a + // stack of LiteralToAssign values, to be processed later on (the use of this + // stack avoids recursive calls to the boolean constraint propagation method + // AssignAndPropagate()). + struct LiteralToAssign { + // The literal that must be assigned to true. + Literal literal; + // The index of the clause from which this assignment was deduced. This is + // kNoClauseIndex for the clause we are currently checking (whose literals + // are all falsified to check if a conflict can be derived). Otherwise this + // is the index of a unit clause with unit literal 'literal' that was found + // during boolean constraint propagation. + ClauseIndex source_clause_index; + }; + + // Hash function for clauses. + struct ClauseHash { + DratChecker* checker; + explicit ClauseHash(DratChecker* checker) : checker(checker) {} + std::size_t operator()(const ClauseIndex clause_index) const; + }; + + // Equality function for clauses. + struct ClauseEquiv { + DratChecker* checker; + explicit ClauseEquiv(DratChecker* checker) : checker(checker) {} + bool operator()(const ClauseIndex clause_index1, + const ClauseIndex clause_index2) const; + }; + + // Adds a clause and returns its index. + ClauseIndex AddClause(absl::Span clause); + + // Removes the last clause added to 'clauses_'. + void RemoveLastClause(); + + // Returns the literals of the given clause in increasing order. + absl::Span Literals(const Clause& clause) const; + + // Initializes the data structures used to check the DRAT proof. + void Init(); + + // Adds 2 watch literals for the given clause. + void WatchClause(ClauseIndex clause_index); + + // Returns true if, by assigning all the literals of 'clause' to false, a + // conflict can be found with boolean constraint propagation, using the non + // deleted clauses whose index is strictly less than 'num_clauses'. If so, + // marks the clauses actually used in this process as needed to check to DRAT + // proof. + bool HasRupProperty(ClauseIndex num_clauses, + absl::Span clause); + + // Assigns 'literal' to true in 'assignment_' (and pushes it to 'assigned_'), + // records its source clause 'source_clause_index' in 'assignment_source_', + // and uses the watched literals to find all the clauses (whose index is less + // than 'num_clauses') that become unit due to this assignment. For each unit + // clause found, pushes its unit literal on top of + // 'high_priority_literals_to_assign_' or 'low_priority_literals_to_assign_'. + // Returns kNoClauseIndex if no falsified clause is found, or the index of the + // first found falsified clause otherwise. + ClauseIndex AssignAndPropagate(ClauseIndex num_clauses, Literal literal, + ClauseIndex source_clause_index); + + // Marks the given clause as needed to check the DRAT proof, as well as the + // other clauses which where used to check this clause (these are found from + // 'unit_stack_', containing the clauses that became unit in + // AssignAndPropagate, and from 'assignment_source_', containing for each + // variable the clause that caused its assignment). + void MarkAsNeededForProof(Clause* clause); + + // Returns the clauses whose index is in [begin,end) which are needed for the + // proof. The result is undefined if Check() was not previously called, or did + // not return true. + std::vector> GetClausesNeededForProof( + ClauseIndex begin, ClauseIndex end) const; + + void LogStatistics(int64 duration_nanos) const; + + // The index of the first infered clause in 'clauses_', or kNoClauseIndex if + // there is no infered clause. + ClauseIndex first_infered_clause_index_; + + // The problem clauses, followed by the infered clauses. + ITIVector clauses_; + + // A content addressable set of the non-deleted clauses in clauses_. After + // adding a clause to clauses_, this set can be used to find if the same + // clause was previously added (i.e if a find using the new clause index + // returns a previous index) and not yet deleted. + std::unordered_set clause_set_; + + // All the literals used in 'clauses_'. + std::vector literals_; + + // The number of Boolean variables used in the clauses. + int num_variables_; + + // --------------------------------------------------------------------------- + // Data initialized in Init() and used in Check() to check the DRAT proof. + + // The literals that have been assigned so far (this is used to unassign them + // after a clause has been checked, before checking the next one). + std::vector assigned_; + + // The current assignment values of literals_. + VariablesAssignment assignment_; + + // For each variable, the index of the unit clause that caused its assignment, + // or kNoClauseIndex if the variable is not assigned, or was assigned to + // falsify the clause that is currently being checked. + ITIVector assignment_source_; + + // The stack of literals that remain to be assigned to true during boolean + // constraint propagation, with high priority (unit clauses which are already + // marked as needed for the proof are given higher priority than the others + // during boolean constraint propagation. According to 'Trimming while + // Checking Clausal Proofs', this heuristics reduces the final number of + // clauses that are marked as needed for the proof, and therefore the + // verification time, in a majority of cases -- but not all). + std::vector high_priority_literals_to_assign_; + + // The stack of literals that remain to be assigned to true during boolean + // constraint propagation, with low priority (see above). + std::vector low_priority_literals_to_assign_; + + // For each literal, the list of clauses in which this literal is watched. + // Invariant 1: the literals with indices first_watched_literal_index and + // second_watched_literal_index of each clause with at least two literals are + // watched. + // Invariant 2: watched literals are non-falsified if the clause is not + // satisfied (in more details: if a clause c is contained in + // 'watched_literals_[l]' for literal l, then either c is satisfied with + // 'assignment_', or l is unassigned or assigned to true). + ITIVector> watched_literals_; + + // The list of clauses with only one literal. This is needed for boolean + // constraint propagation, in addition to watched literals, because watched + // literals can only be used with clauses having at least two literals. + std::vector single_literal_clauses_; + + // The stack of clauses that have become unit during boolean constraint + // propagation, in HasRupProperty(). + std::vector unit_stack_; + + // A temporary assignment, always fully unassigned except in Resolve(). + VariablesAssignment tmp_assignment_; + + // --------------------------------------------------------------------------- + // Statistics + + // The number of infered clauses having the RAT property (but not the RUP + // property). + int num_rat_checks_; +}; + +// Returns true if the given clause contains the given literal. This works in +// O(clause.size()). +bool ContainsLiteral(absl::Span clause, Literal literal); + +// Returns true if 'complementary_literal' is the unique complementary literal +// in the two given clauses. If so the resolvent of these clauses (i.e. their +// union with 'complementary_literal' and its negation removed) is set in +// 'resolvent'. 'clause' must contain 'complementary_literal', while +// 'other_clause' must contain its negation. 'assignment' must have at least as +// many variables as each clause, and they must all be unassigned. They are +// still unassigned upon return. +bool Resolve(absl::Span clause, + absl::Span other_clause, + Literal complementary_literal, VariablesAssignment* assignment, + std::vector* resolvent); + +// Adds to the given drat checker the problem clauses from the file at the given +// path, which must be in DIMACS format. Returns true iff the file was +// successfully parsed. +bool AddProblemClauses(const std::string& file_path, DratChecker* drat_checker); + +// Adds to the given drat checker the infered and deleted clauses from the file +// at the given path, which must be in DRAT format. Returns true iff the file +// was successfully parsed. +bool AddInferedAndDeletedClauses(const std::string& file_path, + DratChecker* drat_checker); + +// The file formats that can be used to save a list of clauses. +enum SatFormat { + DIMACS, + DRAT, +}; + +// Prints the given clauses in the file at the given path, using the given file +// format. Returns true iff the file was successfully written. +bool PrintClauses(const std::string& file_path, SatFormat format, + const std::vector>& clauses, + int num_variables); + +} // namespace sat +} // namespace operations_research + +#endif // OR_TOOLS_SAT_DRAT_CHECKER_H_ diff --git a/ortools/sat/drat.cc b/ortools/sat/drat_proof_handler.cc similarity index 53% rename from ortools/sat/drat.cc rename to ortools/sat/drat_proof_handler.cc index b17b3f41f0..8324bf0797 100644 --- a/ortools/sat/drat.cc +++ b/ortools/sat/drat_proof_handler.cc @@ -11,32 +11,30 @@ // See the License for the specific language governing permissions and // limitations under the License. -#include "ortools/sat/drat.h" +#include "ortools/sat/drat_proof_handler.h" #include -#include -#include #include "ortools/base/logging.h" -#include "ortools/base/stringprintf.h" -#if !defined(__PORTABLE_PLATFORM__) -#endif // !__PORTABLE_PLATFORM__ +#include "ortools/base/memory.h" #include "ortools/base/int_type.h" -#include "ortools/base/status.h" namespace operations_research { namespace sat { -DratWriter::~DratWriter() { - if (output_ != nullptr) { -#if !defined(__PORTABLE_PLATFORM__) - CHECK_OK(file::WriteString(output_, buffer_, file::Defaults())); - CHECK_OK(output_->Close(file::Defaults())); -#endif // !__PORTABLE_PLATFORM__ +DratProofHandler::DratProofHandler() + : variable_index_(0), drat_checker_(new DratChecker()) {} + +DratProofHandler::DratProofHandler(bool in_binary_format, File* output, + bool check) + : variable_index_(0), + drat_writer_(new DratWriter(in_binary_format, output)) { + if (check) { + drat_checker_ = absl::make_unique(); } } -void DratWriter::ApplyMapping( +void DratProofHandler::ApplyMapping( const ITIVector& mapping) { ITIVector new_mapping; for (BooleanVariable v(0); v < mapping.size(); ++v) { @@ -53,49 +51,67 @@ void DratWriter::ApplyMapping( std::swap(new_mapping, reverse_mapping_); } -void DratWriter::SetNumVariables(int num_variables) { +void DratProofHandler::SetNumVariables(int num_variables) { CHECK_GE(num_variables, reverse_mapping_.size()); while (reverse_mapping_.size() < num_variables) { reverse_mapping_.push_back(BooleanVariable(variable_index_++)); } } -void DratWriter::AddOneVariable() { +void DratProofHandler::AddOneVariable() { reverse_mapping_.push_back(BooleanVariable(variable_index_++)); } -void DratWriter::AddClause(absl::Span clause) { - WriteClause(clause); +void DratProofHandler::AddProblemClause(absl::Span clause) { + if (drat_checker_ != nullptr) { + drat_checker_->AddProblemClause(clause); + } } -void DratWriter::DeleteClause(absl::Span clause) { - buffer_ += "d "; - WriteClause(clause); +void DratProofHandler::AddClause(absl::Span clause) { + MapClause(clause); + if (drat_checker_ != nullptr) { + drat_checker_->AddInferedClause(values_); + } + if (drat_writer_ != nullptr) { + drat_writer_->AddClause(values_); + } } -void DratWriter::WriteClause(absl::Span clause) { +void DratProofHandler::DeleteClause(absl::Span clause) { + MapClause(clause); + if (drat_checker_ != nullptr) { + drat_checker_->DeleteClause(values_); + } + if (drat_writer_ != nullptr) { + drat_writer_->DeleteClause(values_); + } +} + +DratChecker::Status DratProofHandler::Check(double max_time_in_seconds) { + if (drat_checker_ != nullptr) { + // The empty clause is not explicitly added by the solver. + drat_checker_->AddInferedClause({}); + return drat_checker_->Check(max_time_in_seconds); + } + return DratChecker::Status::UNKNOWN; +} + +void DratProofHandler::MapClause(absl::Span clause) { values_.clear(); for (const Literal l : clause) { CHECK_LT(l.Variable(), reverse_mapping_.size()); const Literal original_literal = Literal(reverse_mapping_[l.Variable()], l.IsPositive()); - values_.push_back(original_literal.SignedValue()); + values_.push_back(original_literal); } // The sorting is such that new variables appear first. This is important for // BVA since DRAT-trim only check the RAT property with respect to the first // variable of the clause. - std::sort(values_.begin(), values_.end(), - [](int a, int b) { return std::abs(a) > std::abs(b); }); - - for (const int v : values_) StringAppendF(&buffer_, "%d ", v); - buffer_ += "0\n"; - if (buffer_.size() > 10000) { -#if !defined(__PORTABLE_PLATFORM__) - CHECK_OK(file::WriteString(output_, buffer_, file::Defaults())); -#endif // !__PORTABLE_PLATFORM__ - buffer_.clear(); - } + std::sort(values_.begin(), values_.end(), [](Literal a, Literal b) { + return std::abs(a.SignedValue()) > std::abs(b.SignedValue()); + }); } } // namespace sat diff --git a/ortools/sat/drat.h b/ortools/sat/drat_proof_handler.h similarity index 59% rename from ortools/sat/drat.h rename to ortools/sat/drat_proof_handler.h index 3eb0d77300..d7268c934c 100644 --- a/ortools/sat/drat.h +++ b/ortools/sat/drat_proof_handler.h @@ -11,19 +11,17 @@ // See the License for the specific language governing permissions and // limitations under the License. -#ifndef OR_TOOLS_SAT_DRAT_H_ -#define OR_TOOLS_SAT_DRAT_H_ +#ifndef OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_ +#define OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_ +#include #include #include -#if !defined(__PORTABLE_PLATFORM__) -#include "ortools/base/file.h" -#else -class File {}; -#endif // !__PORTABLE_PLATFORM__ #include "ortools/base/span.h" #include "ortools/base/int_type_indexed_vector.h" +#include "ortools/sat/drat_checker.h" +#include "ortools/sat/drat_writer.h" #include "ortools/sat/sat_base.h" namespace operations_research { @@ -35,17 +33,25 @@ namespace sat { // // Note that DRAT proofs are often huge (can be GB), and take about as much time // to check as it takes for the solver to find the proof in the first place! -class DratWriter { +// +// This class is used to build the SAT proof, and can either save it to disk, +// and/or store it in memory (in which case the proof can be checked when it is +// complete). +class DratProofHandler { public: - DratWriter(bool in_binary_format, File* output) - : variable_index_(0), - in_binary_format_(in_binary_format), - output_(output) {} - ~DratWriter(); + // Use this constructor to store the DRAT proof in memory. The proof will not + // be written to disk, and can be checked with Check() when it is complete. + DratProofHandler(); + // Use this constructor to write the DRAT proof to disk, and to optionally + // store it in memory as well (in which case the proof can be checked with + // Check() when it is complete). + DratProofHandler(bool in_binary_format, File* output, bool check = false); + ~DratProofHandler() {} // During the presolve step, variable get deleted and the set of non-deleted // variable is remaped in a dense set. This allows to keep track of that and - // always output the DRAT clauses in term of the original variables. + // always output the DRAT clauses in term of the original variables. Must be + // called before adding or deleting clauses AddClause() or DeleteClause(). // // TODO(user): This is exactly the same mecanism as in the SatPostsolver // class. Factor out the code. @@ -55,42 +61,53 @@ class DratWriter { void SetNumVariables(int num_variables); void AddOneVariable(); + // Adds a clause of the UNSAT problem. This must be called before any call to + // AddClause() or DeleteClause(), in order to be able to check the DRAT proof + // with the Check() method when it is complete. + void AddProblemClause(absl::Span clause); + // Writes a new clause to the DRAT output. The output clause is sorted so that // newer variables always comes first. This is needed because in the DRAT // format, the clause is checked for the RAT property with only its first - // literal. + // literal. Must not be called after Check(). void AddClause(absl::Span clause); // Writes a "deletion" information about a clause that has been added before // to the DRAT output. Note that it is also possible to delete a clause from - // the problem. + // the problem. Must not be called after Check(). // // Because of a limitation a the DRAT-trim tool, it seems the order of the // literals during addition and deletion should be EXACTLY the same. Because // of this we get warnings for problem clauses. void DeleteClause(absl::Span clause); + // Returns VALID if the DRAT proof is correct, INVALID if it is not correct, + // or UNKNOWN if proof checking was not enabled (by choosing the right + // constructor) or timed out. This requires the problem clauses to be + // specified with AddProblemClause(), before the proof itself. + // + // WARNING: no new clause must be added or deleted after this method has been + // called. + DratChecker::Status Check(double max_time_in_seconds); + private: - void WriteClause(absl::Span clause); + void MapClause(absl::Span clause); // We need to keep track of the variable newly created. int variable_index_; - // TODO(user): Support binary format as proof in text format can be large. - bool in_binary_format_; - File* output_; - - std::string buffer_; - // Temporary vector used for sorting the outputed clauses. - std::vector values_; + std::vector values_; // This mapping will be applied to all clause passed to AddClause() or // DeleteClause() so that they are in term of the original problem. ITIVector reverse_mapping_; + + std::unique_ptr drat_checker_; + std::unique_ptr drat_writer_; }; } // namespace sat } // namespace operations_research -#endif // OR_TOOLS_SAT_DRAT_H_ +#endif // OR_TOOLS_SAT_DRAT_PROOF_HANDLER_H_ diff --git a/ortools/sat/drat_writer.cc b/ortools/sat/drat_writer.cc new file mode 100644 index 0000000000..9ce505d5a9 --- /dev/null +++ b/ortools/sat/drat_writer.cc @@ -0,0 +1,59 @@ +// Copyright 2010-2017 Google +// 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. + +#include "ortools/sat/drat_writer.h" + +#include + +#include "ortools/base/logging.h" +#include "ortools/base/stringprintf.h" +#if !defined(__PORTABLE_PLATFORM__) +#endif // !__PORTABLE_PLATFORM__ +#include "ortools/base/status.h" + +namespace operations_research { +namespace sat { + +DratWriter::~DratWriter() { + if (output_ != nullptr) { +#if !defined(__PORTABLE_PLATFORM__) + CHECK_OK(file::WriteString(output_, buffer_, file::Defaults())); + CHECK_OK(output_->Close(file::Defaults())); +#endif // !__PORTABLE_PLATFORM__ + } +} + +void DratWriter::AddClause(absl::Span clause) { + WriteClause(clause); +} + +void DratWriter::DeleteClause(absl::Span clause) { + buffer_ += "d "; + WriteClause(clause); +} + +void DratWriter::WriteClause(absl::Span clause) { + for (const Literal literal : clause) { + StringAppendF(&buffer_, "%d ", literal.SignedValue()); + } + buffer_ += "0\n"; + if (buffer_.size() > 10000) { +#if !defined(__PORTABLE_PLATFORM__) + CHECK_OK(file::WriteString(output_, buffer_, file::Defaults())); +#endif // !__PORTABLE_PLATFORM__ + buffer_.clear(); + } +} + +} // namespace sat +} // namespace operations_research diff --git a/ortools/sat/drat_writer.h b/ortools/sat/drat_writer.h new file mode 100644 index 0000000000..964acf9bab --- /dev/null +++ b/ortools/sat/drat_writer.h @@ -0,0 +1,64 @@ +// Copyright 2010-2017 Google +// 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. + +#ifndef OR_TOOLS_SAT_DRAT_WRITER_H_ +#define OR_TOOLS_SAT_DRAT_WRITER_H_ + +#include + +#if !defined(__PORTABLE_PLATFORM__) +#include "ortools/base/file.h" +#else +class File {}; +#endif // !__PORTABLE_PLATFORM__ +#include "ortools/base/span.h" +#include "ortools/sat/sat_base.h" + +namespace operations_research { +namespace sat { + +// DRAT is a SAT proof format that allows a simple program to check that the +// problem is really UNSAT. The description of the format and a checker are +// available at: // http://www.cs.utexas.edu/~marijn/drat-trim/ +// +// Note that DRAT proofs are often huge (can be GB), and take about as much time +// to check as it takes for the solver to find the proof in the first place! +class DratWriter { + public: + DratWriter(bool in_binary_format, File* output) + : in_binary_format_(in_binary_format), output_(output) {} + ~DratWriter(); + + // Writes a new clause to the DRAT output. Note that the RAT property is only + // checked on the first literal. + void AddClause(absl::Span clause); + + // Writes a "deletion" information about a clause that has been added before + // to the DRAT output. Note that it is also possible to delete a clause from + // the problem. + void DeleteClause(absl::Span clause); + + private: + void WriteClause(absl::Span clause); + + // TODO(user): Support binary format as proof in text format can be large. + bool in_binary_format_; + File* output_; + + std::string buffer_; +}; + +} // namespace sat +} // namespace operations_research + +#endif // OR_TOOLS_SAT_DRAT_WRITER_H_ diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index 540653a75b..92e12d242e 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -966,13 +966,17 @@ IntegerTrail::Dependencies(int trail_index) const { void IntegerTrail::AppendLiteralsReason(int trail_index, std::vector* output) const { const int reason_index = integer_trail_[trail_index].reason_index; - output->insert( - output->end(), - literals_reason_buffer_.begin() + literals_reason_starts_[reason_index], - reason_index + 1 < literals_reason_starts_.size() - ? literals_reason_buffer_.begin() + - literals_reason_starts_[reason_index + 1] - : literals_reason_buffer_.end()); + const int start = literals_reason_starts_[reason_index]; + const int end = reason_index + 1 < literals_reason_starts_.size() + ? literals_reason_starts_[reason_index + 1] + : literals_reason_buffer_.size(); + for (int i = start; i < end; ++i) { + const Literal l = literals_reason_buffer_[i]; + if (!added_variables_[l.Variable()]) { + added_variables_.Set(l.Variable()); + output->push_back(l); + } + } } std::vector IntegerTrail::ReasonFor(IntegerLiteral literal) const { @@ -1015,6 +1019,11 @@ void IntegerTrail::MergeReasonIntoInternal(std::vector* output) const { tmp_var_to_trail_index_in_queue_.end(), [](int v) { return v == 0; })); + added_variables_.ClearAndResize(BooleanVariable(trail_->NumVariables())); + for (const Literal l : *output) { + added_variables_.Set(l.Variable()); + } + // During the algorithm execution, all the queue entries that do not match the // content of tmp_var_to_trail_index_in_queue_[] will be ignored. for (const int trail_index : tmp_queue_) { @@ -1109,13 +1118,13 @@ void IntegerTrail::MergeReasonIntoInternal(std::vector* output) const { for (const IntegerVariable var : tmp_to_clear_) { tmp_var_to_trail_index_in_queue_[var] = 0; } - gtl::STLSortAndRemoveDuplicates(output); } absl::Span IntegerTrail::Reason(const Trail& trail, int trail_index) const { const int index = boolean_trail_index_to_integer_one_[trail_index]; std::vector* reason = trail.GetEmptyVectorToStoreReason(trail_index); + added_variables_.ClearAndResize(BooleanVariable(trail_->NumVariables())); AppendLiteralsReason(index, reason); DCHECK(tmp_queue_.empty()); for (const IntegerLiteral lit : Dependencies(index)) { diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index ce238fd54c..2cbd18eb1b 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -648,7 +648,9 @@ class IntegerTrail : public SatPropagator { Dependencies(int trail_index) const; // Helper function to append the Literal part of the reason for this bound - // assignment. + // assignment. We use added_variables_ to not add the same literal twice. + // Note that looking at literal.Variable() is enough since all the literals + // of a reason must be false. void AppendLiteralsReason(int trail_index, std::vector* output) const; @@ -725,6 +727,7 @@ class IntegerTrail : public SatPropagator { mutable std::vector tmp_queue_; mutable std::vector tmp_to_clear_; mutable ITIVector tmp_var_to_trail_index_in_queue_; + mutable SparseBitset added_variables_; // For EnqueueLiteral(), we store a special TrailEntry to recover the reason // lazily. This vector indicates the correspondence between a literal that diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index d3e5612be6..d118914e75 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -257,6 +257,9 @@ std::function SatSolverRestartPolicy(Model* model) { SatSolver::Status SolveIntegerProblemWithLazyEncoding( const std::vector& assumptions, const std::function& next_decision, Model* model) { + if (model->GetOrCreate()->LimitReached()) { + return SatSolver::LIMIT_REACHED; + } SatSolver* const solver = model->GetOrCreate(); if (!solver->ResetWithGivenAssumptions(assumptions)) { return solver->UnsatStatus(); diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index ae0ba0848a..115ff91cfc 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -1132,6 +1132,8 @@ SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( LOG(INFO) << "#Boolean_variables:" << sat_solver->NumVariables(); } + const SatParameters& parameters = *(model->GetOrCreate()); + // Simple linear scan algorithm to find the optimal. SatSolver::Status result; bool model_is_feasible = false; @@ -1149,6 +1151,9 @@ SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( if (feasible_solution_observer != nullptr) { feasible_solution_observer(*model); } + if (parameters.stop_after_first_solution()) { + return SatSolver::LIMIT_REACHED; + } // Restrict the objective. sat_solver->Backtrack(0); @@ -1178,6 +1183,103 @@ SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( return result; } +void RestrictObjectiveDomainWithBinarySearch( + IntegerVariable objective_var, + const std::function& next_decision, + const std::function& feasible_solution_observer, + Model* model) { + const SatParameters old_params = *model->GetOrCreate(); + SatSolver* sat_solver = model->GetOrCreate(); + IntegerTrail* integer_trail = model->GetOrCreate(); + IntegerEncoder* integer_encoder = model->GetOrCreate(); + + // Set the requested conflict limit. + { + SatParameters new_params = old_params; + new_params.set_max_number_of_conflicts( + old_params.binary_search_num_conflicts()); + *model->GetOrCreate() = new_params; + } + + // The assumption (objective <= value) for values in + // [unknown_min, unknown_max] reached the conflict limit. + bool loop = true; + IntegerValue unknown_min = integer_trail->UpperBound(objective_var); + IntegerValue unknown_max = integer_trail->LowerBound(objective_var); + while (loop) { + sat_solver->Backtrack(0); + const IntegerValue lb = integer_trail->LowerBound(objective_var); + const IntegerValue ub = integer_trail->UpperBound(objective_var); + unknown_min = std::min(unknown_min, ub); + unknown_max = std::max(unknown_max, lb); + + // We first refine the lower bound and then the upper bound. + IntegerValue target; + if (lb < unknown_min) { + target = lb + (unknown_min - lb) / 2; + } else if (unknown_max < ub) { + target = ub - (ub - unknown_max) / 2; + } else { + VLOG(1) << "Binary-search, done."; + break; + } + VLOG(1) << "Binary-search, objective: [" << lb << "," << ub << "]" + << " tried: [" << unknown_min << "," << unknown_max << "]" + << " target: obj<=" << target; + SatSolver::Status result; + if (target < ub) { + const Literal assumption = integer_encoder->GetOrCreateAssociatedLiteral( + IntegerLiteral::LowerOrEqual(objective_var, target)); + result = SolveIntegerProblemWithLazyEncoding({assumption}, next_decision, + model); + } else { + result = SolveIntegerProblemWithLazyEncoding({}, next_decision, model); + } + + switch (result) { + case SatSolver::MODEL_UNSAT: { + loop = false; + break; + } + case SatSolver::ASSUMPTIONS_UNSAT: { + // Update the objective lower bound. + sat_solver->Backtrack(0); + if (!integer_trail->Enqueue( + IntegerLiteral::GreaterOrEqual(objective_var, target + 1), {}, + {})) { + loop = false; + } + break; + } + case SatSolver::MODEL_SAT: { + // The objective is the current lower bound of the objective_var. + const IntegerValue objective = integer_trail->LowerBound(objective_var); + if (feasible_solution_observer != nullptr) { + feasible_solution_observer(*model); + } + + // We have a solution, restrict the objective upper bound to only look + // for better ones now. + sat_solver->Backtrack(0); + if (!integer_trail->Enqueue( + IntegerLiteral::LowerOrEqual(objective_var, objective - 1), {}, + {})) { + loop = false; + } + break; + } + case SatSolver::LIMIT_REACHED: { + unknown_min = std::min(target, unknown_min); + unknown_max = std::max(target, unknown_max); + break; + } + } + } + + sat_solver->Backtrack(0); + *model->GetOrCreate() = old_params; +} + namespace { // If the given model is unsat under the given assumptions, returns one or more diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h index 1a25416590..4f958078f7 100644 --- a/ortools/sat/optimization.h +++ b/ortools/sat/optimization.h @@ -145,6 +145,14 @@ SatSolver::Status MinimizeIntegerVariableWithLinearScanAndLazyEncoding( const std::function& feasible_solution_observer, Model* model); +// Use a low conflict limit and performs a binary search to try to restrict the +// domain of objective_var. +void RestrictObjectiveDomainWithBinarySearch( + IntegerVariable objective_var, + const std::function& next_decision, + const std::function& feasible_solution_observer, + Model* model); + // Same as MinimizeIntegerVariableWithLinearScanAndLazyEncoding() but use // a core-based approach instead. Note that the given objective_var is just used // for reporting the lower-bound and do not need to be linked with its linear diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index d085520463..34eaf241f1 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -18,7 +18,7 @@ package operations_research.sat; // Contains the definitions for all the sat algorithm parameters and their // default values. // -// NEXT TAG: 98 +// NEXT TAG: 100 message SatParameters { // ========================================================================== // Branching and polarity @@ -169,6 +169,22 @@ message SatParameters { optional int32 pb_cleanup_increment = 46 [default = 200]; optional double pb_cleanup_ratio = 47 [default = 0.5]; + // Parameters for an heuristic similar to the one descibed in "An effective + // learnt clause minimization approach for CDCL Sat Solvers", + // https://www.ijcai.org/proceedings/2017/0098.pdf + // + // For now, we have a somewhat simpler implementation where every x restart we + // spend y decisions on clause minimization. The minimization technique is the + // same as the one used to minimize core in max-sat. We also minimize problem + // clauses and not just the learned clause that we keep forever like in the + // paper. + // + // Changing these parameters or the kind of clause we minimize seems to have + // a big impact on the overall perf on our benchmarks. So this technique seems + // definitely useful, but it is hard to tune properly. + optional int32 minimize_with_propagation_restart_period = 96 [default = 10]; + optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000]; + // ========================================================================== // Variable and clause activities // ========================================================================== @@ -507,6 +523,12 @@ message SatParameters { // lower bound instead. optional bool optimize_with_core = 83 [default = false]; + // If non-negative, perform a binary search on the objective variable in order + // to find an [min, max] interval outside of which the solver proved unsat/sat + // under this amount of conflict. This can quickly reduce the objective domain + // on some problems. + optional int32 binary_search_num_conflicts = 99 [default = -1]; + // This has no effect if optimize_with_core is false. If true, use a different // core-based algorithm similar to the max-HS algo for max-SAT. This is a // hybrid MIP/CP approach and it uses a MIP solver in addition to the CP/SAT @@ -535,19 +557,6 @@ message SatParameters { // of precedence. optional bool auto_detect_greater_than_at_least_one_of = 95 [default = true]; - // Parameters for an heuristic similar to the one descibed in "An effective - // learnt clause minimization approach for CDCL Sat Solvers", - // https://www.ijcai.org/proceedings/2017/0098.pdf - // - // For now, we have a somewhat simpler implementation where every x restart we - // spend y decisions on clause minimization. The minimization technique is the - // same as the one used to minimize core in max-sat. We also minimize problem - // clauses and not just the learned clause that we keep forever like in the - // paper. - // - // Changing these parameters or the kind of clause we minimize seems to have - // a big impact on the overall perf on our benchmarks. So this technique seems - // definitely useful, but it is hard to tune properly. - optional int32 minimize_with_propagation_restart_period = 96 [default = 10]; - optional int32 minimize_with_propagation_num_decisions = 97 [default = 1000]; + // For an optimization problem, stop the solver as soon as we have a solution. + optional bool stop_after_first_solution = 98 [default = false]; } diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index d449cd2d38..48d7bfdf0c 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -59,7 +59,7 @@ SatSolver::SatSolver(Model* model) same_reason_identifier_(*trail_), is_relevant_for_core_computation_(true), problem_is_pure_sat_(true), - drat_writer_(nullptr), + drat_proof_handler_(nullptr), stats_("SatSolver") { // TODO(user): move these 3 classes in the Model so that everyone can access // them if needed and we don't have the wiring here. @@ -724,8 +724,8 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() { // database. This is because we already backtracked and some of the clauses // that where needed to infer the conflict may not be "reasons" anymore and // may be deleted. - if (drat_writer_ != nullptr) { - drat_writer_->AddClause(learned_conflict_); + if (drat_proof_handler_ != nullptr) { + drat_proof_handler_->AddClause(learned_conflict_); } // Detach any subsumed clause. They will actually be deleted on the next @@ -958,6 +958,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) { const int variable_level = LiteralTrail().Info(literal.Variable()).level; if (variable_level == 0) { + ProcessNewlyFixedVariablesForDratProof(); counters_.minimization_num_true++; counters_.minimization_num_removed_literals += clause->Size(); Backtrack(0); @@ -1011,7 +1012,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) { // Write the new clause to the proof before the deletion of the old one // happens (when we will detach it). - if (drat_writer_ != nullptr) drat_writer_->AddClause(candidate); + if (drat_proof_handler_ != nullptr) drat_proof_handler_->AddClause(candidate); if (candidate.size() == 1) { if (!Assignment().VariableIsAssigned(candidate[0].Variable())) { @@ -1460,7 +1461,7 @@ std::string SatSolver::RunningStatisticsString() const { "%6.2fs, mem:%s, fails:%" GG_LL_FORMAT "d, " "depth:%d, clauses:%lld, tmp:%lld, bin:%llu, restarts:%d, vars:%d", - time_in_s, MemoryUsage().c_str(), counters_.num_failures, CurrentDecisionLevel(), + time_in_s, MemoryUsage(), counters_.num_failures, CurrentDecisionLevel(), clauses_propagator_.num_clauses() - clauses_propagator_.num_removable_clauses(), clauses_propagator_.num_removable_clauses(), @@ -1468,22 +1469,35 @@ std::string SatSolver::RunningStatisticsString() const { num_variables_.value() - num_processed_fixed_variables_); } +void SatSolver::ProcessNewlyFixedVariablesForDratProof() { + if (drat_proof_handler_ == nullptr) return; + if (CurrentDecisionLevel() != 0) return; + + // We need to output the literals that are fixed so we can remove all + // clauses that contains them. Note that this doesn't seems to be needed + // for drat-trim. + // + // TODO(user): Ideally we could output such literal as soon as they are fixed, + // but this is not that easy to do. Spend some time to find a cleaner + // alternative? Currently this works, but: + // - We will output some fixed literals twice since we already output learnt + // clauses of size one. + // - We need to call this function when needed. + Literal temp; + for (; drat_num_processed_fixed_variables_ < trail_->Index(); + ++drat_num_processed_fixed_variables_) { + temp = (*trail_)[drat_num_processed_fixed_variables_]; + drat_proof_handler_->AddClause({&temp, 1}); + } +} + void SatSolver::ProcessNewlyFixedVariables() { SCOPED_TIME_STAT(&stats_); DCHECK_EQ(CurrentDecisionLevel(), 0); int num_detached_clauses = 0; int num_binary = 0; - if (drat_writer_ != nullptr) { - // We need to output the literals that are fixed so we can remove all - // clauses that contains them. Note that this doesn't seems to be needed - // for drat-trim. - Literal temp; - for (int i = num_processed_fixed_variables_; i < trail_->Index(); ++i) { - temp = (*trail_)[i]; - drat_writer_->AddClause({&temp, 1}); - } - } + ProcessNewlyFixedVariablesForDratProof(); // We remove the clauses that are always true and the fixed literals from the // others. Note that none of the clause should be all false because we should @@ -1502,10 +1516,10 @@ void SatSolver::ProcessNewlyFixedVariables() { const size_t new_size = clause->Size(); if (new_size == old_size) continue; - if (drat_writer_ != nullptr) { + if (drat_proof_handler_ != nullptr) { CHECK_GT(new_size, 0); - drat_writer_->AddClause({clause->begin(), new_size}); - drat_writer_->DeleteClause({clause->begin(), old_size}); + drat_proof_handler_->AddClause({clause->begin(), new_size}); + drat_proof_handler_->DeleteClause({clause->begin(), old_size}); } if (new_size == 2 && parameters_->treat_binary_clauses_separately()) { diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index 4c0dcf8f80..425e2e152d 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -36,7 +36,7 @@ #include "ortools/base/int_type_indexed_vector.h" #include "ortools/base/hash.h" #include "ortools/sat/clause.h" -#include "ortools/sat/drat.h" +#include "ortools/sat/drat_proof_handler.h" #include "ortools/sat/model.h" #include "ortools/sat/pb_constraint.h" #include "ortools/sat/restart.h" @@ -372,9 +372,9 @@ class SatSolver { // Returns true iff the loaded problem only contains clauses. bool ProblemIsPureSat() const { return problem_is_pure_sat_; } - void SetDratWriter(DratWriter* drat_writer) { - drat_writer_ = drat_writer; - clauses_propagator_.SetDratWriter(drat_writer); + void SetDratProofHandler(DratProofHandler* drat_proof_handler) { + drat_proof_handler_ = drat_proof_handler; + clauses_propagator_.SetDratProofHandler(drat_proof_handler_); } // This function is here to deal with the case where a SAT/CP model is found @@ -547,6 +547,9 @@ class SatSolver { // Simplifies the problem when new variables are assigned at level 0. void ProcessNewlyFixedVariables(); + // Output to the DRAT proof handler any newly fixed variables. + void ProcessNewlyFixedVariablesForDratProof(); + // Returns the maximum trail_index of the literals in the given clause. // All the literals must be assigned. Returns -1 if the clause is empty. int ComputeMaxTrailIndex(absl::Span clause) const; @@ -716,6 +719,9 @@ class SatSolver { int num_processed_fixed_variables_; double deterministic_time_of_last_fixed_variables_cleanup_; + // Used in ProcessNewlyFixedVariablesForDratProof(). + int drat_num_processed_fixed_variables_ = 0; + // Tracks various information about the solver progress. struct Counters { int64 num_branches = 0; @@ -810,7 +816,7 @@ class SatSolver { // This is true iff the loaded problem only contains clauses. bool problem_is_pure_sat_; - DratWriter* drat_writer_; + DratProofHandler* drat_proof_handler_; mutable StatsGroup stats_; DISALLOW_COPY_AND_ASSIGN(SatSolver); diff --git a/ortools/sat/simplification.cc b/ortools/sat/simplification.cc index 8c661a3aa0..872258de31 100644 --- a/ortools/sat/simplification.cc +++ b/ortools/sat/simplification.cc @@ -186,9 +186,9 @@ void SatPresolver::AddClause(absl::Span clause) { } } - if (drat_writer_ != nullptr && changed) { - drat_writer_->AddClause(clause_ref); - drat_writer_->DeleteClause(clause); + if (drat_proof_handler_ != nullptr && changed) { + drat_proof_handler_->AddClause(clause_ref); + drat_proof_handler_->DeleteClause(clause); } const Literal max_literal = clause_ref.back(); @@ -214,7 +214,7 @@ void SatPresolver::SetNumVariables(int num_variables) { } void SatPresolver::AddClauseInternal(std::vector* clause) { - if (drat_writer_ != nullptr) drat_writer_->AddClause(*clause); + if (drat_proof_handler_ != nullptr) drat_proof_handler_->AddClause(*clause); DCHECK(std::is_sorted(clause->begin(), clause->end())); CHECK_GT(clause->size(), 0) << "TODO(fdid): Unsat during presolve?"; @@ -431,7 +431,7 @@ void SatPresolver::SimpleBva(LiteralIndex l) { bva_pq_elements_[x_false.value()].literal = x_false; // Add the new clauses. - if (drat_writer_ != nullptr) drat_writer_->AddOneVariable(); + if (drat_proof_handler_ != nullptr) drat_proof_handler_->AddOneVariable(); for (const LiteralIndex lit : m_lit_) { tmp_new_clause_ = {Literal(lit), Literal(x_true)}; AddClauseInternal(&tmp_new_clause_); @@ -519,9 +519,9 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) { } else { CHECK_NE(opposite_literal, lit.Index()); if (clauses_[ci].empty()) return false; // UNSAT. - if (drat_writer_ != nullptr) { + if (drat_proof_handler_ != nullptr) { // TODO(user): remove the old clauses_[ci] afterwards. - drat_writer_->AddClause(clauses_[ci]); + drat_proof_handler_->AddClause(clauses_[ci]); } // Remove ci from the occurrence list. Note that the occurrence list @@ -564,9 +564,9 @@ bool SatPresolver::ProcessClauseToSimplifyOthers(ClauseIndex clause_index) { if (SimplifyClause(clause, &clauses_[ci], &opposite_literal)) { CHECK_EQ(opposite_literal, lit.NegatedIndex()); if (clauses_[ci].empty()) return false; // UNSAT. - if (drat_writer_ != nullptr) { + if (drat_proof_handler_ != nullptr) { // TODO(user): remove the old clauses_[ci] afterwards. - drat_writer_->AddClause(clauses_[ci]); + drat_proof_handler_->AddClause(clauses_[ci]); } if (!in_clause_to_process_[ci]) { in_clause_to_process_[ci] = true; @@ -692,8 +692,8 @@ void SatPresolver::Remove(ClauseIndex ci) { UpdateBvaPriorityQueue(Literal(e.Variable(), true).Index()); UpdateBvaPriorityQueue(Literal(e.Variable(), false).Index()); } - if (drat_writer_ != nullptr) { - drat_writer_->DeleteClause(clauses_[ci]); + if (drat_proof_handler_ != nullptr) { + drat_proof_handler_->DeleteClause(clauses_[ci]); } gtl::STLClearObject(&clauses_[ci]); } @@ -1016,7 +1016,8 @@ class PropagationGraph { }; void ProbeAndFindEquivalentLiteral( - SatSolver* solver, SatPostsolver* postsolver, DratWriter* drat_writer, + SatSolver* solver, SatPostsolver* postsolver, + DratProofHandler* drat_proof_handler, ITIVector* mapping) { solver->Backtrack(0); mapping->clear(); @@ -1081,7 +1082,9 @@ void ProbeAndFindEquivalentLiteral( ? Literal(rep) : Literal(rep).Negated(); solver->AddUnitClause(true_lit); - if (drat_writer != nullptr) drat_writer->AddClause({true_lit}); + if (drat_proof_handler != nullptr) { + drat_proof_handler->AddClause({true_lit}); + } } } for (LiteralIndex i(0); i < size; ++i) { @@ -1093,7 +1096,9 @@ void ProbeAndFindEquivalentLiteral( ? Literal(i) : Literal(i).Negated(); solver->AddUnitClause(true_lit); - if (drat_writer != nullptr) drat_writer->AddClause({true_lit}); + if (drat_proof_handler != nullptr) { + drat_proof_handler->AddClause({true_lit}); + } } } else if (assignment.LiteralIsAssigned(Literal(i))) { if (!assignment.LiteralIsAssigned(Literal(rep))) { @@ -1101,15 +1106,15 @@ void ProbeAndFindEquivalentLiteral( ? Literal(rep) : Literal(rep).Negated(); solver->AddUnitClause(true_lit); - if (drat_writer != nullptr) { - drat_writer->AddClause({true_lit}); + if (drat_proof_handler != nullptr) { + drat_proof_handler->AddClause({true_lit}); } } } else if (rep != i) { ++num_equiv; postsolver->Add(Literal(i), {Literal(i), Literal(rep).Negated()}); - if (drat_writer != nullptr) { - drat_writer->AddClause({Literal(i), Literal(rep).Negated()}); + if (drat_proof_handler != nullptr) { + drat_proof_handler->AddClause({Literal(i), Literal(rep).Negated()}); } } } @@ -1123,7 +1128,7 @@ void ProbeAndFindEquivalentLiteral( SatSolver::Status SolveWithPresolve(std::unique_ptr* solver, TimeLimit* time_limit, std::vector* solution, - DratWriter* drat_writer) { + DratProofHandler* drat_proof_handler) { // We save the initial parameters. const SatParameters parameters = (*solver)->parameters(); SatPostsolver postsolver((*solver)->NumVariables()); @@ -1182,8 +1187,8 @@ SatSolver::Status SolveWithPresolve(std::unique_ptr* solver, // Probe + find equivalent literals. // TODO(user): Use a derived time limit in the probing phase. ITIVector equiv_map; - ProbeAndFindEquivalentLiteral((*solver).get(), &postsolver, drat_writer, - &equiv_map); + ProbeAndFindEquivalentLiteral((*solver).get(), &postsolver, + drat_proof_handler, &equiv_map); if ((*solver)->IsModelUnsat()) { VLOG(1) << "UNSAT during probing."; return SatSolver::MODEL_UNSAT; @@ -1206,7 +1211,7 @@ SatSolver::Status SolveWithPresolve(std::unique_ptr* solver, // TODO(user): Pass the time_limit to the presolver. SatPresolver presolver(&postsolver); presolver.SetParameters(parameters); - presolver.SetDratWriter(drat_writer); + presolver.SetDratProofHandler(drat_proof_handler); presolver.SetEquivalentLiteralMapping(equiv_map); (*solver)->ExtractClauses(&presolver); (*solver)->AdvanceDeterministicTime(time_limit); @@ -1220,13 +1225,13 @@ SatSolver::Status SolveWithPresolve(std::unique_ptr* solver, } postsolver.ApplyMapping(presolver.VariableMapping()); - if (drat_writer != nullptr) { - drat_writer->ApplyMapping(presolver.VariableMapping()); + if (drat_proof_handler != nullptr) { + drat_proof_handler->ApplyMapping(presolver.VariableMapping()); } // Load the presolved problem in a new solver. (*solver).reset(new SatSolver()); - (*solver)->SetDratWriter(drat_writer); + (*solver)->SetDratProofHandler(drat_proof_handler); (*solver)->SetParameters(parameters); presolver.LoadProblemIntoSatSolver((*solver).get()); diff --git a/ortools/sat/simplification.h b/ortools/sat/simplification.h index 763fb410ef..21a8b07a0b 100644 --- a/ortools/sat/simplification.h +++ b/ortools/sat/simplification.h @@ -29,7 +29,7 @@ #include "ortools/base/span.h" #include "ortools/base/int_type.h" #include "ortools/base/int_type_indexed_vector.h" -#include "ortools/sat/drat.h" +#include "ortools/sat/drat_proof_handler.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" @@ -140,7 +140,7 @@ class SatPresolver { explicit SatPresolver(SatPostsolver* postsolver) : postsolver_(postsolver), num_trivial_clauses_(0), - drat_writer_(nullptr) {} + drat_proof_handler_(nullptr) {} void SetParameters(const SatParameters& params) { parameters_ = params; } // Registers a mapping to encode equivalent literals. @@ -208,7 +208,9 @@ class SatPresolver { // Visible for testing. Just applies the BVA step of the presolve. void PresolveWithBva(); - void SetDratWriter(DratWriter* drat_writer) { drat_writer_ = drat_writer; } + void SetDratProofHandler(DratProofHandler* drat_proof_handler) { + drat_proof_handler_ = drat_proof_handler; + } private: // Internal function to add clauses generated during the presolve. The clause @@ -331,7 +333,7 @@ class SatPresolver { int num_trivial_clauses_; SatParameters parameters_; - DratWriter* drat_writer_; + DratProofHandler* drat_proof_handler_; DISALLOW_COPY_AND_ASSIGN(SatPresolver); }; @@ -384,7 +386,8 @@ int ComputeResolvantSize(Literal x, const std::vector& a, // only pure SAT problem, but the returned mapping do need to be applied to all // constraints. void ProbeAndFindEquivalentLiteral( - SatSolver* solver, SatPostsolver* postsolver, DratWriter* drat_writer, + SatSolver* solver, SatPostsolver* postsolver, + DratProofHandler* drat_proof_handler, ITIVector* mapping); // Given a 'solver' with a problem already loaded, this will try to simplify the @@ -400,7 +403,7 @@ void ProbeAndFindEquivalentLiteral( SatSolver::Status SolveWithPresolve( std::unique_ptr* solver, TimeLimit* time_limit, std::vector* solution /* only filled if SAT */, - DratWriter* drat_writer /* can be nullptr */); + DratProofHandler* drat_proof_handler /* can be nullptr */); } // namespace sat } // namespace operations_research