From 5a20b0296ed83ef96e4429f511916a489ebb3d1b Mon Sep 17 00:00:00 2001 From: Corentin Le Molgat Date: Wed, 20 Nov 2024 15:10:09 +0100 Subject: [PATCH] backport sat fuzztest from main --- MODULE.bazel | 20 +- ortools/base/BUILD.bazel | 13 + ortools/base/fuzztest.h | 55 + ortools/sat/BUILD.bazel | 16 + ortools/sat/CMakeLists.txt | 1 + ortools/sat/cp_model_solver_fuzz.cc | 69 + ortools/sat/fuzz_testdata/BadHintWithCore | 38 + .../DualConnectedComponentsModel | 70 + .../sat/fuzz_testdata/EnumerateAllSolutions | 27 + .../fuzz_testdata/EnumerateAllSolutionsBis | 21 + .../EnumerateAllSolutionsOfEmptyModel | 15 + ortools/sat/fuzz_testdata/HintWithCore | 34 + ortools/sat/fuzz_testdata/InvalidProblem | 5 + .../fuzz_testdata/MultipleEnforcementLiteral | 31 + .../fuzz_testdata/NonInstantiatedVariables | 21 + .../fuzz_testdata/ObjectiveDomainLowerBound | 27 + ortools/sat/fuzz_testdata/PureSatProblem | 2504 ++++++++ .../sat/fuzz_testdata/PureSatProblemWithLimit | 3386 +++++++++++ ortools/sat/fuzz_testdata/SimpleCumulative | 61 + ortools/sat/fuzz_testdata/SimpleInterval | 46 + .../SimpleLinearExampleWithMaximize | 28 + .../SimpleOptionalIntervalFeasible | 83 + .../SimpleOptionalIntervalInfeasible | 83 + .../SmallDualConnectedComponentsModel | 50 + .../sat/fuzz_testdata/SolutionHintBasicTest | 5406 +++++++++++++++++ .../fuzz_testdata/SolutionHintEnumerateTest | 27 + .../fuzz_testdata/SolutionHintObjectiveTest | 39 + .../SolutionHintOptimalObjectiveTest | 39 + ...lutionsAreCorrectlyPostsolvedInTheObserver | 19 + ortools/sat/fuzz_testdata/TightenedDomains | 27 + .../TightenedDomainsIfInfeasible | 27 + .../TrivialLinearTranslatedModel | 42 + .../sat/fuzz_testdata/TrivialModelWithCore | 11 + ortools/sat/fuzz_testdata/UnsatProblem | 21 + 34 files changed, 12353 insertions(+), 9 deletions(-) create mode 100644 ortools/base/fuzztest.h create mode 100644 ortools/sat/cp_model_solver_fuzz.cc create mode 100644 ortools/sat/fuzz_testdata/BadHintWithCore create mode 100644 ortools/sat/fuzz_testdata/DualConnectedComponentsModel create mode 100644 ortools/sat/fuzz_testdata/EnumerateAllSolutions create mode 100644 ortools/sat/fuzz_testdata/EnumerateAllSolutionsBis create mode 100644 ortools/sat/fuzz_testdata/EnumerateAllSolutionsOfEmptyModel create mode 100644 ortools/sat/fuzz_testdata/HintWithCore create mode 100644 ortools/sat/fuzz_testdata/InvalidProblem create mode 100644 ortools/sat/fuzz_testdata/MultipleEnforcementLiteral create mode 100644 ortools/sat/fuzz_testdata/NonInstantiatedVariables create mode 100644 ortools/sat/fuzz_testdata/ObjectiveDomainLowerBound create mode 100644 ortools/sat/fuzz_testdata/PureSatProblem create mode 100644 ortools/sat/fuzz_testdata/PureSatProblemWithLimit create mode 100644 ortools/sat/fuzz_testdata/SimpleCumulative create mode 100644 ortools/sat/fuzz_testdata/SimpleInterval create mode 100644 ortools/sat/fuzz_testdata/SimpleLinearExampleWithMaximize create mode 100644 ortools/sat/fuzz_testdata/SimpleOptionalIntervalFeasible create mode 100644 ortools/sat/fuzz_testdata/SimpleOptionalIntervalInfeasible create mode 100644 ortools/sat/fuzz_testdata/SmallDualConnectedComponentsModel create mode 100644 ortools/sat/fuzz_testdata/SolutionHintBasicTest create mode 100644 ortools/sat/fuzz_testdata/SolutionHintEnumerateTest create mode 100644 ortools/sat/fuzz_testdata/SolutionHintObjectiveTest create mode 100644 ortools/sat/fuzz_testdata/SolutionHintOptimalObjectiveTest create mode 100644 ortools/sat/fuzz_testdata/SolutionsAreCorrectlyPostsolvedInTheObserver create mode 100644 ortools/sat/fuzz_testdata/TightenedDomains create mode 100644 ortools/sat/fuzz_testdata/TightenedDomainsIfInfeasible create mode 100644 ortools/sat/fuzz_testdata/TrivialLinearTranslatedModel create mode 100644 ortools/sat/fuzz_testdata/TrivialModelWithCore create mode 100644 ortools/sat/fuzz_testdata/UnsatProblem diff --git a/MODULE.bazel b/MODULE.bazel index 5a295913d4..dff277c77c 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -9,14 +9,15 @@ OR_TOOLS_VERSION = "9.12.0" module( name = "or-tools", - repo_name = "com_google_ortools", version = OR_TOOLS_VERSION, + repo_name = "com_google_ortools", ) bazel_dep(name = "abseil-cpp", version = "20240722.0", repo_name = "com_google_absl") bazel_dep(name = "bazel_skylib", version = "1.7.1") bazel_dep(name = "contrib_rules_jvm", version = "0.27.0") bazel_dep(name = "eigen", version = "3.4.0.bcr.1") +bazel_dep(name = "fuzztest", version = "20241028.0", repo_name = "com_google_fuzztest") bazel_dep(name = "gazelle", version = "0.39.1", repo_name = "bazel_gazelle") bazel_dep(name = "glpk", version = "5.0.bcr.1") bazel_dep(name = "google_benchmark", version = "1.8.5", repo_name = "com_google_benchmark") @@ -42,8 +43,8 @@ bazel_dep(name = "zlib", version = "1.3.1.bcr.3") git_override( module_name = "pybind11_abseil", commit = "70f8b693b3b70573ca785ef62d9f48054f45d786", - patches = ["//patches:pybind11_abseil.patch"], patch_strip = 1, + patches = ["//patches:pybind11_abseil.patch"], remote = "https://github.com/pybind/pybind11_abseil.git", ) @@ -57,14 +58,15 @@ SUPPORTED_PYTHON_VERSIONS = [ DEFAULT_PYTHON = "3.11" -python = use_extension("@rules_python//python/extensions:python.bzl", "python", dev_dependency=True) +python = use_extension("@rules_python//python/extensions:python.bzl", "python", dev_dependency = True) + [ - python.toolchain( - ignore_root_user_error = True, # needed for CI - python_version = version, - is_default = version == DEFAULT_PYTHON, - ) - for version in SUPPORTED_PYTHON_VERSIONS + python.toolchain( + ignore_root_user_error = True, # needed for CI + is_default = version == DEFAULT_PYTHON, + python_version = version, + ) + for version in SUPPORTED_PYTHON_VERSIONS ] pip = use_extension("@rules_python//python/extensions:pip.bzl", "pip") diff --git a/ortools/base/BUILD.bazel b/ortools/base/BUILD.bazel index f1f205ec87..2e7d63e657 100644 --- a/ortools/base/BUILD.bazel +++ b/ortools/base/BUILD.bazel @@ -215,6 +215,19 @@ cc_library( ], ) +cc_library( + name = "fuzztest", + testonly = 1, + hdrs = ["fuzztest.h"], + deps = [ + "@com_google_absl//absl/log:check", + "@com_google_fuzztest//fuzztest", + "@com_google_fuzztest//fuzztest:googletest_fixture_adapter", + "@com_google_fuzztest//fuzztest:init_fuzztest", + "@com_google_protobuf//:protobuf", + ], +) + cc_library( name = "status_matchers", hdrs = ["status_matchers.h"], diff --git a/ortools/base/fuzztest.h b/ortools/base/fuzztest.h new file mode 100644 index 0000000000..675a3d7d33 --- /dev/null +++ b/ortools/base/fuzztest.h @@ -0,0 +1,55 @@ +// Copyright 2010-2024 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#ifndef OR_TOOLS_BASE_FUZZTEST_H_ +#define OR_TOOLS_BASE_FUZZTEST_H_ + +#include +#include +#include +#include +#include + +#include "fuzztest/domain.h" +#include "fuzztest/fuzztest.h" +#include "fuzztest/googletest_fixture_adapter.h" +#include "fuzztest/init_fuzztest.h" +#include "google/protobuf/message.h" +#include "google/protobuf/text_format.h" +#include "ortools/base/logging.h" + +namespace fuzztest { + +// Reads protos from directory and returns a vector usable by the .WithSeeds() +// function to aid in fuzz test migrations. `is_text_format` should be true iff +// the protos are in text format. +template +std::vector> ReadFilesFromDirectory( + std::string_view dir) { + std::vector> corpus; + + for (std::tuple& proto_tuple : ReadFilesFromDirectory(dir)) { + std::string text_proto = std::get<0>(proto_tuple); + ProtoType proto; + bool was_parsed = + google::protobuf::TextFormat::ParseFromString(text_proto, &proto); + if (was_parsed) { + corpus.push_back(std::make_tuple(proto)); + } + } + return corpus; +} + +} // namespace fuzztest + +#endif // OR_TOOLS_BASE_FUZZTEST_H_ diff --git a/ortools/sat/BUILD.bazel b/ortools/sat/BUILD.bazel index 3047678851..d668ed3c75 100644 --- a/ortools/sat/BUILD.bazel +++ b/ortools/sat/BUILD.bazel @@ -3743,6 +3743,22 @@ cc_test( ], ) +cc_test( + name = "cp_model_solver_fuzz", + size = "large", + srcs = ["cp_model_solver_fuzz.cc"], + data = glob(["fuzz_testdata/*"]), + deps = [ + ":cp_model_cc_proto", + ":cp_model_solver", + "//ortools/base:fuzztest", + "//ortools/base:path", + "@bazel_tools//tools/cpp/runfiles", + "@com_google_absl//absl/log:check", + "@com_google_fuzztest//fuzztest:fuzztest_gtest_main", + ], +) + cc_test( name = "flaky_models_test", size = "small", diff --git a/ortools/sat/CMakeLists.txt b/ortools/sat/CMakeLists.txt index ec3a1b22c3..a636beaeff 100644 --- a/ortools/sat/CMakeLists.txt +++ b/ortools/sat/CMakeLists.txt @@ -13,6 +13,7 @@ file(GLOB _SRCS "*.h" "*.cc") list(FILTER _SRCS EXCLUDE REGEX ".*/.*_test.cc") +list(FILTER _SRCS EXCLUDE REGEX ".*/.*_fuzz.cc") list(REMOVE_ITEM _SRCS ${CMAKE_CURRENT_SOURCE_DIR}/opb_reader.h ${CMAKE_CURRENT_SOURCE_DIR}/sat_cnf_reader.h diff --git a/ortools/sat/cp_model_solver_fuzz.cc b/ortools/sat/cp_model_solver_fuzz.cc new file mode 100644 index 0000000000..35d69966d0 --- /dev/null +++ b/ortools/sat/cp_model_solver_fuzz.cc @@ -0,0 +1,69 @@ +// Copyright 2010-2024 Google LLC +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include + +#include "absl/log/check.h" +#include "gtest/gtest.h" // IWYU pragma: keep +#include "ortools/base/fuzztest.h" +#include "ortools/base/path.h" // IWYU pragma: keep +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "tools/cpp/runfiles/runfiles.h" + +namespace operations_research::sat { + +namespace { + +std::string GetTestDataDir() { + return file::JoinPathRespectAbsolute(::testing::SrcDir(), + "_main/ortools/sat/fuzz_testdata"); +} + +void Solve(const CpModelProto& proto) { + const CpSolverResponse response = + operations_research::sat::SolveWithParameters(proto, + "max_time_in_seconds: 4.0"); + + const CpSolverResponse response_no_presolve = + operations_research::sat::SolveWithParameters( + proto, "max_time_in_seconds:4.0,cp_model_presolve:false"); + + CHECK_EQ(response.status() == CpSolverStatus::MODEL_INVALID, + response_no_presolve.status() == CpSolverStatus::MODEL_INVALID) + << "Model being invalid should not depend on presolve"; + + if (response.status() == CpSolverStatus::MODEL_INVALID) { + return; + } + + if (response.status() == CpSolverStatus::UNKNOWN || + response_no_presolve.status() == CpSolverStatus::UNKNOWN) { + return; + } + + CHECK_EQ(response.status() == CpSolverStatus::INFEASIBLE, + response_no_presolve.status() == CpSolverStatus::INFEASIBLE) + << "Presolve should not change feasibility"; +} + +// Fuzzing repeats solve() 100 times, and timeout after 600s. +// With a time limit of 4s, we should be fine. +FUZZ_TEST(CpModelProtoFuzzer, Solve) + .WithDomains(/*proto:*/ fuzztest::Arbitrary()) + .WithSeeds([]() { + return fuzztest::ReadFilesFromDirectory(GetTestDataDir()); + }); + +} // namespace +} // namespace operations_research::sat diff --git a/ortools/sat/fuzz_testdata/BadHintWithCore b/ortools/sat/fuzz_testdata/BadHintWithCore new file mode 100644 index 0000000000..a80bf4a5bd --- /dev/null +++ b/ortools/sat/fuzz_testdata/BadHintWithCore @@ -0,0 +1,38 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 5 +} +variables { + domain: 0 + domain: 5 +} +variables { + domain: 2 + domain: 8 +} +constraints { + linear { + vars: 0 + vars: 1 + vars: 2 + coeffs: 1 + coeffs: 1 + coeffs: -1 + domain: 0 + domain: 0 + } +} +objective { + vars: 2 + scaling_factor: 1 + coeffs: 1 +} +solution_hint { + vars: 0 + vars: 1 + values: 4 + values: 5 +} diff --git a/ortools/sat/fuzz_testdata/DualConnectedComponentsModel b/ortools/sat/fuzz_testdata/DualConnectedComponentsModel new file mode 100644 index 0000000000..a94c2cbab4 --- /dev/null +++ b/ortools/sat/fuzz_testdata/DualConnectedComponentsModel @@ -0,0 +1,70 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 1 + domain: 10 +} +variables { + domain: 1 + domain: 10 +} +variables { + domain: 1 + domain: 10 +} +variables { + domain: 1 + domain: 10 +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 1 + coeffs: 2 + domain: 0 + domain: 8 + } +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 1 + coeffs: 1 + domain: 2 + domain: 20 + } +} +constraints { + linear { + vars: 2 + vars: 3 + coeffs: 1 + coeffs: 2 + domain: 0 + domain: 6 + } +} +constraints { + linear { + vars: 2 + vars: 3 + coeffs: 1 + coeffs: 1 + domain: 2 + domain: 20 + } +} +objective { + vars: -1 + vars: -2 + vars: -3 + vars: -4 + scaling_factor: -1 + coeffs: 1 + coeffs: 2 + coeffs: 3 + coeffs: 4 +} diff --git a/ortools/sat/fuzz_testdata/EnumerateAllSolutions b/ortools/sat/fuzz_testdata/EnumerateAllSolutions new file mode 100644 index 0000000000..ff90cb400c --- /dev/null +++ b/ortools/sat/fuzz_testdata/EnumerateAllSolutions @@ -0,0 +1,27 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 1 + domain: 4 +} +variables { + domain: 1 + domain: 4 +} +variables { + domain: 1 + domain: 4 +} +variables { + domain: 1 + domain: 4 +} +constraints { + all_diff { + exprs { + vars: [0, 1, 2, 3] + coeffs: [1, 1, 1, 1] + } + } +} diff --git a/ortools/sat/fuzz_testdata/EnumerateAllSolutionsBis b/ortools/sat/fuzz_testdata/EnumerateAllSolutionsBis new file mode 100644 index 0000000000..9fb226f29a --- /dev/null +++ b/ortools/sat/fuzz_testdata/EnumerateAllSolutionsBis @@ -0,0 +1,21 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 5 +} +variables { + domain: 0 + domain: 5 +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 1 + coeffs: 1 + domain: 6 + domain: 6 + } +} diff --git a/ortools/sat/fuzz_testdata/EnumerateAllSolutionsOfEmptyModel b/ortools/sat/fuzz_testdata/EnumerateAllSolutionsOfEmptyModel new file mode 100644 index 0000000000..c362ee8e5b --- /dev/null +++ b/ortools/sat/fuzz_testdata/EnumerateAllSolutionsOfEmptyModel @@ -0,0 +1,15 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 2 +} +variables { + domain: 0 + domain: 2 +} +variables { + domain: 0 + domain: 2 +} diff --git a/ortools/sat/fuzz_testdata/HintWithCore b/ortools/sat/fuzz_testdata/HintWithCore new file mode 100644 index 0000000000..c7c051ed10 --- /dev/null +++ b/ortools/sat/fuzz_testdata/HintWithCore @@ -0,0 +1,34 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 5 +} +variables { + domain: 0 + domain: 5 +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 1 + coeffs: 1 + domain: 2 + domain: 8 + } +} +objective { + vars: 0 + vars: 1 + scaling_factor: 1 + coeffs: 1 + coeffs: 1 +} +solution_hint { + vars: 0 + vars: 1 + values: 2 + values: 3 +} diff --git a/ortools/sat/fuzz_testdata/InvalidProblem b/ortools/sat/fuzz_testdata/InvalidProblem new file mode 100644 index 0000000000..4aa225e1db --- /dev/null +++ b/ortools/sat/fuzz_testdata/InvalidProblem @@ -0,0 +1,5 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { +} diff --git a/ortools/sat/fuzz_testdata/MultipleEnforcementLiteral b/ortools/sat/fuzz_testdata/MultipleEnforcementLiteral new file mode 100644 index 0000000000..ac3446011d --- /dev/null +++ b/ortools/sat/fuzz_testdata/MultipleEnforcementLiteral @@ -0,0 +1,31 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 4 +} +variables { + domain: 0 + domain: 4 +} +constraints { + enforcement_literal: 0 + enforcement_literal: 1 + linear { + vars: 2 + vars: 3 + coeffs: 1 + coeffs: -1 + domain: 0 + domain: 0 + } +} diff --git a/ortools/sat/fuzz_testdata/NonInstantiatedVariables b/ortools/sat/fuzz_testdata/NonInstantiatedVariables new file mode 100644 index 0000000000..29bff4ad1b --- /dev/null +++ b/ortools/sat/fuzz_testdata/NonInstantiatedVariables @@ -0,0 +1,21 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 10 +} +variables { + domain: 0 + domain: 10 +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 1 + coeffs: 1 + domain: 4 + domain: 5 + } +} diff --git a/ortools/sat/fuzz_testdata/ObjectiveDomainLowerBound b/ortools/sat/fuzz_testdata/ObjectiveDomainLowerBound new file mode 100644 index 0000000000..2b41ef772e --- /dev/null +++ b/ortools/sat/fuzz_testdata/ObjectiveDomainLowerBound @@ -0,0 +1,27 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 1 + domain: 10 +} +variables { + domain: 1 + domain: 10 +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 2 + coeffs: 1 + domain: 10 + domain: 10 + } +} +objective { + vars: 1 + coeffs: 1 + domain: 8 + domain: 10 +} diff --git a/ortools/sat/fuzz_testdata/PureSatProblem b/ortools/sat/fuzz_testdata/PureSatProblem new file mode 100644 index 0000000000..8d80724abd --- /dev/null +++ b/ortools/sat/fuzz_testdata/PureSatProblem @@ -0,0 +1,2504 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +name: "Random 3-SAT" +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +constraints { + bool_or { + literals: 92 + literals: 32 + literals: -92 + } +} +constraints { + bool_or { + literals: 14 + literals: -55 + literals: 73 + } +} +constraints { + bool_or { + literals: 97 + literals: 28 + literals: -21 + } +} +constraints { + bool_or { + literals: -51 + literals: -97 + literals: -75 + } +} +constraints { + bool_or { + literals: 99 + literals: 98 + literals: 3 + } +} +constraints { + bool_or { + literals: 27 + literals: -76 + literals: 8 + } +} +constraints { + bool_or { + literals: -98 + literals: 74 + literals: -50 + } +} +constraints { + bool_or { + literals: -51 + literals: -67 + literals: 43 + } +} +constraints { + bool_or { + literals: -100 + literals: 23 + literals: -12 + } +} +constraints { + bool_or { + literals: -33 + literals: 79 + literals: 28 + } +} +constraints { + bool_or { + literals: -24 + literals: -63 + literals: -52 + } +} +constraints { + bool_or { + literals: 61 + literals: 80 + literals: 44 + } +} +constraints { + bool_or { + literals: 0 + literals: -21 + literals: 88 + } +} +constraints { + bool_or { + literals: 30 + literals: 19 + literals: -43 + } +} +constraints { + bool_or { + literals: -13 + literals: -30 + literals: 19 + } +} +constraints { + bool_or { + literals: -17 + literals: 82 + literals: 21 + } +} +constraints { + bool_or { + literals: -34 + literals: 51 + literals: 35 + } +} +constraints { + bool_or { + literals: -11 + literals: 35 + literals: 41 + } +} +constraints { + bool_or { + literals: 38 + literals: -39 + literals: 30 + } +} +constraints { + bool_or { + literals: -3 + literals: 38 + literals: 91 + } +} +constraints { + bool_or { + literals: -41 + literals: -2 + literals: -7 + } +} +constraints { + bool_or { + literals: 13 + literals: 62 + literals: -64 + } +} +constraints { + bool_or { + literals: 34 + literals: -20 + literals: 66 + } +} +constraints { + bool_or { + literals: -68 + literals: -46 + literals: -45 + } +} +constraints { + bool_or { + literals: -68 + literals: -13 + literals: 15 + } +} +constraints { + bool_or { + literals: -27 + literals: -30 + literals: 61 + } +} +constraints { + bool_or { + literals: -75 + literals: -89 + literals: 99 + } +} +constraints { + bool_or { + literals: 15 + literals: -68 + literals: -1 + } +} +constraints { + bool_or { + literals: -62 + literals: 82 + literals: 8 + } +} +constraints { + bool_or { + literals: 76 + literals: -21 + literals: -27 + } +} +constraints { + bool_or { + literals: 16 + literals: -65 + literals: 2 + } +} +constraints { + bool_or { + literals: -49 + literals: 64 + literals: -9 + } +} +constraints { + bool_or { + literals: -70 + literals: -82 + literals: 63 + } +} +constraints { + bool_or { + literals: -21 + literals: -39 + literals: -85 + } +} +constraints { + bool_or { + literals: 44 + literals: 28 + literals: 96 + } +} +constraints { + bool_or { + literals: 88 + literals: -32 + literals: 85 + } +} +constraints { + bool_or { + literals: -92 + literals: -76 + literals: -75 + } +} +constraints { + bool_or { + literals: -5 + literals: 42 + literals: -18 + } +} +constraints { + bool_or { + literals: -54 + literals: 90 + literals: 28 + } +} +constraints { + bool_or { + literals: 24 + literals: -71 + literals: -90 + } +} +constraints { + bool_or { + literals: 82 + literals: -19 + literals: -13 + } +} +constraints { + bool_or { + literals: -15 + literals: -62 + literals: -37 + } +} +constraints { + bool_or { + literals: -54 + literals: 75 + literals: -99 + } +} +constraints { + bool_or { + literals: 23 + literals: -21 + literals: 12 + } +} +constraints { + bool_or { + literals: -86 + literals: -41 + literals: 16 + } +} +constraints { + bool_or { + literals: -65 + literals: 13 + literals: 56 + } +} +constraints { + bool_or { + literals: -80 + literals: -71 + literals: -19 + } +} +constraints { + bool_or { + literals: 98 + literals: 88 + literals: 66 + } +} +constraints { + bool_or { + literals: -71 + literals: 48 + literals: -42 + } +} +constraints { + bool_or { + literals: 61 + literals: -32 + literals: -65 + } +} +constraints { + bool_or { + literals: -77 + literals: 13 + literals: -68 + } +} +constraints { + bool_or { + literals: 21 + literals: -49 + literals: 2 + } +} +constraints { + bool_or { + literals: 82 + literals: 99 + literals: -57 + } +} +constraints { + bool_or { + literals: 6 + literals: 14 + literals: 5 + } +} +constraints { + bool_or { + literals: 74 + literals: 79 + literals: 91 + } +} +constraints { + bool_or { + literals: -75 + literals: 47 + literals: -37 + } +} +constraints { + bool_or { + literals: 52 + literals: 94 + literals: 48 + } +} +constraints { + bool_or { + literals: 93 + literals: 33 + literals: -91 + } +} +constraints { + bool_or { + literals: 54 + literals: 41 + literals: 46 + } +} +constraints { + bool_or { + literals: 55 + literals: 30 + literals: 75 + } +} +constraints { + bool_or { + literals: -69 + literals: 68 + literals: -6 + } +} +constraints { + bool_or { + literals: -72 + literals: -43 + literals: -22 + } +} +constraints { + bool_or { + literals: 27 + literals: -18 + literals: -44 + } +} +constraints { + bool_or { + literals: -68 + literals: -6 + literals: 84 + } +} +constraints { + bool_or { + literals: -14 + literals: -65 + literals: 36 + } +} +constraints { + bool_or { + literals: 56 + literals: 42 + literals: 46 + } +} +constraints { + bool_or { + literals: -95 + literals: 11 + literals: 15 + } +} +constraints { + bool_or { + literals: -23 + literals: -70 + literals: -44 + } +} +constraints { + bool_or { + literals: 31 + literals: -4 + literals: 76 + } +} +constraints { + bool_or { + literals: -85 + literals: -71 + literals: 8 + } +} +constraints { + bool_or { + literals: 56 + literals: -6 + literals: -14 + } +} +constraints { + bool_or { + literals: 90 + literals: -80 + literals: 91 + } +} +constraints { + bool_or { + literals: 78 + literals: -72 + literals: -86 + } +} +constraints { + bool_or { + literals: -27 + literals: -65 + literals: -92 + } +} +constraints { + bool_or { + literals: 85 + literals: 53 + literals: -51 + } +} +constraints { + bool_or { + literals: -64 + literals: 68 + literals: -21 + } +} +constraints { + bool_or { + literals: -74 + literals: 80 + literals: -73 + } +} +constraints { + bool_or { + literals: -23 + literals: 60 + literals: 74 + } +} +constraints { + bool_or { + literals: -89 + literals: -19 + literals: -67 + } +} +constraints { + bool_or { + literals: 48 + literals: -46 + literals: -8 + } +} +constraints { + bool_or { + literals: -39 + literals: -6 + literals: -60 + } +} +constraints { + bool_or { + literals: 28 + literals: 13 + literals: -31 + } +} +constraints { + bool_or { + literals: 48 + literals: 11 + literals: -62 + } +} +constraints { + bool_or { + literals: -63 + literals: 75 + literals: -25 + } +} +constraints { + bool_or { + literals: -83 + literals: 4 + literals: 49 + } +} +constraints { + bool_or { + literals: 29 + literals: 10 + literals: 77 + } +} +constraints { + bool_or { + literals: 58 + literals: 86 + literals: -25 + } +} +constraints { + bool_or { + literals: -20 + literals: -82 + literals: 86 + } +} +constraints { + bool_or { + literals: -1 + literals: -73 + literals: -50 + } +} +constraints { + bool_or { + literals: 15 + literals: 38 + literals: -46 + } +} +constraints { + bool_or { + literals: 91 + literals: -79 + literals: 55 + } +} +constraints { + bool_or { + literals: 64 + literals: -54 + literals: 54 + } +} +constraints { + bool_or { + literals: -56 + literals: 95 + literals: 74 + } +} +constraints { + bool_or { + literals: -90 + literals: -8 + literals: 52 + } +} +constraints { + bool_or { + literals: 46 + literals: 40 + literals: -57 + } +} +constraints { + bool_or { + literals: -10 + literals: 51 + literals: -67 + } +} +constraints { + bool_or { + literals: -35 + literals: -74 + literals: 50 + } +} +constraints { + bool_or { + literals: 38 + literals: -29 + literals: 58 + } +} +constraints { + bool_or { + literals: 70 + literals: -42 + literals: 36 + } +} +constraints { + bool_or { + literals: -67 + literals: -59 + literals: -91 + } +} +constraints { + bool_or { + literals: -9 + literals: 53 + literals: 57 + } +} +constraints { + bool_or { + literals: 58 + literals: -5 + literals: -60 + } +} +constraints { + bool_or { + literals: -93 + literals: 67 + literals: -8 + } +} +constraints { + bool_or { + literals: -42 + literals: -69 + literals: -32 + } +} +constraints { + bool_or { + literals: 34 + literals: -45 + literals: -56 + } +} +constraints { + bool_or { + literals: -20 + literals: 89 + literals: -65 + } +} +constraints { + bool_or { + literals: -6 + literals: 4 + literals: -38 + } +} +constraints { + bool_or { + literals: -95 + literals: 70 + literals: -20 + } +} +constraints { + bool_or { + literals: 35 + literals: -89 + literals: 37 + } +} +constraints { + bool_or { + literals: 93 + literals: -2 + literals: 19 + } +} +constraints { + bool_or { + literals: 16 + literals: 66 + literals: 34 + } +} +constraints { + bool_or { + literals: 15 + literals: 74 + literals: -20 + } +} +constraints { + bool_or { + literals: 72 + literals: -68 + literals: 85 + } +} +constraints { + bool_or { + literals: -87 + literals: 8 + literals: -2 + } +} +constraints { + bool_or { + literals: -36 + literals: 39 + literals: -52 + } +} +constraints { + bool_or { + literals: -39 + literals: -87 + literals: 34 + } +} +constraints { + bool_or { + literals: -31 + literals: 49 + literals: -37 + } +} +constraints { + bool_or { + literals: -59 + literals: 53 + literals: 79 + } +} +constraints { + bool_or { + literals: -45 + literals: -52 + literals: -9 + } +} +constraints { + bool_or { + literals: 30 + literals: -76 + literals: 36 + } +} +constraints { + bool_or { + literals: 50 + literals: -26 + literals: 94 + } +} +constraints { + bool_or { + literals: -32 + literals: 13 + literals: -29 + } +} +constraints { + bool_or { + literals: -18 + literals: 50 + literals: -28 + } +} +constraints { + bool_or { + literals: 82 + literals: -71 + literals: 97 + } +} +constraints { + bool_or { + literals: -70 + literals: 15 + literals: -91 + } +} +constraints { + bool_or { + literals: 88 + literals: 8 + literals: 91 + } +} +constraints { + bool_or { + literals: -52 + literals: -90 + literals: 52 + } +} +constraints { + bool_or { + literals: -83 + literals: -20 + literals: -49 + } +} +constraints { + bool_or { + literals: 30 + literals: 75 + literals: -61 + } +} +constraints { + bool_or { + literals: -61 + literals: 56 + literals: 36 + } +} +constraints { + bool_or { + literals: 36 + literals: 7 + literals: -75 + } +} +constraints { + bool_or { + literals: 36 + literals: -84 + literals: -86 + } +} +constraints { + bool_or { + literals: 16 + literals: -55 + literals: 93 + } +} +constraints { + bool_or { + literals: 53 + literals: -47 + literals: -69 + } +} +constraints { + bool_or { + literals: -18 + literals: 30 + literals: 47 + } +} +constraints { + bool_or { + literals: -68 + literals: 8 + literals: -86 + } +} +constraints { + bool_or { + literals: -9 + literals: -15 + literals: -62 + } +} +constraints { + bool_or { + literals: -98 + literals: -88 + literals: -25 + } +} +constraints { + bool_or { + literals: 21 + literals: -76 + literals: 49 + } +} +constraints { + bool_or { + literals: -13 + literals: -32 + literals: -37 + } +} +constraints { + bool_or { + literals: -69 + literals: -71 + literals: -28 + } +} +constraints { + bool_or { + literals: -80 + literals: 25 + literals: -100 + } +} +constraints { + bool_or { + literals: 37 + literals: -27 + literals: -19 + } +} +constraints { + bool_or { + literals: -66 + literals: 0 + literals: 67 + } +} +constraints { + bool_or { + literals: 89 + literals: -75 + literals: 49 + } +} +constraints { + bool_or { + literals: 34 + literals: -44 + literals: 59 + } +} +constraints { + bool_or { + literals: -9 + literals: -80 + literals: 70 + } +} +constraints { + bool_or { + literals: 86 + literals: -55 + literals: -37 + } +} +constraints { + bool_or { + literals: -34 + literals: 15 + literals: -12 + } +} +constraints { + bool_or { + literals: -42 + literals: 27 + literals: -49 + } +} +constraints { + bool_or { + literals: 60 + literals: -91 + literals: 62 + } +} +constraints { + bool_or { + literals: 13 + literals: 65 + literals: 44 + } +} +constraints { + bool_or { + literals: -79 + literals: -80 + literals: 44 + } +} +constraints { + bool_or { + literals: -84 + literals: 14 + literals: 37 + } +} +constraints { + bool_or { + literals: 35 + literals: 58 + literals: -38 + } +} +constraints { + bool_or { + literals: 60 + literals: -41 + literals: -32 + } +} +constraints { + bool_or { + literals: -81 + literals: 77 + literals: -18 + } +} +constraints { + bool_or { + literals: -73 + literals: 10 + literals: -74 + } +} +constraints { + bool_or { + literals: 0 + literals: 19 + literals: 83 + } +} +constraints { + bool_or { + literals: 0 + literals: 33 + literals: -42 + } +} +constraints { + bool_or { + literals: -18 + literals: 1 + literals: 18 + } +} +constraints { + bool_or { + literals: -77 + literals: -72 + literals: -24 + } +} +constraints { + bool_or { + literals: 66 + literals: -5 + literals: -84 + } +} +constraints { + bool_or { + literals: 20 + literals: 36 + literals: -18 + } +} +constraints { + bool_or { + literals: 32 + literals: 90 + literals: 43 + } +} +constraints { + bool_or { + literals: -84 + literals: -87 + literals: 15 + } +} +constraints { + bool_or { + literals: 35 + literals: -13 + literals: 47 + } +} +constraints { + bool_or { + literals: -4 + literals: 93 + literals: -30 + } +} +constraints { + bool_or { + literals: -12 + literals: -51 + literals: 81 + } +} +constraints { + bool_or { + literals: 48 + literals: 6 + literals: 41 + } +} +constraints { + bool_or { + literals: 10 + literals: 56 + literals: -27 + } +} +constraints { + bool_or { + literals: 28 + literals: 23 + literals: -62 + } +} +constraints { + bool_or { + literals: -8 + literals: 7 + literals: -30 + } +} +constraints { + bool_or { + literals: -87 + literals: -15 + literals: 39 + } +} +constraints { + bool_or { + literals: 96 + literals: 36 + literals: 69 + } +} +constraints { + bool_or { + literals: 91 + literals: -55 + literals: -73 + } +} +constraints { + bool_or { + literals: -44 + literals: -88 + literals: -18 + } +} +constraints { + bool_or { + literals: 1 + literals: 24 + literals: -6 + } +} +constraints { + bool_or { + literals: 90 + literals: -36 + literals: -11 + } +} +constraints { + bool_or { + literals: -100 + literals: -70 + literals: -33 + } +} +constraints { + bool_or { + literals: 78 + literals: -46 + literals: -26 + } +} +constraints { + bool_or { + literals: 63 + literals: -10 + literals: 71 + } +} +constraints { + bool_or { + literals: 94 + literals: 24 + literals: -4 + } +} +constraints { + bool_or { + literals: -70 + literals: 86 + literals: 29 + } +} +constraints { + bool_or { + literals: 84 + literals: -12 + literals: 97 + } +} +constraints { + bool_or { + literals: 47 + literals: 31 + literals: 17 + } +} +constraints { + bool_or { + literals: 97 + literals: 30 + literals: -36 + } +} +constraints { + bool_or { + literals: 50 + literals: -49 + literals: 42 + } +} +constraints { + bool_or { + literals: -92 + literals: -71 + literals: -43 + } +} +constraints { + bool_or { + literals: 15 + literals: 73 + literals: 25 + } +} +constraints { + bool_or { + literals: -73 + literals: -5 + literals: 59 + } +} +constraints { + bool_or { + literals: -91 + literals: 27 + literals: 62 + } +} +constraints { + bool_or { + literals: 94 + literals: 39 + literals: 0 + } +} +constraints { + bool_or { + literals: 78 + literals: -84 + literals: -83 + } +} +constraints { + bool_or { + literals: -57 + literals: -8 + literals: -24 + } +} +constraints { + bool_or { + literals: 41 + literals: -5 + literals: -17 + } +} +constraints { + bool_or { + literals: 29 + literals: 85 + literals: -98 + } +} +constraints { + bool_or { + literals: 63 + literals: -48 + literals: 61 + } +} +constraints { + bool_or { + literals: -16 + literals: -71 + literals: 42 + } +} +constraints { + bool_or { + literals: -4 + literals: -60 + literals: 49 + } +} +constraints { + bool_or { + literals: -76 + literals: 58 + literals: 78 + } +} +constraints { + bool_or { + literals: 90 + literals: -48 + literals: -86 + } +} +constraints { + bool_or { + literals: 7 + literals: 11 + literals: -15 + } +} +constraints { + bool_or { + literals: 93 + literals: -27 + literals: 68 + } +} +constraints { + bool_or { + literals: -100 + literals: 59 + literals: 9 + } +} +constraints { + bool_or { + literals: 14 + literals: 29 + literals: -88 + } +} +constraints { + bool_or { + literals: 10 + literals: -46 + literals: -34 + } +} +constraints { + bool_or { + literals: -86 + literals: 11 + literals: 36 + } +} +constraints { + bool_or { + literals: 53 + literals: -93 + literals: -51 + } +} +constraints { + bool_or { + literals: -13 + literals: -55 + literals: -15 + } +} +constraints { + bool_or { + literals: 24 + literals: 15 + literals: -16 + } +} +constraints { + bool_or { + literals: 82 + literals: 7 + literals: 66 + } +} +constraints { + bool_or { + literals: 99 + literals: -93 + literals: 1 + } +} +constraints { + bool_or { + literals: -95 + literals: 84 + literals: -86 + } +} +constraints { + bool_or { + literals: -18 + literals: -16 + literals: -69 + } +} +constraints { + bool_or { + literals: 67 + literals: -100 + literals: 46 + } +} +constraints { + bool_or { + literals: 74 + literals: 64 + literals: 5 + } +} +constraints { + bool_or { + literals: -26 + literals: -5 + literals: -43 + } +} +constraints { + bool_or { + literals: -1 + literals: -64 + literals: -6 + } +} +constraints { + bool_or { + literals: 90 + literals: 89 + literals: 43 + } +} +constraints { + bool_or { + literals: 58 + literals: -30 + literals: -35 + } +} +constraints { + bool_or { + literals: 84 + literals: -98 + literals: 94 + } +} +constraints { + bool_or { + literals: -27 + literals: 55 + literals: 43 + } +} +constraints { + bool_or { + literals: -95 + literals: -35 + literals: -19 + } +} +constraints { + bool_or { + literals: 58 + literals: -9 + literals: 87 + } +} +constraints { + bool_or { + literals: 34 + literals: -60 + literals: -31 + } +} +constraints { + bool_or { + literals: -94 + literals: -43 + literals: -78 + } +} +constraints { + bool_or { + literals: 5 + literals: 23 + literals: -38 + } +} +constraints { + bool_or { + literals: 71 + literals: -23 + literals: -95 + } +} +constraints { + bool_or { + literals: -12 + literals: 12 + literals: -96 + } +} +constraints { + bool_or { + literals: -26 + literals: 98 + literals: -96 + } +} +constraints { + bool_or { + literals: 4 + literals: 59 + literals: -82 + } +} +constraints { + bool_or { + literals: -20 + literals: 30 + literals: 97 + } +} +constraints { + bool_or { + literals: -1 + literals: 60 + literals: 76 + } +} +constraints { + bool_or { + literals: -98 + literals: 72 + literals: -90 + } +} +constraints { + bool_or { + literals: -45 + literals: 62 + literals: -10 + } +} +constraints { + bool_or { + literals: 63 + literals: -85 + literals: -24 + } +} +constraints { + bool_or { + literals: -38 + literals: -49 + literals: -99 + } +} +constraints { + bool_or { + literals: -79 + literals: -56 + literals: 60 + } +} +constraints { + bool_or { + literals: -9 + literals: 74 + literals: -71 + } +} +constraints { + bool_or { + literals: 81 + literals: 21 + literals: -98 + } +} +constraints { + bool_or { + literals: -94 + literals: -86 + literals: 9 + } +} +constraints { + bool_or { + literals: -98 + literals: -37 + literals: 48 + } +} +constraints { + bool_or { + literals: -8 + literals: 34 + literals: 41 + } +} +constraints { + bool_or { + literals: -91 + literals: 71 + literals: -100 + } +} +constraints { + bool_or { + literals: -95 + literals: 34 + literals: 72 + } +} +constraints { + bool_or { + literals: -90 + literals: -77 + literals: -67 + } +} +constraints { + bool_or { + literals: 59 + literals: -18 + literals: -77 + } +} +constraints { + bool_or { + literals: -81 + literals: -14 + literals: 37 + } +} +constraints { + bool_or { + literals: 31 + literals: 61 + literals: 34 + } +} +constraints { + bool_or { + literals: -98 + literals: -28 + literals: -84 + } +} +constraints { + bool_or { + literals: -86 + literals: -66 + literals: 92 + } +} +constraints { + bool_or { + literals: -49 + literals: -76 + literals: 66 + } +} +constraints { + bool_or { + literals: 6 + literals: -100 + literals: 32 + } +} +constraints { + bool_or { + literals: -100 + literals: 45 + literals: 53 + } +} +constraints { + bool_or { + literals: -79 + literals: 72 + literals: -25 + } +} +constraints { + bool_or { + literals: -27 + literals: -61 + literals: -83 + } +} +constraints { + bool_or { + literals: -95 + literals: -40 + literals: -76 + } +} +constraints { + bool_or { + literals: 80 + literals: 9 + literals: -58 + } +} +constraints { + bool_or { + literals: 62 + literals: -41 + literals: 14 + } +} +constraints { + bool_or { + literals: -14 + literals: 81 + literals: 80 + } +} +constraints { + bool_or { + literals: 46 + literals: 25 + literals: 65 + } +} +constraints { + bool_or { + literals: -22 + literals: 43 + literals: 67 + } +} +constraints { + bool_or { + literals: -44 + literals: -100 + literals: 27 + } +} +constraints { + bool_or { + literals: -56 + literals: 6 + literals: -77 + } +} +constraints { + bool_or { + literals: -59 + literals: 79 + literals: 76 + } +} +constraints { + bool_or { + literals: -81 + literals: 45 + literals: -85 + } +} +constraints { + bool_or { + literals: 98 + literals: -75 + literals: 4 + } +} +constraints { + bool_or { + literals: -73 + literals: -41 + literals: 80 + } +} +constraints { + bool_or { + literals: -3 + literals: 92 + literals: 18 + } +} +constraints { + bool_or { + literals: 11 + literals: 49 + literals: -5 + } +} +constraints { + bool_or { + literals: 37 + literals: 16 + literals: -25 + } +} +constraints { + bool_or { + literals: 77 + literals: -17 + literals: 74 + } +} +constraints { + bool_or { + literals: -44 + literals: -77 + literals: 47 + } +} +constraints { + bool_or { + literals: 72 + literals: 95 + literals: 45 + } +} +constraints { + bool_or { + literals: 99 + literals: -33 + literals: -78 + } +} +constraints { + bool_or { + literals: -20 + literals: 84 + literals: -69 + } +} +constraints { + bool_or { + literals: 99 + literals: -32 + literals: 84 + } +} +constraints { + bool_or { + literals: 14 + literals: -39 + literals: 39 + } +} +constraints { + bool_or { + literals: 21 + literals: 32 + literals: -63 + } +} +constraints { + bool_or { + literals: -10 + literals: -57 + literals: -25 + } +} +constraints { + bool_or { + literals: 22 + literals: -44 + literals: 16 + } +} +constraints { + bool_or { + literals: 90 + literals: -78 + literals: 25 + } +} +constraints { + bool_or { + literals: 98 + literals: -24 + literals: 47 + } +} +constraints { + bool_or { + literals: 77 + literals: -13 + literals: -78 + } +} +constraints { + bool_or { + literals: -3 + literals: -41 + literals: 96 + } +} +constraints { + bool_or { + literals: -78 + literals: 74 + literals: -82 + } +} +constraints { + bool_or { + literals: 4 + literals: -100 + literals: 97 + } +} +constraints { + bool_or { + literals: 96 + literals: -6 + literals: -37 + } +} +constraints { + bool_or { + literals: 64 + literals: 29 + literals: -25 + } +} +constraints { + bool_or { + literals: -82 + literals: 29 + literals: 95 + } +} +constraints { + bool_or { + literals: -37 + literals: -58 + literals: -53 + } +} +constraints { + bool_or { + literals: 34 + literals: 82 + literals: 20 + } +} +constraints { + bool_or { + literals: 42 + literals: 98 + literals: 31 + } +} +constraints { + bool_or { + literals: -99 + literals: 82 + literals: -7 + } +} +constraints { + bool_or { + literals: -91 + literals: -28 + literals: -39 + } +} +constraints { + bool_or { + literals: -93 + literals: 3 + literals: -24 + } +} +constraints { + bool_or { + literals: 74 + literals: 84 + literals: -92 + } +} +constraints { + bool_or { + literals: -60 + literals: -84 + literals: 0 + } +} +constraints { + bool_or { + literals: 11 + literals: -22 + literals: -13 + } +} diff --git a/ortools/sat/fuzz_testdata/PureSatProblemWithLimit b/ortools/sat/fuzz_testdata/PureSatProblemWithLimit new file mode 100644 index 0000000000..057e77833b --- /dev/null +++ b/ortools/sat/fuzz_testdata/PureSatProblemWithLimit @@ -0,0 +1,3386 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +name: "Random 3-SAT" +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +constraints { + bool_or { + literals: 28 + literals: -72 + literals: -27 + } +} +constraints { + bool_or { + literals: -21 + literals: 99 + literals: 44 + } +} +constraints { + bool_or { + literals: 24 + literals: 30 + literals: 84 + } +} +constraints { + bool_or { + literals: -39 + literals: 5 + literals: 81 + } +} +constraints { + bool_or { + literals: -28 + literals: -91 + literals: -4 + } +} +constraints { + bool_or { + literals: 27 + literals: 98 + literals: -32 + } +} +constraints { + bool_or { + literals: -1 + literals: -99 + literals: 94 + } +} +constraints { + bool_or { + literals: -49 + literals: 87 + literals: -68 + } +} +constraints { + bool_or { + literals: 36 + literals: -4 + literals: -97 + } +} +constraints { + bool_or { + literals: 57 + literals: -45 + literals: 48 + } +} +constraints { + bool_or { + literals: -78 + literals: -16 + literals: -13 + } +} +constraints { + bool_or { + literals: 26 + literals: -61 + literals: 3 + } +} +constraints { + bool_or { + literals: -53 + literals: -90 + literals: 79 + } +} +constraints { + bool_or { + literals: 42 + literals: -80 + literals: -85 + } +} +constraints { + bool_or { + literals: -45 + literals: -27 + literals: -48 + } +} +constraints { + bool_or { + literals: -42 + literals: -23 + literals: 39 + } +} +constraints { + bool_or { + literals: -28 + literals: -33 + literals: 17 + } +} +constraints { + bool_or { + literals: -29 + literals: -85 + literals: -33 + } +} +constraints { + bool_or { + literals: -80 + literals: 94 + literals: 89 + } +} +constraints { + bool_or { + literals: -61 + literals: -91 + literals: 13 + } +} +constraints { + bool_or { + literals: -92 + literals: 64 + literals: 42 + } +} +constraints { + bool_or { + literals: 61 + literals: 87 + literals: -8 + } +} +constraints { + bool_or { + literals: 55 + literals: 52 + literals: 48 + } +} +constraints { + bool_or { + literals: 14 + literals: 77 + literals: 74 + } +} +constraints { + bool_or { + literals: -95 + literals: 16 + literals: -78 + } +} +constraints { + bool_or { + literals: -26 + literals: 56 + literals: -83 + } +} +constraints { + bool_or { + literals: -65 + literals: -78 + literals: 72 + } +} +constraints { + bool_or { + literals: -6 + literals: -93 + literals: 57 + } +} +constraints { + bool_or { + literals: -7 + literals: -3 + literals: 67 + } +} +constraints { + bool_or { + literals: 39 + literals: 14 + literals: -6 + } +} +constraints { + bool_or { + literals: -46 + literals: 93 + literals: 60 + } +} +constraints { + bool_or { + literals: 26 + literals: 67 + literals: 42 + } +} +constraints { + bool_or { + literals: 85 + literals: -22 + literals: -48 + } +} +constraints { + bool_or { + literals: -3 + literals: -55 + literals: -51 + } +} +constraints { + bool_or { + literals: 21 + literals: 41 + literals: 47 + } +} +constraints { + bool_or { + literals: -48 + literals: 0 + literals: -63 + } +} +constraints { + bool_or { + literals: 34 + literals: 37 + literals: -54 + } +} +constraints { + bool_or { + literals: 5 + literals: 1 + literals: 81 + } +} +constraints { + bool_or { + literals: 66 + literals: -98 + literals: -89 + } +} +constraints { + bool_or { + literals: 25 + literals: -41 + literals: 35 + } +} +constraints { + bool_or { + literals: 68 + literals: -28 + literals: -99 + } +} +constraints { + bool_or { + literals: 26 + literals: -36 + literals: -61 + } +} +constraints { + bool_or { + literals: -11 + literals: -36 + literals: 97 + } +} +constraints { + bool_or { + literals: 2 + literals: 45 + literals: 5 + } +} +constraints { + bool_or { + literals: -63 + literals: 30 + literals: 74 + } +} +constraints { + bool_or { + literals: -32 + literals: 55 + literals: -94 + } +} +constraints { + bool_or { + literals: -78 + literals: 30 + literals: 6 + } +} +constraints { + bool_or { + literals: 63 + literals: -16 + literals: 86 + } +} +constraints { + bool_or { + literals: -78 + literals: -72 + literals: -87 + } +} +constraints { + bool_or { + literals: -71 + literals: -50 + literals: 44 + } +} +constraints { + bool_or { + literals: -98 + literals: -13 + literals: 83 + } +} +constraints { + bool_or { + literals: -95 + literals: 59 + literals: 15 + } +} +constraints { + bool_or { + literals: 80 + literals: 84 + literals: -33 + } +} +constraints { + bool_or { + literals: 17 + literals: 83 + literals: -76 + } +} +constraints { + bool_or { + literals: 73 + literals: 2 + literals: -74 + } +} +constraints { + bool_or { + literals: -61 + literals: 77 + literals: 99 + } +} +constraints { + bool_or { + literals: -35 + literals: 21 + literals: 79 + } +} +constraints { + bool_or { + literals: -72 + literals: 21 + literals: 27 + } +} +constraints { + bool_or { + literals: 96 + literals: -29 + literals: 3 + } +} +constraints { + bool_or { + literals: -4 + literals: -61 + literals: 4 + } +} +constraints { + bool_or { + literals: 30 + literals: -27 + literals: 92 + } +} +constraints { + bool_or { + literals: -58 + literals: 49 + literals: 23 + } +} +constraints { + bool_or { + literals: -39 + literals: 60 + literals: 47 + } +} +constraints { + bool_or { + literals: -70 + literals: 53 + literals: -53 + } +} +constraints { + bool_or { + literals: 11 + literals: 71 + literals: 10 + } +} +constraints { + bool_or { + literals: 17 + literals: -83 + literals: 27 + } +} +constraints { + bool_or { + literals: -73 + literals: -41 + literals: -86 + } +} +constraints { + bool_or { + literals: 65 + literals: 5 + literals: -23 + } +} +constraints { + bool_or { + literals: 20 + literals: 60 + literals: 6 + } +} +constraints { + bool_or { + literals: 58 + literals: -76 + literals: -98 + } +} +constraints { + bool_or { + literals: 62 + literals: 42 + literals: 2 + } +} +constraints { + bool_or { + literals: 3 + literals: 9 + literals: 58 + } +} +constraints { + bool_or { + literals: -64 + literals: -89 + literals: 85 + } +} +constraints { + bool_or { + literals: -8 + literals: 11 + literals: 82 + } +} +constraints { + bool_or { + literals: 92 + literals: 64 + literals: 1 + } +} +constraints { + bool_or { + literals: -51 + literals: 56 + literals: 80 + } +} +constraints { + bool_or { + literals: 42 + literals: -5 + literals: -34 + } +} +constraints { + bool_or { + literals: 71 + literals: -21 + literals: -89 + } +} +constraints { + bool_or { + literals: 66 + literals: -75 + literals: -38 + } +} +constraints { + bool_or { + literals: 56 + literals: 19 + literals: 68 + } +} +constraints { + bool_or { + literals: -83 + literals: 73 + literals: 81 + } +} +constraints { + bool_or { + literals: -73 + literals: -88 + literals: 71 + } +} +constraints { + bool_or { + literals: -45 + literals: -8 + literals: -5 + } +} +constraints { + bool_or { + literals: 61 + literals: -56 + literals: 34 + } +} +constraints { + bool_or { + literals: 1 + literals: 3 + literals: 62 + } +} +constraints { + bool_or { + literals: -89 + literals: 85 + literals: -60 + } +} +constraints { + bool_or { + literals: -11 + literals: 91 + literals: 21 + } +} +constraints { + bool_or { + literals: -72 + literals: -5 + literals: -57 + } +} +constraints { + bool_or { + literals: -30 + literals: -97 + literals: 45 + } +} +constraints { + bool_or { + literals: -19 + literals: 30 + literals: -84 + } +} +constraints { + bool_or { + literals: -6 + literals: -25 + literals: 51 + } +} +constraints { + bool_or { + literals: 63 + literals: 26 + literals: 54 + } +} +constraints { + bool_or { + literals: 17 + literals: -82 + literals: -18 + } +} +constraints { + bool_or { + literals: 95 + literals: 49 + literals: 42 + } +} +constraints { + bool_or { + literals: 98 + literals: -28 + literals: -14 + } +} +constraints { + bool_or { + literals: -54 + literals: -4 + literals: -41 + } +} +constraints { + bool_or { + literals: 38 + literals: 62 + literals: 7 + } +} +constraints { + bool_or { + literals: 58 + literals: -66 + literals: -15 + } +} +constraints { + bool_or { + literals: -94 + literals: -78 + literals: -49 + } +} +constraints { + bool_or { + literals: -68 + literals: 53 + literals: 55 + } +} +constraints { + bool_or { + literals: -24 + literals: -81 + literals: -82 + } +} +constraints { + bool_or { + literals: 54 + literals: 31 + literals: 59 + } +} +constraints { + bool_or { + literals: 46 + literals: -16 + literals: -24 + } +} +constraints { + bool_or { + literals: 56 + literals: -29 + literals: -86 + } +} +constraints { + bool_or { + literals: 93 + literals: 57 + literals: 54 + } +} +constraints { + bool_or { + literals: 95 + literals: 78 + literals: 32 + } +} +constraints { + bool_or { + literals: 94 + literals: -100 + literals: 76 + } +} +constraints { + bool_or { + literals: 25 + literals: 72 + literals: -83 + } +} +constraints { + bool_or { + literals: -11 + literals: -17 + literals: 43 + } +} +constraints { + bool_or { + literals: 82 + literals: -52 + literals: -86 + } +} +constraints { + bool_or { + literals: -96 + literals: 90 + literals: -87 + } +} +constraints { + bool_or { + literals: -41 + literals: -32 + literals: -31 + } +} +constraints { + bool_or { + literals: 1 + literals: -99 + literals: 32 + } +} +constraints { + bool_or { + literals: 97 + literals: -43 + literals: -16 + } +} +constraints { + bool_or { + literals: -10 + literals: -83 + literals: -68 + } +} +constraints { + bool_or { + literals: 10 + literals: 47 + literals: -58 + } +} +constraints { + bool_or { + literals: -37 + literals: 70 + literals: 99 + } +} +constraints { + bool_or { + literals: 86 + literals: 8 + literals: 66 + } +} +constraints { + bool_or { + literals: 83 + literals: 44 + literals: 36 + } +} +constraints { + bool_or { + literals: -43 + literals: -25 + literals: -78 + } +} +constraints { + bool_or { + literals: -37 + literals: 91 + literals: -65 + } +} +constraints { + bool_or { + literals: 12 + literals: 29 + literals: 31 + } +} +constraints { + bool_or { + literals: -6 + literals: 76 + literals: -78 + } +} +constraints { + bool_or { + literals: 28 + literals: 62 + literals: -98 + } +} +constraints { + bool_or { + literals: -100 + literals: 7 + literals: 92 + } +} +constraints { + bool_or { + literals: 93 + literals: -44 + literals: 34 + } +} +constraints { + bool_or { + literals: -21 + literals: 3 + literals: 10 + } +} +constraints { + bool_or { + literals: 79 + literals: -84 + literals: 30 + } +} +constraints { + bool_or { + literals: 66 + literals: -59 + literals: 29 + } +} +constraints { + bool_or { + literals: -82 + literals: -35 + literals: -63 + } +} +constraints { + bool_or { + literals: -60 + literals: -80 + literals: 65 + } +} +constraints { + bool_or { + literals: -29 + literals: -64 + literals: -14 + } +} +constraints { + bool_or { + literals: 29 + literals: 76 + literals: -46 + } +} +constraints { + bool_or { + literals: 24 + literals: 93 + literals: 78 + } +} +constraints { + bool_or { + literals: 12 + literals: 32 + literals: 16 + } +} +constraints { + bool_or { + literals: -10 + literals: 46 + literals: -46 + } +} +constraints { + bool_or { + literals: -98 + literals: -29 + literals: 82 + } +} +constraints { + bool_or { + literals: 16 + literals: 62 + literals: -73 + } +} +constraints { + bool_or { + literals: 29 + literals: 85 + literals: 41 + } +} +constraints { + bool_or { + literals: -94 + literals: 72 + literals: 58 + } +} +constraints { + bool_or { + literals: -51 + literals: 44 + literals: 3 + } +} +constraints { + bool_or { + literals: -68 + literals: 12 + literals: -32 + } +} +constraints { + bool_or { + literals: 39 + literals: 70 + literals: 31 + } +} +constraints { + bool_or { + literals: 65 + literals: -71 + literals: -51 + } +} +constraints { + bool_or { + literals: -13 + literals: 87 + literals: -32 + } +} +constraints { + bool_or { + literals: -39 + literals: -37 + literals: 82 + } +} +constraints { + bool_or { + literals: -65 + literals: 19 + literals: -77 + } +} +constraints { + bool_or { + literals: -16 + literals: 16 + literals: -18 + } +} +constraints { + bool_or { + literals: 98 + literals: -23 + literals: 99 + } +} +constraints { + bool_or { + literals: -98 + literals: -60 + literals: 45 + } +} +constraints { + bool_or { + literals: 96 + literals: -89 + literals: -35 + } +} +constraints { + bool_or { + literals: 61 + literals: 14 + literals: 54 + } +} +constraints { + bool_or { + literals: 35 + literals: 4 + literals: 63 + } +} +constraints { + bool_or { + literals: -4 + literals: 59 + literals: -35 + } +} +constraints { + bool_or { + literals: 40 + literals: -78 + literals: 91 + } +} +constraints { + bool_or { + literals: 81 + literals: 5 + literals: -57 + } +} +constraints { + bool_or { + literals: 41 + literals: 83 + literals: -68 + } +} +constraints { + bool_or { + literals: 27 + literals: 32 + literals: 51 + } +} +constraints { + bool_or { + literals: -83 + literals: 8 + literals: 50 + } +} +constraints { + bool_or { + literals: -95 + literals: -8 + literals: -84 + } +} +constraints { + bool_or { + literals: 8 + literals: -31 + literals: 54 + } +} +constraints { + bool_or { + literals: -90 + literals: 44 + literals: 35 + } +} +constraints { + bool_or { + literals: 73 + literals: 48 + literals: -27 + } +} +constraints { + bool_or { + literals: 60 + literals: 15 + literals: -73 + } +} +constraints { + bool_or { + literals: -45 + literals: -94 + literals: -74 + } +} +constraints { + bool_or { + literals: 3 + literals: -55 + literals: -12 + } +} +constraints { + bool_or { + literals: -71 + literals: -3 + literals: -44 + } +} +constraints { + bool_or { + literals: 88 + literals: 31 + literals: 42 + } +} +constraints { + bool_or { + literals: -24 + literals: 1 + literals: -61 + } +} +constraints { + bool_or { + literals: -20 + literals: -30 + literals: -13 + } +} +constraints { + bool_or { + literals: -30 + literals: 70 + literals: 4 + } +} +constraints { + bool_or { + literals: -11 + literals: -34 + literals: -22 + } +} +constraints { + bool_or { + literals: 53 + literals: 20 + literals: 56 + } +} +constraints { + bool_or { + literals: -85 + literals: -74 + literals: 18 + } +} +constraints { + bool_or { + literals: -85 + literals: -29 + literals: 21 + } +} +constraints { + bool_or { + literals: -35 + literals: -74 + literals: -38 + } +} +constraints { + bool_or { + literals: 24 + literals: -6 + literals: 41 + } +} +constraints { + bool_or { + literals: 91 + literals: -50 + literals: -87 + } +} +constraints { + bool_or { + literals: -100 + literals: -79 + literals: -18 + } +} +constraints { + bool_or { + literals: 3 + literals: 82 + literals: -57 + } +} +constraints { + bool_or { + literals: 42 + literals: -52 + literals: 11 + } +} +constraints { + bool_or { + literals: 37 + literals: -38 + literals: 62 + } +} +constraints { + bool_or { + literals: 31 + literals: -66 + literals: -42 + } +} +constraints { + bool_or { + literals: -12 + literals: 23 + literals: -14 + } +} +constraints { + bool_or { + literals: 88 + literals: 97 + literals: 40 + } +} +constraints { + bool_or { + literals: 39 + literals: -64 + literals: 96 + } +} +constraints { + bool_or { + literals: -43 + literals: -57 + literals: 93 + } +} +constraints { + bool_or { + literals: -47 + literals: -54 + literals: 14 + } +} +constraints { + bool_or { + literals: 35 + literals: -5 + literals: 92 + } +} +constraints { + bool_or { + literals: -23 + literals: -45 + literals: -33 + } +} +constraints { + bool_or { + literals: 66 + literals: -74 + literals: -84 + } +} +constraints { + bool_or { + literals: -88 + literals: -99 + literals: 99 + } +} +constraints { + bool_or { + literals: 29 + literals: 48 + literals: -96 + } +} +constraints { + bool_or { + literals: -41 + literals: 69 + literals: 16 + } +} +constraints { + bool_or { + literals: 31 + literals: -20 + literals: 55 + } +} +constraints { + bool_or { + literals: -72 + literals: -42 + literals: -54 + } +} +constraints { + bool_or { + literals: 55 + literals: -91 + literals: -27 + } +} +constraints { + bool_or { + literals: 80 + literals: -21 + literals: -30 + } +} +constraints { + bool_or { + literals: -34 + literals: 21 + literals: -4 + } +} +constraints { + bool_or { + literals: 73 + literals: 99 + literals: -69 + } +} +constraints { + bool_or { + literals: 83 + literals: 85 + literals: -92 + } +} +constraints { + bool_or { + literals: 32 + literals: 8 + literals: 72 + } +} +constraints { + bool_or { + literals: 6 + literals: 34 + literals: 18 + } +} +constraints { + bool_or { + literals: -52 + literals: -3 + literals: -26 + } +} +constraints { + bool_or { + literals: 30 + literals: -46 + literals: 19 + } +} +constraints { + bool_or { + literals: 54 + literals: 40 + literals: 30 + } +} +constraints { + bool_or { + literals: -80 + literals: 34 + literals: 35 + } +} +constraints { + bool_or { + literals: -30 + literals: 30 + literals: -65 + } +} +constraints { + bool_or { + literals: -47 + literals: 85 + literals: -67 + } +} +constraints { + bool_or { + literals: -72 + literals: 52 + literals: -16 + } +} +constraints { + bool_or { + literals: -43 + literals: -87 + literals: -6 + } +} +constraints { + bool_or { + literals: 54 + literals: -91 + literals: -43 + } +} +constraints { + bool_or { + literals: -40 + literals: 14 + literals: -82 + } +} +constraints { + bool_or { + literals: -90 + literals: 31 + literals: 42 + } +} +constraints { + bool_or { + literals: -50 + literals: 34 + literals: -48 + } +} +constraints { + bool_or { + literals: -53 + literals: 41 + literals: 99 + } +} +constraints { + bool_or { + literals: 48 + literals: -63 + literals: 44 + } +} +constraints { + bool_or { + literals: -18 + literals: 57 + literals: -31 + } +} +constraints { + bool_or { + literals: -51 + literals: 7 + literals: 97 + } +} +constraints { + bool_or { + literals: 85 + literals: 20 + literals: -91 + } +} +constraints { + bool_or { + literals: -5 + literals: -54 + literals: -98 + } +} +constraints { + bool_or { + literals: -68 + literals: 5 + literals: 37 + } +} +constraints { + bool_or { + literals: 33 + literals: 29 + literals: -34 + } +} +constraints { + bool_or { + literals: 39 + literals: -16 + literals: 9 + } +} +constraints { + bool_or { + literals: -50 + literals: 64 + literals: 48 + } +} +constraints { + bool_or { + literals: 77 + literals: 71 + literals: -36 + } +} +constraints { + bool_or { + literals: -62 + literals: 47 + literals: -86 + } +} +constraints { + bool_or { + literals: -54 + literals: -39 + literals: 53 + } +} +constraints { + bool_or { + literals: -98 + literals: 8 + literals: -8 + } +} +constraints { + bool_or { + literals: 29 + literals: 39 + literals: 58 + } +} +constraints { + bool_or { + literals: 56 + literals: 40 + literals: -13 + } +} +constraints { + bool_or { + literals: 82 + literals: -18 + literals: -47 + } +} +constraints { + bool_or { + literals: 81 + literals: -71 + literals: -77 + } +} +constraints { + bool_or { + literals: -21 + literals: -12 + literals: 9 + } +} +constraints { + bool_or { + literals: 91 + literals: -79 + literals: -73 + } +} +constraints { + bool_or { + literals: -15 + literals: -42 + literals: 59 + } +} +constraints { + bool_or { + literals: -45 + literals: 3 + literals: 53 + } +} +constraints { + bool_or { + literals: -2 + literals: -72 + literals: 31 + } +} +constraints { + bool_or { + literals: -53 + literals: 86 + literals: 23 + } +} +constraints { + bool_or { + literals: 42 + literals: 54 + literals: 13 + } +} +constraints { + bool_or { + literals: -29 + literals: -93 + literals: 67 + } +} +constraints { + bool_or { + literals: -15 + literals: -89 + literals: -52 + } +} +constraints { + bool_or { + literals: 52 + literals: 40 + literals: -90 + } +} +constraints { + bool_or { + literals: -53 + literals: -52 + literals: 81 + } +} +constraints { + bool_or { + literals: 74 + literals: -48 + literals: 49 + } +} +constraints { + bool_or { + literals: -67 + literals: -13 + literals: -47 + } +} +constraints { + bool_or { + literals: 4 + literals: 96 + literals: 67 + } +} +constraints { + bool_or { + literals: 47 + literals: -31 + literals: -9 + } +} +constraints { + bool_or { + literals: 35 + literals: 74 + literals: 71 + } +} +constraints { + bool_or { + literals: -80 + literals: -61 + literals: -91 + } +} +constraints { + bool_or { + literals: -87 + literals: 19 + literals: -60 + } +} +constraints { + bool_or { + literals: -84 + literals: -100 + literals: 92 + } +} +constraints { + bool_or { + literals: -22 + literals: -99 + literals: -61 + } +} +constraints { + bool_or { + literals: 37 + literals: 80 + literals: 14 + } +} +constraints { + bool_or { + literals: -36 + literals: -87 + literals: 17 + } +} +constraints { + bool_or { + literals: 66 + literals: -77 + literals: -10 + } +} +constraints { + bool_or { + literals: -42 + literals: 61 + literals: 16 + } +} +constraints { + bool_or { + literals: -78 + literals: 13 + literals: 48 + } +} +constraints { + bool_or { + literals: 68 + literals: -82 + literals: -29 + } +} +constraints { + bool_or { + literals: 29 + literals: -82 + literals: -99 + } +} +constraints { + bool_or { + literals: 52 + literals: 17 + literals: 56 + } +} +constraints { + bool_or { + literals: -84 + literals: -37 + literals: 2 + } +} +constraints { + bool_or { + literals: 13 + literals: 8 + literals: 48 + } +} +constraints { + bool_or { + literals: 29 + literals: 14 + literals: -44 + } +} +constraints { + bool_or { + literals: -27 + literals: 2 + literals: -43 + } +} +constraints { + bool_or { + literals: -22 + literals: -74 + literals: -59 + } +} +constraints { + bool_or { + literals: -99 + literals: 94 + literals: 38 + } +} +constraints { + bool_or { + literals: 42 + literals: 69 + literals: 12 + } +} +constraints { + bool_or { + literals: -93 + literals: -19 + literals: -4 + } +} +constraints { + bool_or { + literals: -91 + literals: -30 + literals: 89 + } +} +constraints { + bool_or { + literals: -21 + literals: 8 + literals: -49 + } +} +constraints { + bool_or { + literals: -23 + literals: -48 + literals: 14 + } +} +constraints { + bool_or { + literals: -13 + literals: -14 + literals: -17 + } +} +constraints { + bool_or { + literals: 30 + literals: -48 + literals: -3 + } +} +constraints { + bool_or { + literals: -92 + literals: 41 + literals: 75 + } +} +constraints { + bool_or { + literals: 56 + literals: 2 + literals: 28 + } +} +constraints { + bool_or { + literals: 60 + literals: -38 + literals: -61 + } +} +constraints { + bool_or { + literals: -64 + literals: -60 + literals: 58 + } +} +constraints { + bool_or { + literals: 88 + literals: -7 + literals: -71 + } +} +constraints { + bool_or { + literals: 92 + literals: 36 + literals: 97 + } +} +constraints { + bool_or { + literals: -12 + literals: 19 + literals: -13 + } +} +constraints { + bool_or { + literals: -88 + literals: -72 + literals: 22 + } +} +constraints { + bool_or { + literals: 31 + literals: -66 + literals: -65 + } +} +constraints { + bool_or { + literals: -89 + literals: -45 + literals: 14 + } +} +constraints { + bool_or { + literals: 87 + literals: 17 + literals: -55 + } +} +constraints { + bool_or { + literals: 14 + literals: 93 + literals: -59 + } +} +constraints { + bool_or { + literals: -52 + literals: 3 + literals: -38 + } +} +constraints { + bool_or { + literals: 46 + literals: -16 + literals: 95 + } +} +constraints { + bool_or { + literals: -54 + literals: 6 + literals: 89 + } +} +constraints { + bool_or { + literals: 20 + literals: -71 + literals: 11 + } +} +constraints { + bool_or { + literals: -94 + literals: -96 + literals: -24 + } +} +constraints { + bool_or { + literals: -77 + literals: -18 + literals: -13 + } +} +constraints { + bool_or { + literals: -32 + literals: 80 + literals: -23 + } +} +constraints { + bool_or { + literals: -20 + literals: -82 + literals: -69 + } +} +constraints { + bool_or { + literals: -96 + literals: -11 + literals: -79 + } +} +constraints { + bool_or { + literals: -8 + literals: -86 + literals: -30 + } +} +constraints { + bool_or { + literals: -97 + literals: -20 + literals: 39 + } +} +constraints { + bool_or { + literals: 25 + literals: -81 + literals: 90 + } +} +constraints { + bool_or { + literals: -83 + literals: 11 + literals: -31 + } +} +constraints { + bool_or { + literals: 76 + literals: 83 + literals: -2 + } +} +constraints { + bool_or { + literals: -89 + literals: -96 + literals: -45 + } +} +constraints { + bool_or { + literals: 88 + literals: 52 + literals: 51 + } +} +constraints { + bool_or { + literals: 81 + literals: 13 + literals: -87 + } +} +constraints { + bool_or { + literals: 20 + literals: 21 + literals: -72 + } +} +constraints { + bool_or { + literals: -5 + literals: -82 + literals: -88 + } +} +constraints { + bool_or { + literals: 94 + literals: 54 + literals: 40 + } +} +constraints { + bool_or { + literals: -14 + literals: -62 + literals: 79 + } +} +constraints { + bool_or { + literals: 10 + literals: -56 + literals: -72 + } +} +constraints { + bool_or { + literals: 91 + literals: -29 + literals: -34 + } +} +constraints { + bool_or { + literals: -76 + literals: 31 + literals: -95 + } +} +constraints { + bool_or { + literals: -44 + literals: -31 + literals: -33 + } +} +constraints { + bool_or { + literals: 29 + literals: -60 + literals: 14 + } +} +constraints { + bool_or { + literals: -76 + literals: -78 + literals: 31 + } +} +constraints { + bool_or { + literals: -78 + literals: -84 + literals: 39 + } +} +constraints { + bool_or { + literals: -56 + literals: -25 + literals: -65 + } +} +constraints { + bool_or { + literals: -32 + literals: 66 + literals: 5 + } +} +constraints { + bool_or { + literals: 32 + literals: 40 + literals: -2 + } +} +constraints { + bool_or { + literals: -48 + literals: 83 + literals: -33 + } +} +constraints { + bool_or { + literals: 57 + literals: 23 + literals: 77 + } +} +constraints { + bool_or { + literals: 36 + literals: -8 + literals: 76 + } +} +constraints { + bool_or { + literals: 25 + literals: 98 + literals: -42 + } +} +constraints { + bool_or { + literals: -60 + literals: 80 + literals: 63 + } +} +constraints { + bool_or { + literals: -100 + literals: 70 + literals: 89 + } +} +constraints { + bool_or { + literals: 71 + literals: -60 + literals: -15 + } +} +constraints { + bool_or { + literals: 74 + literals: 35 + literals: 30 + } +} +constraints { + bool_or { + literals: 90 + literals: -67 + literals: 88 + } +} +constraints { + bool_or { + literals: -72 + literals: 38 + literals: -95 + } +} +constraints { + bool_or { + literals: -17 + literals: 29 + literals: 43 + } +} +constraints { + bool_or { + literals: -38 + literals: 59 + literals: -88 + } +} +constraints { + bool_or { + literals: -92 + literals: 63 + literals: 94 + } +} +constraints { + bool_or { + literals: 62 + literals: 9 + literals: 84 + } +} +constraints { + bool_or { + literals: -98 + literals: 23 + literals: 96 + } +} +constraints { + bool_or { + literals: -16 + literals: 33 + literals: -54 + } +} +constraints { + bool_or { + literals: 26 + literals: -50 + literals: -70 + } +} +constraints { + bool_or { + literals: 27 + literals: 86 + literals: -75 + } +} +constraints { + bool_or { + literals: 31 + literals: -61 + literals: 63 + } +} +constraints { + bool_or { + literals: -25 + literals: -79 + literals: -73 + } +} +constraints { + bool_or { + literals: -32 + literals: -59 + literals: 2 + } +} +constraints { + bool_or { + literals: 33 + literals: -46 + literals: 57 + } +} +constraints { + bool_or { + literals: 25 + literals: -45 + literals: -40 + } +} +constraints { + bool_or { + literals: 75 + literals: 28 + literals: 83 + } +} +constraints { + bool_or { + literals: -13 + literals: 73 + literals: -36 + } +} +constraints { + bool_or { + literals: 49 + literals: -28 + literals: 72 + } +} +constraints { + bool_or { + literals: -65 + literals: 92 + literals: 51 + } +} +constraints { + bool_or { + literals: 24 + literals: 54 + literals: -49 + } +} +constraints { + bool_or { + literals: 57 + literals: 98 + literals: -20 + } +} +constraints { + bool_or { + literals: -76 + literals: -23 + literals: -7 + } +} +constraints { + bool_or { + literals: 63 + literals: -48 + literals: -58 + } +} +constraints { + bool_or { + literals: -65 + literals: 30 + literals: -27 + } +} +constraints { + bool_or { + literals: -76 + literals: 15 + literals: -59 + } +} +constraints { + bool_or { + literals: 60 + literals: 96 + literals: 45 + } +} +constraints { + bool_or { + literals: 17 + literals: 80 + literals: 37 + } +} +constraints { + bool_or { + literals: 71 + literals: -47 + literals: 69 + } +} +constraints { + bool_or { + literals: -55 + literals: 16 + literals: -87 + } +} +constraints { + bool_or { + literals: 8 + literals: -75 + literals: 35 + } +} +constraints { + bool_or { + literals: 49 + literals: -94 + literals: 31 + } +} +constraints { + bool_or { + literals: 37 + literals: -6 + literals: -17 + } +} +constraints { + bool_or { + literals: 98 + literals: -90 + literals: -48 + } +} +constraints { + bool_or { + literals: -25 + literals: -74 + literals: 52 + } +} +constraints { + bool_or { + literals: 51 + literals: 94 + literals: -79 + } +} +constraints { + bool_or { + literals: 16 + literals: -32 + literals: -90 + } +} +constraints { + bool_or { + literals: -65 + literals: 39 + literals: 6 + } +} +constraints { + bool_or { + literals: 25 + literals: -11 + literals: 17 + } +} +constraints { + bool_or { + literals: 49 + literals: -42 + literals: -10 + } +} +constraints { + bool_or { + literals: -69 + literals: 22 + literals: -23 + } +} +constraints { + bool_or { + literals: -49 + literals: 30 + literals: 14 + } +} +constraints { + bool_or { + literals: 28 + literals: -60 + literals: -63 + } +} +constraints { + bool_or { + literals: -8 + literals: -74 + literals: 32 + } +} +constraints { + bool_or { + literals: 7 + literals: 20 + literals: -95 + } +} +constraints { + bool_or { + literals: -22 + literals: -64 + literals: 83 + } +} +constraints { + bool_or { + literals: 67 + literals: -81 + literals: 75 + } +} +constraints { + bool_or { + literals: 71 + literals: -3 + literals: -78 + } +} +constraints { + bool_or { + literals: -97 + literals: 87 + literals: -79 + } +} +constraints { + bool_or { + literals: 89 + literals: 40 + literals: 82 + } +} +constraints { + bool_or { + literals: -67 + literals: -50 + literals: 92 + } +} +constraints { + bool_or { + literals: -50 + literals: 89 + literals: 98 + } +} +constraints { + bool_or { + literals: -5 + literals: 12 + literals: 29 + } +} +constraints { + bool_or { + literals: -74 + literals: -16 + literals: 23 + } +} +constraints { + bool_or { + literals: 2 + literals: -91 + literals: -48 + } +} +constraints { + bool_or { + literals: 48 + literals: 50 + literals: 99 + } +} +constraints { + bool_or { + literals: -87 + literals: 35 + literals: -15 + } +} +constraints { + bool_or { + literals: 19 + literals: 1 + literals: 65 + } +} +constraints { + bool_or { + literals: -87 + literals: 77 + literals: -67 + } +} +constraints { + bool_or { + literals: -90 + literals: 86 + literals: -61 + } +} +constraints { + bool_or { + literals: 13 + literals: 28 + literals: 88 + } +} +constraints { + bool_or { + literals: -50 + literals: -2 + literals: -34 + } +} +constraints { + bool_or { + literals: -81 + literals: 27 + literals: 3 + } +} +constraints { + bool_or { + literals: -63 + literals: 5 + literals: 66 + } +} +constraints { + bool_or { + literals: 64 + literals: 48 + literals: -98 + } +} +constraints { + bool_or { + literals: -43 + literals: -67 + literals: -1 + } +} +constraints { + bool_or { + literals: -7 + literals: 53 + literals: -91 + } +} +constraints { + bool_or { + literals: 22 + literals: 52 + literals: 7 + } +} +constraints { + bool_or { + literals: -80 + literals: 68 + literals: 25 + } +} +constraints { + bool_or { + literals: 66 + literals: -15 + literals: 97 + } +} +constraints { + bool_or { + literals: 9 + literals: 72 + literals: -39 + } +} +constraints { + bool_or { + literals: -52 + literals: 8 + literals: -34 + } +} +constraints { + bool_or { + literals: -57 + literals: -41 + literals: -95 + } +} +constraints { + bool_or { + literals: 26 + literals: 34 + literals: 24 + } +} +constraints { + bool_or { + literals: 29 + literals: 8 + literals: 7 + } +} +constraints { + bool_or { + literals: -69 + literals: -60 + literals: -73 + } +} +constraints { + bool_or { + literals: -29 + literals: 30 + literals: -89 + } +} +constraints { + bool_or { + literals: -59 + literals: -39 + literals: -55 + } +} +constraints { + bool_or { + literals: -43 + literals: 39 + literals: 76 + } +} +constraints { + bool_or { + literals: -69 + literals: 0 + literals: 49 + } +} +constraints { + bool_or { + literals: 71 + literals: 65 + literals: 45 + } +} +constraints { + bool_or { + literals: -38 + literals: -97 + literals: 57 + } +} +constraints { + bool_or { + literals: -17 + literals: 6 + literals: -64 + } +} +constraints { + bool_or { + literals: 99 + literals: 42 + literals: 94 + } +} +constraints { + bool_or { + literals: -67 + literals: 59 + literals: 80 + } +} +constraints { + bool_or { + literals: -6 + literals: 60 + literals: -29 + } +} +constraints { + bool_or { + literals: -54 + literals: -77 + literals: -93 + } +} +constraints { + bool_or { + literals: 0 + literals: 34 + literals: -52 + } +} +constraints { + bool_or { + literals: 56 + literals: -97 + literals: -81 + } +} +constraints { + bool_or { + literals: -97 + literals: -60 + literals: -45 + } +} +constraints { + bool_or { + literals: -46 + literals: 67 + literals: -50 + } +} +constraints { + bool_or { + literals: 96 + literals: 47 + literals: -29 + } +} +constraints { + bool_or { + literals: 31 + literals: 15 + literals: 62 + } +} +constraints { + bool_or { + literals: -54 + literals: -68 + literals: 51 + } +} +constraints { + bool_or { + literals: 86 + literals: 11 + literals: -36 + } +} +constraints { + bool_or { + literals: -62 + literals: -55 + literals: -50 + } +} +constraints { + bool_or { + literals: 15 + literals: 6 + literals: -41 + } +} +constraints { + bool_or { + literals: -25 + literals: 88 + literals: 92 + } +} +constraints { + bool_or { + literals: -40 + literals: -8 + literals: -71 + } +} +constraints { + bool_or { + literals: 75 + literals: 19 + literals: -93 + } +} +constraints { + bool_or { + literals: -41 + literals: 89 + literals: -18 + } +} +constraints { + bool_or { + literals: -72 + literals: -2 + literals: -97 + } +} diff --git a/ortools/sat/fuzz_testdata/SimpleCumulative b/ortools/sat/fuzz_testdata/SimpleCumulative new file mode 100644 index 0000000000..d937e2e97a --- /dev/null +++ b/ortools/sat/fuzz_testdata/SimpleCumulative @@ -0,0 +1,61 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 4 +} +variables { + domain: 2 + domain: 2 +} +variables { + domain: 0 + domain: 4 +} +variables { + domain: 1 + domain: 4 +} +variables { + domain: 2 + domain: 2 +} +variables { + domain: 0 + domain: 4 +} +variables { + domain: 3 + domain: 3 +} +variables { + domain: 4 + domain: 4 +} +variables { + domain: 6 + domain: 6 +} +constraints { + interval { + end { vars: 2 coeffs: 1 } + size { vars: 2 coeffs: 1 } + } +} +constraints { + interval { + start { vars: 3 coeffs: 1 } + end { vars: 5 coeffs: 1 } + size { vars: 4 coeffs: 1 } + } +} +constraints { + cumulative { + capacity { vars: 8 coeffs: 1 } + intervals: 0 + intervals: 1 + demands: { vars: 6 coeffs: 1 } + demands: { vars: 7 coeffs: 1 } + } +} diff --git a/ortools/sat/fuzz_testdata/SimpleInterval b/ortools/sat/fuzz_testdata/SimpleInterval new file mode 100644 index 0000000000..b566ec24a1 --- /dev/null +++ b/ortools/sat/fuzz_testdata/SimpleInterval @@ -0,0 +1,46 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 6 +} +variables { + domain: 3 + domain: 3 +} +variables { + domain: 0 + domain: 6 +} +variables { + domain: 3 + domain: 6 +} +variables { + domain: 3 + domain: 3 +} +variables { + domain: 3 + domain: 6 +} +constraints { + interval { + end {vars: 2 coeffs: 1 } + size { vars: 1 coeffs: 1 } + } +} +constraints { + interval { + start { vars: 3 coeffs: 1 } + end {vars: 5 coeffs: 1 } + size {vars: 4 coeffs: 1 } + } +} +constraints { + no_overlap { + intervals: 0 + intervals: 1 + } +} diff --git a/ortools/sat/fuzz_testdata/SimpleLinearExampleWithMaximize b/ortools/sat/fuzz_testdata/SimpleLinearExampleWithMaximize new file mode 100644 index 0000000000..4bb5b29aba --- /dev/null +++ b/ortools/sat/fuzz_testdata/SimpleLinearExampleWithMaximize @@ -0,0 +1,28 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: -10 + domain: 10 +} +variables { + domain: -10 + domain: 10 +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 1 + coeffs: 1 + domain: -100 + domain: 100 + } +} +objective { + vars: 0 + vars: 1 + scaling_factor: -1 + coeffs: -1 + coeffs: -2 +} diff --git a/ortools/sat/fuzz_testdata/SimpleOptionalIntervalFeasible b/ortools/sat/fuzz_testdata/SimpleOptionalIntervalFeasible new file mode 100644 index 0000000000..161b4cc41c --- /dev/null +++ b/ortools/sat/fuzz_testdata/SimpleOptionalIntervalFeasible @@ -0,0 +1,83 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 6 +} +variables { + domain: 3 + domain: 3 +} +variables { + domain: 0 + domain: 6 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 2 + domain: 6 +} +variables { + domain: 2 + domain: 2 +} +variables { + domain: 2 + domain: 6 +} +variables { + domain: 3 + domain: 6 +} +variables { + domain: 3 + domain: 3 +} +variables { + domain: 3 + domain: 6 +} +constraints { + enforcement_literal: 0 + interval { + start { vars: 1 coeffs: 1 } + end { vars: 3 coeffs: 1 } + size { vars: 2 offset: 2 } + } +} +constraints { + enforcement_literal: 4 + interval { + start { vars: 5 coeffs: 1 } + end { vars: 7 coeffs: 1 } + size { vars: 6 coeffs: 1 } + } +} +constraints { + interval { + start { vars: 8 coeffs: 1 } + end { vars: 10 coeffs: 1 } + size { vars: 9 coeffs: 1 } + } +} +constraints { + no_overlap { + intervals: 0 + intervals: 1 + intervals: 2 + } +} +constraints { + bool_xor { + literals: 0 + literals: 4 + } +} diff --git a/ortools/sat/fuzz_testdata/SimpleOptionalIntervalInfeasible b/ortools/sat/fuzz_testdata/SimpleOptionalIntervalInfeasible new file mode 100644 index 0000000000..604b198097 --- /dev/null +++ b/ortools/sat/fuzz_testdata/SimpleOptionalIntervalInfeasible @@ -0,0 +1,83 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 6 +} +variables { + domain: 3 + domain: 3 +} +variables { + domain: 0 + domain: 6 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 2 + domain: 6 +} +variables { + domain: 2 + domain: 2 +} +variables { + domain: 2 + domain: 6 +} +variables { + domain: 3 + domain: 6 +} +variables { + domain: 3 + domain: 3 +} +variables { + domain: 3 + domain: 6 +} +constraints { + enforcement_literal: 0 + interval { + start { vars: 1 coeffs: 1 } + end { vars: 3 coeffs: 1 } + size { vars: 2 coeffs: 1 } + } +} +constraints { + enforcement_literal: 4 + interval { + start { vars: 5 coeffs: 1 } + end { vars: 7 coeffs: 1 } + size { vars: 6 coeffs: 1 } + } +} +constraints { + interval { + start { vars: 8 coeffs: 1 } + end { vars: 10 coeffs: 1 } + size { vars: 9 coeffs: 1 } + } +} +constraints { + no_overlap { + intervals: 0 + intervals: 1 + intervals: 2 + } +} +constraints { + bool_and { + literals: 0 + literals: 4 + } +} diff --git a/ortools/sat/fuzz_testdata/SmallDualConnectedComponentsModel b/ortools/sat/fuzz_testdata/SmallDualConnectedComponentsModel new file mode 100644 index 0000000000..d838bcfac6 --- /dev/null +++ b/ortools/sat/fuzz_testdata/SmallDualConnectedComponentsModel @@ -0,0 +1,50 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 1 + domain: 10 +} +variables { + domain: 1 + domain: 10 +} +variables { + domain: 1 + domain: 10 +} +variables { + domain: 1 + domain: 10 +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 1 + coeffs: 2 + domain: 0 + domain: 8 + } +} +constraints { + linear { + vars: 2 + vars: 3 + coeffs: 1 + coeffs: 2 + domain: 0 + domain: 6 + } +} +objective { + vars: -1 + vars: -2 + vars: -3 + vars: -4 + scaling_factor: -1 + coeffs: 1 + coeffs: 2 + coeffs: 3 + coeffs: 4 +} diff --git a/ortools/sat/fuzz_testdata/SolutionHintBasicTest b/ortools/sat/fuzz_testdata/SolutionHintBasicTest new file mode 100644 index 0000000000..159c9460a5 --- /dev/null +++ b/ortools/sat/fuzz_testdata/SolutionHintBasicTest @@ -0,0 +1,5406 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +name: "Random 3-SAT" +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +constraints { + bool_or { + literals: 34 + literals: 13 + literals: 157 + } +} +constraints { + bool_or { + literals: -103 + literals: 12 + literals: 65 + } +} +constraints { + bool_or { + literals: 107 + literals: -183 + literals: 87 + } +} +constraints { + bool_or { + literals: -57 + literals: 108 + literals: -96 + } +} +constraints { + bool_or { + literals: 174 + literals: -9 + literals: 141 + } +} +constraints { + bool_or { + literals: -113 + literals: 144 + literals: -145 + } +} +constraints { + bool_or { + literals: -56 + literals: 130 + literals: -166 + } +} +constraints { + bool_or { + literals: -73 + literals: 82 + literals: -173 + } +} +constraints { + bool_or { + literals: -46 + literals: -80 + literals: -189 + } +} +constraints { + bool_or { + literals: 108 + literals: -105 + literals: -1 + } +} +constraints { + bool_or { + literals: 154 + literals: -155 + literals: 30 + } +} +constraints { + bool_or { + literals: 94 + literals: 112 + literals: -126 + } +} +constraints { + bool_or { + literals: 93 + literals: 73 + literals: 89 + } +} +constraints { + bool_or { + literals: 197 + literals: -140 + literals: -27 + } +} +constraints { + bool_or { + literals: 96 + literals: 152 + literals: 65 + } +} +constraints { + bool_or { + literals: 136 + literals: 65 + literals: 199 + } +} +constraints { + bool_or { + literals: 1 + literals: -48 + literals: -147 + } +} +constraints { + bool_or { + literals: -61 + literals: 8 + literals: -186 + } +} +constraints { + bool_or { + literals: 158 + literals: -84 + literals: -128 + } +} +constraints { + bool_or { + literals: -60 + literals: -182 + literals: 100 + } +} +constraints { + bool_or { + literals: -94 + literals: 42 + literals: 152 + } +} +constraints { + bool_or { + literals: -116 + literals: -65 + literals: 111 + } +} +constraints { + bool_or { + literals: 126 + literals: -87 + literals: 39 + } +} +constraints { + bool_or { + literals: 106 + literals: 12 + literals: -106 + } +} +constraints { + bool_or { + literals: 40 + literals: 104 + literals: 42 + } +} +constraints { + bool_or { + literals: -185 + literals: -28 + literals: 145 + } +} +constraints { + bool_or { + literals: -163 + literals: 156 + literals: -124 + } +} +constraints { + bool_or { + literals: -171 + literals: -173 + literals: -26 + } +} +constraints { + bool_or { + literals: -51 + literals: -15 + literals: -67 + } +} +constraints { + bool_or { + literals: 66 + literals: 148 + literals: 34 + } +} +constraints { + bool_or { + literals: 37 + literals: 81 + literals: 83 + } +} +constraints { + bool_or { + literals: -189 + literals: -18 + literals: 5 + } +} +constraints { + bool_or { + literals: -74 + literals: -199 + literals: -39 + } +} +constraints { + bool_or { + literals: -60 + literals: -169 + literals: 58 + } +} +constraints { + bool_or { + literals: 114 + literals: 81 + literals: 169 + } +} +constraints { + bool_or { + literals: -157 + literals: 96 + literals: -35 + } +} +constraints { + bool_or { + literals: 167 + literals: -86 + literals: -195 + } +} +constraints { + bool_or { + literals: 151 + literals: 160 + literals: -182 + } +} +constraints { + bool_or { + literals: 76 + literals: -102 + literals: 2 + } +} +constraints { + bool_or { + literals: 134 + literals: 28 + literals: 106 + } +} +constraints { + bool_or { + literals: 182 + literals: 168 + literals: -24 + } +} +constraints { + bool_or { + literals: 9 + literals: 125 + literals: -111 + } +} +constraints { + bool_or { + literals: -102 + literals: -87 + literals: 7 + } +} +constraints { + bool_or { + literals: 73 + literals: -129 + literals: -90 + } +} +constraints { + bool_or { + literals: 5 + literals: -55 + literals: 146 + } +} +constraints { + bool_or { + literals: -100 + literals: 182 + literals: -192 + } +} +constraints { + bool_or { + literals: 78 + literals: -178 + literals: 152 + } +} +constraints { + bool_or { + literals: 106 + literals: -16 + literals: 52 + } +} +constraints { + bool_or { + literals: 66 + literals: -121 + literals: 99 + } +} +constraints { + bool_or { + literals: 167 + literals: -26 + literals: -21 + } +} +constraints { + bool_or { + literals: 42 + literals: 173 + literals: -192 + } +} +constraints { + bool_or { + literals: -80 + literals: 16 + literals: 137 + } +} +constraints { + bool_or { + literals: -61 + literals: 104 + literals: -96 + } +} +constraints { + bool_or { + literals: 3 + literals: 81 + literals: -97 + } +} +constraints { + bool_or { + literals: -163 + literals: 94 + literals: -27 + } +} +constraints { + bool_or { + literals: 11 + literals: -107 + literals: -191 + } +} +constraints { + bool_or { + literals: -5 + literals: -82 + literals: 83 + } +} +constraints { + bool_or { + literals: -96 + literals: -194 + literals: 193 + } +} +constraints { + bool_or { + literals: 129 + literals: -4 + literals: 125 + } +} +constraints { + bool_or { + literals: 196 + literals: -196 + literals: -164 + } +} +constraints { + bool_or { + literals: -195 + literals: -96 + literals: -61 + } +} +constraints { + bool_or { + literals: -28 + literals: -195 + literals: -63 + } +} +constraints { + bool_or { + literals: -21 + literals: 12 + literals: 142 + } +} +constraints { + bool_or { + literals: -152 + literals: 30 + literals: -133 + } +} +constraints { + bool_or { + literals: -42 + literals: 65 + literals: -66 + } +} +constraints { + bool_or { + literals: 181 + literals: -126 + literals: -4 + } +} +constraints { + bool_or { + literals: -99 + literals: 38 + literals: -86 + } +} +constraints { + bool_or { + literals: -55 + literals: 187 + literals: 21 + } +} +constraints { + bool_or { + literals: -113 + literals: 102 + literals: 133 + } +} +constraints { + bool_or { + literals: -172 + literals: 114 + literals: 186 + } +} +constraints { + bool_or { + literals: -174 + literals: -99 + literals: 55 + } +} +constraints { + bool_or { + literals: 184 + literals: 68 + literals: -12 + } +} +constraints { + bool_or { + literals: -44 + literals: -99 + literals: 38 + } +} +constraints { + bool_or { + literals: -116 + literals: 121 + literals: 195 + } +} +constraints { + bool_or { + literals: 167 + literals: 150 + literals: -116 + } +} +constraints { + bool_or { + literals: -159 + literals: -105 + literals: -16 + } +} +constraints { + bool_or { + literals: -13 + literals: 191 + literals: 158 + } +} +constraints { + bool_or { + literals: -73 + literals: 36 + literals: 61 + } +} +constraints { + bool_or { + literals: -110 + literals: 23 + literals: 160 + } +} +constraints { + bool_or { + literals: 7 + literals: 168 + literals: -58 + } +} +constraints { + bool_or { + literals: 181 + literals: 87 + literals: 48 + } +} +constraints { + bool_or { + literals: 25 + literals: 42 + literals: -20 + } +} +constraints { + bool_or { + literals: -128 + literals: -167 + literals: -159 + } +} +constraints { + bool_or { + literals: -4 + literals: -72 + literals: -98 + } +} +constraints { + bool_or { + literals: 163 + literals: 16 + literals: 69 + } +} +constraints { + bool_or { + literals: 98 + literals: 75 + literals: -130 + } +} +constraints { + bool_or { + literals: 31 + literals: 134 + literals: -80 + } +} +constraints { + bool_or { + literals: -121 + literals: 175 + literals: 120 + } +} +constraints { + bool_or { + literals: 137 + literals: 145 + literals: -77 + } +} +constraints { + bool_or { + literals: 176 + literals: 190 + literals: -94 + } +} +constraints { + bool_or { + literals: 77 + literals: -199 + literals: -16 + } +} +constraints { + bool_or { + literals: 42 + literals: -34 + literals: -50 + } +} +constraints { + bool_or { + literals: -44 + literals: -41 + literals: -17 + } +} +constraints { + bool_or { + literals: 64 + literals: 65 + literals: 115 + } +} +constraints { + bool_or { + literals: 105 + literals: 41 + literals: -120 + } +} +constraints { + bool_or { + literals: 125 + literals: -116 + literals: -46 + } +} +constraints { + bool_or { + literals: -122 + literals: 165 + literals: 159 + } +} +constraints { + bool_or { + literals: 30 + literals: 146 + literals: -178 + } +} +constraints { + bool_or { + literals: 175 + literals: 12 + literals: -166 + } +} +constraints { + bool_or { + literals: -182 + literals: -67 + literals: 16 + } +} +constraints { + bool_or { + literals: 158 + literals: 26 + literals: -37 + } +} +constraints { + bool_or { + literals: -176 + literals: 9 + literals: -13 + } +} +constraints { + bool_or { + literals: -115 + literals: -122 + literals: 26 + } +} +constraints { + bool_or { + literals: -28 + literals: 138 + literals: 141 + } +} +constraints { + bool_or { + literals: -131 + literals: 21 + literals: 109 + } +} +constraints { + bool_or { + literals: 45 + literals: 153 + literals: -186 + } +} +constraints { + bool_or { + literals: -43 + literals: -4 + literals: 146 + } +} +constraints { + bool_or { + literals: 183 + literals: -13 + literals: -154 + } +} +constraints { + bool_or { + literals: -36 + literals: 122 + literals: 148 + } +} +constraints { + bool_or { + literals: 18 + literals: 197 + literals: -102 + } +} +constraints { + bool_or { + literals: -145 + literals: 30 + literals: 133 + } +} +constraints { + bool_or { + literals: 70 + literals: -124 + literals: -70 + } +} +constraints { + bool_or { + literals: 88 + literals: -149 + literals: 99 + } +} +constraints { + bool_or { + literals: -44 + literals: 26 + literals: 190 + } +} +constraints { + bool_or { + literals: -30 + literals: 87 + literals: 54 + } +} +constraints { + bool_or { + literals: -49 + literals: -92 + literals: 3 + } +} +constraints { + bool_or { + literals: 99 + literals: 67 + literals: -33 + } +} +constraints { + bool_or { + literals: -52 + literals: 168 + literals: -66 + } +} +constraints { + bool_or { + literals: -155 + literals: 1 + literals: -189 + } +} +constraints { + bool_or { + literals: -58 + literals: -92 + literals: -40 + } +} +constraints { + bool_or { + literals: 69 + literals: 172 + literals: -198 + } +} +constraints { + bool_or { + literals: -178 + literals: -166 + literals: 169 + } +} +constraints { + bool_or { + literals: 12 + literals: -22 + literals: -73 + } +} +constraints { + bool_or { + literals: 46 + literals: 122 + literals: 45 + } +} +constraints { + bool_or { + literals: -78 + literals: -185 + literals: -179 + } +} +constraints { + bool_or { + literals: 108 + literals: 16 + literals: -6 + } +} +constraints { + bool_or { + literals: 132 + literals: 83 + literals: -15 + } +} +constraints { + bool_or { + literals: -57 + literals: -134 + literals: 112 + } +} +constraints { + bool_or { + literals: -134 + literals: 160 + literals: 128 + } +} +constraints { + bool_or { + literals: 6 + literals: 197 + literals: 18 + } +} +constraints { + bool_or { + literals: -122 + literals: -176 + literals: -130 + } +} +constraints { + bool_or { + literals: -118 + literals: -4 + literals: 180 + } +} +constraints { + bool_or { + literals: 138 + literals: -198 + literals: 28 + } +} +constraints { + bool_or { + literals: 3 + literals: 53 + literals: 71 + } +} +constraints { + bool_or { + literals: -67 + literals: 53 + literals: 185 + } +} +constraints { + bool_or { + literals: 183 + literals: 113 + literals: 159 + } +} +constraints { + bool_or { + literals: 55 + literals: 130 + literals: 129 + } +} +constraints { + bool_or { + literals: -2 + literals: -172 + literals: -3 + } +} +constraints { + bool_or { + literals: 57 + literals: -107 + literals: -57 + } +} +constraints { + bool_or { + literals: 31 + literals: -80 + literals: 152 + } +} +constraints { + bool_or { + literals: -64 + literals: -144 + literals: 177 + } +} +constraints { + bool_or { + literals: -94 + literals: 147 + literals: -111 + } +} +constraints { + bool_or { + literals: -101 + literals: -70 + literals: -117 + } +} +constraints { + bool_or { + literals: 189 + literals: 21 + literals: -31 + } +} +constraints { + bool_or { + literals: 136 + literals: -164 + literals: -99 + } +} +constraints { + bool_or { + literals: 135 + literals: -141 + literals: -88 + } +} +constraints { + bool_or { + literals: -74 + literals: -99 + literals: -24 + } +} +constraints { + bool_or { + literals: 181 + literals: -70 + literals: -50 + } +} +constraints { + bool_or { + literals: 182 + literals: -13 + literals: -79 + } +} +constraints { + bool_or { + literals: 155 + literals: -165 + literals: -159 + } +} +constraints { + bool_or { + literals: -6 + literals: -145 + literals: 198 + } +} +constraints { + bool_or { + literals: -8 + literals: -109 + literals: -187 + } +} +constraints { + bool_or { + literals: -109 + literals: 155 + literals: -180 + } +} +constraints { + bool_or { + literals: -128 + literals: 166 + literals: 22 + } +} +constraints { + bool_or { + literals: 60 + literals: -7 + literals: -60 + } +} +constraints { + bool_or { + literals: -2 + literals: 65 + literals: 64 + } +} +constraints { + bool_or { + literals: -193 + literals: 55 + literals: -34 + } +} +constraints { + bool_or { + literals: -41 + literals: 115 + literals: -106 + } +} +constraints { + bool_or { + literals: 47 + literals: -194 + literals: -81 + } +} +constraints { + bool_or { + literals: 90 + literals: 141 + literals: -130 + } +} +constraints { + bool_or { + literals: -161 + literals: -7 + literals: -95 + } +} +constraints { + bool_or { + literals: 84 + literals: 129 + literals: -39 + } +} +constraints { + bool_or { + literals: -72 + literals: -79 + literals: -186 + } +} +constraints { + bool_or { + literals: 10 + literals: -103 + literals: 95 + } +} +constraints { + bool_or { + literals: -127 + literals: -85 + literals: 172 + } +} +constraints { + bool_or { + literals: -65 + literals: 43 + literals: 146 + } +} +constraints { + bool_or { + literals: 125 + literals: -94 + literals: -191 + } +} +constraints { + bool_or { + literals: 0 + literals: -110 + literals: 49 + } +} +constraints { + bool_or { + literals: 9 + literals: 180 + literals: -91 + } +} +constraints { + bool_or { + literals: -54 + literals: -56 + literals: -174 + } +} +constraints { + bool_or { + literals: 99 + literals: -195 + literals: -155 + } +} +constraints { + bool_or { + literals: -85 + literals: 112 + literals: 14 + } +} +constraints { + bool_or { + literals: 43 + literals: -12 + literals: -105 + } +} +constraints { + bool_or { + literals: 104 + literals: -71 + literals: 59 + } +} +constraints { + bool_or { + literals: -12 + literals: -163 + literals: -63 + } +} +constraints { + bool_or { + literals: -90 + literals: -65 + literals: 87 + } +} +constraints { + bool_or { + literals: -86 + literals: 78 + literals: -6 + } +} +constraints { + bool_or { + literals: -17 + literals: -145 + literals: 70 + } +} +constraints { + bool_or { + literals: 96 + literals: 109 + literals: 123 + } +} +constraints { + bool_or { + literals: -68 + literals: 148 + literals: -24 + } +} +constraints { + bool_or { + literals: 198 + literals: -171 + literals: -99 + } +} +constraints { + bool_or { + literals: 181 + literals: 61 + literals: -3 + } +} +constraints { + bool_or { + literals: 161 + literals: -159 + literals: -54 + } +} +constraints { + bool_or { + literals: 37 + literals: 77 + literals: -188 + } +} +constraints { + bool_or { + literals: -46 + literals: -159 + literals: -41 + } +} +constraints { + bool_or { + literals: -99 + literals: -167 + literals: -51 + } +} +constraints { + bool_or { + literals: 149 + literals: 7 + literals: 66 + } +} +constraints { + bool_or { + literals: 88 + literals: 180 + literals: -136 + } +} +constraints { + bool_or { + literals: 159 + literals: -168 + literals: 23 + } +} +constraints { + bool_or { + literals: 116 + literals: -144 + literals: 84 + } +} +constraints { + bool_or { + literals: 30 + literals: 159 + literals: 112 + } +} +constraints { + bool_or { + literals: -160 + literals: 100 + literals: 168 + } +} +constraints { + bool_or { + literals: -105 + literals: 25 + literals: 40 + } +} +constraints { + bool_or { + literals: 198 + literals: -32 + literals: 144 + } +} +constraints { + bool_or { + literals: 38 + literals: -30 + literals: 192 + } +} +constraints { + bool_or { + literals: 128 + literals: -94 + literals: -30 + } +} +constraints { + bool_or { + literals: 156 + literals: -153 + literals: -192 + } +} +constraints { + bool_or { + literals: 6 + literals: 10 + literals: 190 + } +} +constraints { + bool_or { + literals: 157 + literals: -87 + literals: 150 + } +} +constraints { + bool_or { + literals: 163 + literals: -138 + literals: 182 + } +} +constraints { + bool_or { + literals: 139 + literals: 147 + literals: 66 + } +} +constraints { + bool_or { + literals: -7 + literals: -62 + literals: 37 + } +} +constraints { + bool_or { + literals: 80 + literals: -6 + literals: 38 + } +} +constraints { + bool_or { + literals: 141 + literals: 176 + literals: 142 + } +} +constraints { + bool_or { + literals: -44 + literals: -45 + literals: 100 + } +} +constraints { + bool_or { + literals: 148 + literals: -124 + literals: -120 + } +} +constraints { + bool_or { + literals: -25 + literals: 132 + literals: -73 + } +} +constraints { + bool_or { + literals: -151 + literals: -189 + literals: -157 + } +} +constraints { + bool_or { + literals: -199 + literals: 137 + literals: -180 + } +} +constraints { + bool_or { + literals: -37 + literals: -36 + literals: -197 + } +} +constraints { + bool_or { + literals: 177 + literals: 95 + literals: 48 + } +} +constraints { + bool_or { + literals: -182 + literals: 54 + literals: -119 + } +} +constraints { + bool_or { + literals: 35 + literals: 78 + literals: 22 + } +} +constraints { + bool_or { + literals: 93 + literals: -32 + literals: 72 + } +} +constraints { + bool_or { + literals: -10 + literals: 117 + literals: -120 + } +} +constraints { + bool_or { + literals: 77 + literals: -105 + literals: -173 + } +} +constraints { + bool_or { + literals: 58 + literals: 100 + literals: 5 + } +} +constraints { + bool_or { + literals: 29 + literals: 18 + literals: -72 + } +} +constraints { + bool_or { + literals: 17 + literals: 178 + literals: -21 + } +} +constraints { + bool_or { + literals: 135 + literals: 85 + literals: -190 + } +} +constraints { + bool_or { + literals: 92 + literals: 112 + literals: -31 + } +} +constraints { + bool_or { + literals: -32 + literals: 170 + literals: -16 + } +} +constraints { + bool_or { + literals: 12 + literals: 102 + literals: 120 + } +} +constraints { + bool_or { + literals: -142 + literals: 42 + literals: -75 + } +} +constraints { + bool_or { + literals: -34 + literals: -126 + literals: -77 + } +} +constraints { + bool_or { + literals: 185 + literals: -130 + literals: 179 + } +} +constraints { + bool_or { + literals: 60 + literals: 99 + literals: 61 + } +} +constraints { + bool_or { + literals: -126 + literals: 141 + literals: 91 + } +} +constraints { + bool_or { + literals: -25 + literals: -166 + literals: 187 + } +} +constraints { + bool_or { + literals: -88 + literals: 32 + literals: 66 + } +} +constraints { + bool_or { + literals: -76 + literals: -190 + literals: 82 + } +} +constraints { + bool_or { + literals: -122 + literals: -19 + literals: 196 + } +} +constraints { + bool_or { + literals: -175 + literals: -171 + literals: -195 + } +} +constraints { + bool_or { + literals: 92 + literals: -76 + literals: 172 + } +} +constraints { + bool_or { + literals: -126 + literals: -20 + literals: 145 + } +} +constraints { + bool_or { + literals: -168 + literals: 24 + literals: 42 + } +} +constraints { + bool_or { + literals: -97 + literals: 128 + literals: -189 + } +} +constraints { + bool_or { + literals: 88 + literals: 159 + literals: -61 + } +} +constraints { + bool_or { + literals: 183 + literals: -12 + literals: 114 + } +} +constraints { + bool_or { + literals: -192 + literals: 73 + literals: 75 + } +} +constraints { + bool_or { + literals: -152 + literals: -113 + literals: 143 + } +} +constraints { + bool_or { + literals: 28 + literals: -59 + literals: 39 + } +} +constraints { + bool_or { + literals: -113 + literals: 168 + literals: -186 + } +} +constraints { + bool_or { + literals: 134 + literals: -173 + literals: 148 + } +} +constraints { + bool_or { + literals: 79 + literals: 63 + literals: -108 + } +} +constraints { + bool_or { + literals: -63 + literals: 86 + literals: -195 + } +} +constraints { + bool_or { + literals: 99 + literals: 145 + literals: 112 + } +} +constraints { + bool_or { + literals: 86 + literals: -16 + literals: 58 + } +} +constraints { + bool_or { + literals: 150 + literals: -113 + literals: 72 + } +} +constraints { + bool_or { + literals: -77 + literals: -174 + literals: -114 + } +} +constraints { + bool_or { + literals: 175 + literals: -113 + literals: 68 + } +} +constraints { + bool_or { + literals: -116 + literals: 15 + literals: 88 + } +} +constraints { + bool_or { + literals: 188 + literals: -189 + literals: -58 + } +} +constraints { + bool_or { + literals: -146 + literals: 163 + literals: 170 + } +} +constraints { + bool_or { + literals: -35 + literals: -69 + literals: -143 + } +} +constraints { + bool_or { + literals: -81 + literals: -69 + literals: 134 + } +} +constraints { + bool_or { + literals: -73 + literals: -54 + literals: -33 + } +} +constraints { + bool_or { + literals: 16 + literals: -121 + literals: -145 + } +} +constraints { + bool_or { + literals: 16 + literals: 94 + literals: -52 + } +} +constraints { + bool_or { + literals: -186 + literals: -103 + literals: 123 + } +} +constraints { + bool_or { + literals: 99 + literals: -36 + literals: 86 + } +} +constraints { + bool_or { + literals: -25 + literals: 187 + literals: -78 + } +} +constraints { + bool_or { + literals: 171 + literals: -67 + literals: 135 + } +} +constraints { + bool_or { + literals: 163 + literals: 199 + literals: 98 + } +} +constraints { + bool_or { + literals: 158 + literals: 194 + literals: -119 + } +} +constraints { + bool_or { + literals: 137 + literals: 105 + literals: 155 + } +} +constraints { + bool_or { + literals: 91 + literals: 17 + literals: -108 + } +} +constraints { + bool_or { + literals: 40 + literals: 152 + literals: 130 + } +} +constraints { + bool_or { + literals: 142 + literals: 175 + literals: 122 + } +} +constraints { + bool_or { + literals: -20 + literals: 192 + literals: -102 + } +} +constraints { + bool_or { + literals: 29 + literals: -86 + literals: 38 + } +} +constraints { + bool_or { + literals: 161 + literals: 157 + literals: 158 + } +} +constraints { + bool_or { + literals: 27 + literals: -70 + literals: 64 + } +} +constraints { + bool_or { + literals: 178 + literals: -188 + literals: -31 + } +} +constraints { + bool_or { + literals: -109 + literals: 187 + literals: -85 + } +} +constraints { + bool_or { + literals: 187 + literals: -93 + literals: 86 + } +} +constraints { + bool_or { + literals: 134 + literals: -166 + literals: -200 + } +} +constraints { + bool_or { + literals: 52 + literals: 60 + literals: 4 + } +} +constraints { + bool_or { + literals: -176 + literals: -110 + literals: 85 + } +} +constraints { + bool_or { + literals: -159 + literals: 107 + literals: -30 + } +} +constraints { + bool_or { + literals: 14 + literals: 105 + literals: 178 + } +} +constraints { + bool_or { + literals: -43 + literals: -171 + literals: -163 + } +} +constraints { + bool_or { + literals: -41 + literals: -98 + literals: 171 + } +} +constraints { + bool_or { + literals: 24 + literals: 6 + literals: -161 + } +} +constraints { + bool_or { + literals: -29 + literals: 47 + literals: 41 + } +} +constraints { + bool_or { + literals: -11 + literals: -191 + literals: -194 + } +} +constraints { + bool_or { + literals: 146 + literals: -8 + literals: 18 + } +} +constraints { + bool_or { + literals: 110 + literals: -7 + literals: -180 + } +} +constraints { + bool_or { + literals: -167 + literals: -189 + literals: 105 + } +} +constraints { + bool_or { + literals: -125 + literals: 132 + literals: 92 + } +} +constraints { + bool_or { + literals: -15 + literals: 24 + literals: -91 + } +} +constraints { + bool_or { + literals: 65 + literals: -171 + literals: 148 + } +} +constraints { + bool_or { + literals: 92 + literals: 152 + literals: 129 + } +} +constraints { + bool_or { + literals: 129 + literals: 70 + literals: -118 + } +} +constraints { + bool_or { + literals: 94 + literals: 83 + literals: -70 + } +} +constraints { + bool_or { + literals: -83 + literals: -196 + literals: 16 + } +} +constraints { + bool_or { + literals: -165 + literals: 150 + literals: -80 + } +} +constraints { + bool_or { + literals: 71 + literals: -36 + literals: -112 + } +} +constraints { + bool_or { + literals: 134 + literals: 106 + literals: 157 + } +} +constraints { + bool_or { + literals: -145 + literals: 34 + literals: -61 + } +} +constraints { + bool_or { + literals: 155 + literals: 59 + literals: -165 + } +} +constraints { + bool_or { + literals: 89 + literals: -179 + literals: 195 + } +} +constraints { + bool_or { + literals: -152 + literals: -128 + literals: 76 + } +} +constraints { + bool_or { + literals: 97 + literals: 72 + literals: 156 + } +} +constraints { + bool_or { + literals: 16 + literals: -111 + literals: 124 + } +} +constraints { + bool_or { + literals: 55 + literals: 134 + literals: -28 + } +} +constraints { + bool_or { + literals: 115 + literals: -84 + literals: 61 + } +} +constraints { + bool_or { + literals: 70 + literals: 22 + literals: 69 + } +} +constraints { + bool_or { + literals: -24 + literals: -101 + literals: -169 + } +} +constraints { + bool_or { + literals: -109 + literals: 98 + literals: -48 + } +} +constraints { + bool_or { + literals: 80 + literals: 97 + literals: 106 + } +} +constraints { + bool_or { + literals: -83 + literals: -14 + literals: 102 + } +} +constraints { + bool_or { + literals: -128 + literals: 43 + literals: 25 + } +} +constraints { + bool_or { + literals: 101 + literals: -15 + literals: 128 + } +} +constraints { + bool_or { + literals: 159 + literals: 114 + literals: -54 + } +} +constraints { + bool_or { + literals: -113 + literals: 157 + literals: 167 + } +} +constraints { + bool_or { + literals: 48 + literals: 33 + literals: -166 + } +} +constraints { + bool_or { + literals: 107 + literals: 11 + literals: -143 + } +} +constraints { + bool_or { + literals: 152 + literals: 190 + literals: -56 + } +} +constraints { + bool_or { + literals: -99 + literals: 112 + literals: 95 + } +} +constraints { + bool_or { + literals: 11 + literals: -167 + literals: -196 + } +} +constraints { + bool_or { + literals: 53 + literals: 153 + literals: 35 + } +} +constraints { + bool_or { + literals: -120 + literals: -25 + literals: 124 + } +} +constraints { + bool_or { + literals: 52 + literals: -135 + literals: 172 + } +} +constraints { + bool_or { + literals: -34 + literals: 151 + literals: 7 + } +} +constraints { + bool_or { + literals: 173 + literals: -189 + literals: -91 + } +} +constraints { + bool_or { + literals: -141 + literals: 22 + literals: -113 + } +} +constraints { + bool_or { + literals: -54 + literals: 95 + literals: -138 + } +} +constraints { + bool_or { + literals: -37 + literals: 32 + literals: 7 + } +} +constraints { + bool_or { + literals: -62 + literals: 145 + literals: -114 + } +} +constraints { + bool_or { + literals: 101 + literals: 77 + literals: 98 + } +} +constraints { + bool_or { + literals: -200 + literals: -184 + literals: -130 + } +} +constraints { + bool_or { + literals: 36 + literals: 91 + literals: 141 + } +} +constraints { + bool_or { + literals: -156 + literals: 21 + literals: 177 + } +} +constraints { + bool_or { + literals: -33 + literals: -54 + literals: 28 + } +} +constraints { + bool_or { + literals: 41 + literals: 196 + literals: 83 + } +} +constraints { + bool_or { + literals: 68 + literals: 186 + literals: 126 + } +} +constraints { + bool_or { + literals: -182 + literals: 19 + literals: 24 + } +} +constraints { + bool_or { + literals: -13 + literals: -144 + literals: -72 + } +} +constraints { + bool_or { + literals: -168 + literals: 56 + literals: 141 + } +} +constraints { + bool_or { + literals: 16 + literals: 9 + literals: 111 + } +} +constraints { + bool_or { + literals: -140 + literals: -129 + literals: -145 + } +} +constraints { + bool_or { + literals: 64 + literals: -18 + literals: -56 + } +} +constraints { + bool_or { + literals: -114 + literals: 187 + literals: -191 + } +} +constraints { + bool_or { + literals: -117 + literals: -55 + literals: -95 + } +} +constraints { + bool_or { + literals: -44 + literals: 29 + literals: -19 + } +} +constraints { + bool_or { + literals: -140 + literals: -187 + literals: 30 + } +} +constraints { + bool_or { + literals: -180 + literals: 18 + literals: -30 + } +} +constraints { + bool_or { + literals: 10 + literals: -119 + literals: -29 + } +} +constraints { + bool_or { + literals: 146 + literals: 22 + literals: -113 + } +} +constraints { + bool_or { + literals: -166 + literals: -190 + literals: -7 + } +} +constraints { + bool_or { + literals: -132 + literals: 21 + literals: -151 + } +} +constraints { + bool_or { + literals: 187 + literals: -122 + literals: 88 + } +} +constraints { + bool_or { + literals: -93 + literals: 67 + literals: -105 + } +} +constraints { + bool_or { + literals: -164 + literals: -200 + literals: 42 + } +} +constraints { + bool_or { + literals: 177 + literals: 74 + literals: -85 + } +} +constraints { + bool_or { + literals: -13 + literals: 170 + literals: 143 + } +} +constraints { + bool_or { + literals: -5 + literals: 124 + literals: -194 + } +} +constraints { + bool_or { + literals: -43 + literals: 64 + literals: 35 + } +} +constraints { + bool_or { + literals: -35 + literals: -106 + literals: -173 + } +} +constraints { + bool_or { + literals: -57 + literals: -6 + literals: 61 + } +} +constraints { + bool_or { + literals: -170 + literals: -187 + literals: 48 + } +} +constraints { + bool_or { + literals: 85 + literals: -193 + literals: -188 + } +} +constraints { + bool_or { + literals: 144 + literals: 80 + literals: 137 + } +} +constraints { + bool_or { + literals: 133 + literals: 95 + literals: 72 + } +} +constraints { + bool_or { + literals: 112 + literals: 72 + literals: 91 + } +} +constraints { + bool_or { + literals: 22 + literals: -69 + literals: 197 + } +} +constraints { + bool_or { + literals: -96 + literals: -1 + literals: 13 + } +} +constraints { + bool_or { + literals: -178 + literals: -196 + literals: -163 + } +} +constraints { + bool_or { + literals: 145 + literals: -166 + literals: -138 + } +} +constraints { + bool_or { + literals: -69 + literals: 80 + literals: -147 + } +} +constraints { + bool_or { + literals: 98 + literals: -40 + literals: -198 + } +} +constraints { + bool_or { + literals: -157 + literals: -76 + literals: -51 + } +} +constraints { + bool_or { + literals: 89 + literals: -180 + literals: -190 + } +} +constraints { + bool_or { + literals: 16 + literals: -79 + literals: -51 + } +} +constraints { + bool_or { + literals: -154 + literals: 146 + literals: 193 + } +} +constraints { + bool_or { + literals: -18 + literals: 128 + literals: 92 + } +} +constraints { + bool_or { + literals: -52 + literals: 4 + literals: 38 + } +} +constraints { + bool_or { + literals: -194 + literals: -108 + literals: -40 + } +} +constraints { + bool_or { + literals: -53 + literals: 30 + literals: 143 + } +} +constraints { + bool_or { + literals: -8 + literals: 87 + literals: 133 + } +} +constraints { + bool_or { + literals: -176 + literals: -136 + literals: 121 + } +} +constraints { + bool_or { + literals: -81 + literals: 107 + literals: 180 + } +} +constraints { + bool_or { + literals: 66 + literals: -83 + literals: -46 + } +} +constraints { + bool_or { + literals: -187 + literals: -13 + literals: -116 + } +} +constraints { + bool_or { + literals: -75 + literals: 109 + literals: 132 + } +} +constraints { + bool_or { + literals: 179 + literals: 111 + literals: -127 + } +} +constraints { + bool_or { + literals: -28 + literals: 3 + literals: 50 + } +} +constraints { + bool_or { + literals: -132 + literals: -155 + literals: 117 + } +} +constraints { + bool_or { + literals: 138 + literals: 70 + literals: -172 + } +} +constraints { + bool_or { + literals: -120 + literals: -52 + literals: -3 + } +} +constraints { + bool_or { + literals: 144 + literals: 49 + literals: 180 + } +} +constraints { + bool_or { + literals: -80 + literals: 29 + literals: -145 + } +} +constraints { + bool_or { + literals: 195 + literals: 184 + literals: -111 + } +} +constraints { + bool_or { + literals: 73 + literals: 113 + literals: 103 + } +} +constraints { + bool_or { + literals: 35 + literals: -199 + literals: 63 + } +} +constraints { + bool_or { + literals: -122 + literals: 119 + literals: -196 + } +} +constraints { + bool_or { + literals: -102 + literals: -82 + literals: 137 + } +} +constraints { + bool_or { + literals: 84 + literals: 2 + literals: -109 + } +} +constraints { + bool_or { + literals: -168 + literals: -53 + literals: 57 + } +} +constraints { + bool_or { + literals: -97 + literals: 115 + literals: -170 + } +} +constraints { + bool_or { + literals: -56 + literals: -28 + literals: -195 + } +} +constraints { + bool_or { + literals: 48 + literals: -127 + literals: -119 + } +} +constraints { + bool_or { + literals: -159 + literals: 163 + literals: 190 + } +} +constraints { + bool_or { + literals: -104 + literals: 85 + literals: -161 + } +} +constraints { + bool_or { + literals: 128 + literals: -195 + literals: -192 + } +} +constraints { + bool_or { + literals: -153 + literals: -46 + literals: -105 + } +} +constraints { + bool_or { + literals: 93 + literals: 94 + literals: -67 + } +} +constraints { + bool_or { + literals: -47 + literals: 64 + literals: -48 + } +} +constraints { + bool_or { + literals: -86 + literals: 97 + literals: 143 + } +} +constraints { + bool_or { + literals: 57 + literals: 97 + literals: 14 + } +} +constraints { + bool_or { + literals: 38 + literals: -59 + literals: 127 + } +} +constraints { + bool_or { + literals: 44 + literals: 4 + literals: 175 + } +} +constraints { + bool_or { + literals: -129 + literals: 151 + literals: 12 + } +} +constraints { + bool_or { + literals: -190 + literals: -15 + literals: 72 + } +} +constraints { + bool_or { + literals: -55 + literals: -41 + literals: -189 + } +} +constraints { + bool_or { + literals: -54 + literals: -8 + literals: -30 + } +} +constraints { + bool_or { + literals: -17 + literals: 145 + literals: -27 + } +} +constraints { + bool_or { + literals: -79 + literals: -142 + literals: -30 + } +} +constraints { + bool_or { + literals: -198 + literals: -37 + literals: 30 + } +} +constraints { + bool_or { + literals: 134 + literals: -39 + literals: 39 + } +} +constraints { + bool_or { + literals: -31 + literals: -157 + literals: -110 + } +} +constraints { + bool_or { + literals: 109 + literals: 54 + literals: 128 + } +} +constraints { + bool_or { + literals: 181 + literals: -139 + literals: -82 + } +} +constraints { + bool_or { + literals: -74 + literals: 134 + literals: -10 + } +} +constraints { + bool_or { + literals: 166 + literals: -130 + literals: -113 + } +} +constraints { + bool_or { + literals: -107 + literals: 79 + literals: 161 + } +} +constraints { + bool_or { + literals: -48 + literals: 78 + literals: -138 + } +} +constraints { + bool_or { + literals: -54 + literals: -21 + literals: 117 + } +} +constraints { + bool_or { + literals: -199 + literals: -40 + literals: 116 + } +} +constraints { + bool_or { + literals: -157 + literals: 59 + literals: -139 + } +} +constraints { + bool_or { + literals: -43 + literals: 172 + literals: -75 + } +} +constraints { + bool_or { + literals: 58 + literals: 51 + literals: -185 + } +} +constraints { + bool_or { + literals: -84 + literals: -41 + literals: -123 + } +} +constraints { + bool_or { + literals: 8 + literals: -44 + literals: 72 + } +} +constraints { + bool_or { + literals: -90 + literals: -59 + literals: -102 + } +} +constraints { + bool_or { + literals: 23 + literals: 113 + literals: -77 + } +} +constraints { + bool_or { + literals: -20 + literals: -134 + literals: -62 + } +} +constraints { + bool_or { + literals: 184 + literals: -10 + literals: -98 + } +} +constraints { + bool_or { + literals: 26 + literals: 146 + literals: 198 + } +} +constraints { + bool_or { + literals: -153 + literals: -109 + literals: 4 + } +} +constraints { + bool_or { + literals: 19 + literals: -141 + literals: -109 + } +} +constraints { + bool_or { + literals: 20 + literals: 180 + literals: -142 + } +} +constraints { + bool_or { + literals: 117 + literals: -129 + literals: 72 + } +} +constraints { + bool_or { + literals: -20 + literals: 193 + literals: -15 + } +} +constraints { + bool_or { + literals: 153 + literals: -76 + literals: 161 + } +} +constraints { + bool_or { + literals: 170 + literals: 7 + literals: -132 + } +} +constraints { + bool_or { + literals: 67 + literals: -117 + literals: 39 + } +} +constraints { + bool_or { + literals: -37 + literals: -60 + literals: 188 + } +} +constraints { + bool_or { + literals: 151 + literals: -13 + literals: -184 + } +} +constraints { + bool_or { + literals: -106 + literals: -95 + literals: -144 + } +} +constraints { + bool_or { + literals: 7 + literals: 131 + literals: 107 + } +} +constraints { + bool_or { + literals: 53 + literals: 129 + literals: -10 + } +} +constraints { + bool_or { + literals: 79 + literals: 84 + literals: -42 + } +} +constraints { + bool_or { + literals: 14 + literals: -23 + literals: -146 + } +} +constraints { + bool_or { + literals: 129 + literals: 171 + literals: -17 + } +} +constraints { + bool_or { + literals: 184 + literals: -144 + literals: -80 + } +} +constraints { + bool_or { + literals: 115 + literals: -149 + literals: -136 + } +} +constraints { + bool_or { + literals: -99 + literals: 133 + literals: 3 + } +} +constraints { + bool_or { + literals: 156 + literals: 191 + literals: 104 + } +} +constraints { + bool_or { + literals: -84 + literals: -139 + literals: 87 + } +} +constraints { + bool_or { + literals: 89 + literals: -83 + literals: 39 + } +} +constraints { + bool_or { + literals: 114 + literals: -128 + literals: 109 + } +} +constraints { + bool_or { + literals: 121 + literals: -173 + literals: -123 + } +} +constraints { + bool_or { + literals: -136 + literals: 37 + literals: 110 + } +} +constraints { + bool_or { + literals: -78 + literals: -133 + literals: -137 + } +} +constraints { + bool_or { + literals: 170 + literals: -31 + literals: 179 + } +} +constraints { + bool_or { + literals: 60 + literals: 165 + literals: 2 + } +} +constraints { + bool_or { + literals: -53 + literals: 2 + literals: -196 + } +} +constraints { + bool_or { + literals: 131 + literals: -146 + literals: -113 + } +} +constraints { + bool_or { + literals: 27 + literals: 73 + literals: -48 + } +} +constraints { + bool_or { + literals: 131 + literals: -135 + literals: -3 + } +} +constraints { + bool_or { + literals: 147 + literals: -189 + literals: -81 + } +} +constraints { + bool_or { + literals: 30 + literals: 51 + literals: -142 + } +} +constraints { + bool_or { + literals: 115 + literals: 163 + literals: 20 + } +} +constraints { + bool_or { + literals: -50 + literals: 128 + literals: 125 + } +} +constraints { + bool_or { + literals: -30 + literals: -110 + literals: 130 + } +} +constraints { + bool_or { + literals: -177 + literals: -17 + literals: 182 + } +} +constraints { + bool_or { + literals: 46 + literals: -151 + literals: 54 + } +} +constraints { + bool_or { + literals: 143 + literals: 130 + literals: 150 + } +} +constraints { + bool_or { + literals: 125 + literals: -36 + literals: -184 + } +} +constraints { + bool_or { + literals: 21 + literals: -149 + literals: 151 + } +} +constraints { + bool_or { + literals: 67 + literals: -159 + literals: 183 + } +} +constraints { + bool_or { + literals: 27 + literals: -73 + literals: 38 + } +} +constraints { + bool_or { + literals: -39 + literals: -89 + literals: -158 + } +} +constraints { + bool_or { + literals: -145 + literals: 14 + literals: 182 + } +} +constraints { + bool_or { + literals: -95 + literals: 151 + literals: -7 + } +} +constraints { + bool_or { + literals: 173 + literals: -15 + literals: 125 + } +} +constraints { + bool_or { + literals: 134 + literals: 94 + literals: -58 + } +} +constraints { + bool_or { + literals: -154 + literals: 159 + literals: 180 + } +} +constraints { + bool_or { + literals: -87 + literals: -136 + literals: 54 + } +} +constraints { + bool_or { + literals: 116 + literals: -170 + literals: 122 + } +} +constraints { + bool_or { + literals: 84 + literals: 78 + literals: 160 + } +} +constraints { + bool_or { + literals: 138 + literals: -107 + literals: -81 + } +} +constraints { + bool_or { + literals: 107 + literals: 181 + literals: -168 + } +} +constraints { + bool_or { + literals: -85 + literals: -29 + literals: 192 + } +} +constraints { + bool_or { + literals: 13 + literals: 174 + literals: -132 + } +} +constraints { + bool_or { + literals: 56 + literals: -40 + literals: -166 + } +} +constraints { + bool_or { + literals: -54 + literals: -117 + literals: -190 + } +} +constraints { + bool_or { + literals: -87 + literals: 148 + literals: 128 + } +} +constraints { + bool_or { + literals: -41 + literals: 1 + literals: -39 + } +} +constraints { + bool_or { + literals: -84 + literals: -148 + literals: -11 + } +} +constraints { + bool_or { + literals: -85 + literals: -150 + literals: 123 + } +} +constraints { + bool_or { + literals: -130 + literals: -118 + literals: 66 + } +} +constraints { + bool_or { + literals: -167 + literals: -127 + literals: -25 + } +} +constraints { + bool_or { + literals: -77 + literals: -12 + literals: 164 + } +} +constraints { + bool_or { + literals: -59 + literals: -27 + literals: -174 + } +} +constraints { + bool_or { + literals: -168 + literals: 194 + literals: 183 + } +} +constraints { + bool_or { + literals: -1 + literals: 126 + literals: -14 + } +} +constraints { + bool_or { + literals: 105 + literals: -184 + literals: 47 + } +} +constraints { + bool_or { + literals: 179 + literals: -67 + literals: -169 + } +} +constraints { + bool_or { + literals: 130 + literals: 196 + literals: 36 + } +} +constraints { + bool_or { + literals: -156 + literals: -94 + literals: 66 + } +} +constraints { + bool_or { + literals: 49 + literals: 111 + literals: 80 + } +} +constraints { + bool_or { + literals: 37 + literals: 47 + literals: 11 + } +} +constraints { + bool_or { + literals: -11 + literals: -80 + literals: -3 + } +} +constraints { + bool_or { + literals: -73 + literals: -38 + literals: -132 + } +} +constraints { + bool_or { + literals: -115 + literals: -196 + literals: -186 + } +} +constraints { + bool_or { + literals: -169 + literals: -56 + literals: -147 + } +} +constraints { + bool_or { + literals: -76 + literals: 82 + literals: -56 + } +} +constraints { + bool_or { + literals: 68 + literals: 176 + literals: -148 + } +} +constraints { + bool_or { + literals: 16 + literals: -68 + literals: -76 + } +} +constraints { + bool_or { + literals: 106 + literals: 148 + literals: 193 + } +} +constraints { + bool_or { + literals: 75 + literals: -63 + literals: -152 + } +} +constraints { + bool_or { + literals: 16 + literals: 144 + literals: -20 + } +} +constraints { + bool_or { + literals: -24 + literals: 152 + literals: 161 + } +} +constraints { + bool_or { + literals: -175 + literals: 193 + literals: -117 + } +} +constraints { + bool_or { + literals: -198 + literals: 15 + literals: -84 + } +} +constraints { + bool_or { + literals: -61 + literals: 176 + literals: 196 + } +} +constraints { + bool_or { + literals: 131 + literals: 113 + literals: -123 + } +} +constraints { + bool_or { + literals: -173 + literals: -141 + literals: 157 + } +} +constraints { + bool_or { + literals: -153 + literals: 37 + literals: -65 + } +} +constraints { + bool_or { + literals: -6 + literals: -137 + literals: 193 + } +} +constraints { + bool_or { + literals: 44 + literals: -25 + literals: -161 + } +} +constraints { + bool_or { + literals: -141 + literals: 120 + literals: 61 + } +} +constraints { + bool_or { + literals: -113 + literals: -178 + literals: 45 + } +} +constraints { + bool_or { + literals: -45 + literals: 68 + literals: -166 + } +} +constraints { + bool_or { + literals: 64 + literals: 134 + literals: -117 + } +} +constraints { + bool_or { + literals: 107 + literals: 30 + literals: 174 + } +} +constraints { + bool_or { + literals: 163 + literals: -135 + literals: -84 + } +} +constraints { + bool_or { + literals: -96 + literals: -39 + literals: 139 + } +} +constraints { + bool_or { + literals: -106 + literals: -135 + literals: 108 + } +} +constraints { + bool_or { + literals: 83 + literals: -144 + literals: 128 + } +} +constraints { + bool_or { + literals: 10 + literals: 121 + literals: -112 + } +} +constraints { + bool_or { + literals: -66 + literals: -153 + literals: -105 + } +} +constraints { + bool_or { + literals: -176 + literals: -188 + literals: 168 + } +} +constraints { + bool_or { + literals: -103 + literals: 182 + literals: -111 + } +} +constraints { + bool_or { + literals: 44 + literals: -130 + literals: 154 + } +} +constraints { + bool_or { + literals: 151 + literals: 23 + literals: 34 + } +} +constraints { + bool_or { + literals: 116 + literals: -7 + literals: -87 + } +} +constraints { + bool_or { + literals: -130 + literals: 113 + literals: -41 + } +} +constraints { + bool_or { + literals: -162 + literals: -63 + literals: 146 + } +} +constraints { + bool_or { + literals: 168 + literals: -106 + literals: -130 + } +} +constraints { + bool_or { + literals: -184 + literals: -148 + literals: -22 + } +} +constraints { + bool_or { + literals: -32 + literals: 166 + literals: 150 + } +} +constraints { + bool_or { + literals: -128 + literals: -11 + literals: -50 + } +} +constraints { + bool_or { + literals: 15 + literals: 173 + literals: 186 + } +} +constraints { + bool_or { + literals: 30 + literals: 131 + literals: -136 + } +} +constraints { + bool_or { + literals: 26 + literals: 164 + literals: -31 + } +} +constraints { + bool_or { + literals: -162 + literals: -178 + literals: 120 + } +} +constraints { + bool_or { + literals: -119 + literals: -151 + literals: -107 + } +} +constraints { + bool_or { + literals: 40 + literals: -67 + literals: 38 + } +} +constraints { + bool_or { + literals: -166 + literals: 122 + literals: 157 + } +} +constraints { + bool_or { + literals: 147 + literals: -160 + literals: -117 + } +} +constraints { + bool_or { + literals: 199 + literals: 50 + literals: 178 + } +} +constraints { + bool_or { + literals: 95 + literals: -65 + literals: 89 + } +} +constraints { + bool_or { + literals: 73 + literals: -33 + literals: -126 + } +} +constraints { + bool_or { + literals: -162 + literals: -179 + literals: 68 + } +} +constraints { + bool_or { + literals: -19 + literals: -160 + literals: 64 + } +} +constraints { + bool_or { + literals: 111 + literals: 122 + literals: -44 + } +} +constraints { + bool_or { + literals: 29 + literals: 47 + literals: 153 + } +} +constraints { + bool_or { + literals: 36 + literals: -170 + literals: -91 + } +} +constraints { + bool_or { + literals: -172 + literals: -128 + literals: 106 + } +} +constraints { + bool_or { + literals: -71 + literals: 78 + literals: -123 + } +} +constraints { + bool_or { + literals: -138 + literals: -103 + literals: 18 + } +} +constraints { + bool_or { + literals: -9 + literals: 89 + literals: 166 + } +} +constraints { + bool_or { + literals: -62 + literals: -119 + literals: 158 + } +} +constraints { + bool_or { + literals: 42 + literals: -133 + literals: 139 + } +} +constraints { + bool_or { + literals: -119 + literals: -130 + literals: 189 + } +} +constraints { + bool_or { + literals: 130 + literals: 75 + literals: -24 + } +} +constraints { + bool_or { + literals: -77 + literals: -87 + literals: 183 + } +} +constraints { + bool_or { + literals: -106 + literals: -161 + literals: -68 + } +} +constraints { + bool_or { + literals: 180 + literals: 148 + literals: 142 + } +} +constraints { + bool_or { + literals: -8 + literals: 178 + literals: 124 + } +} +constraints { + bool_or { + literals: -39 + literals: 163 + literals: -139 + } +} +constraints { + bool_or { + literals: 96 + literals: -158 + literals: -68 + } +} +constraints { + bool_or { + literals: 143 + literals: 152 + literals: 180 + } +} +constraints { + bool_or { + literals: 65 + literals: 91 + literals: -35 + } +} +constraints { + bool_or { + literals: -118 + literals: -55 + literals: 14 + } +} +constraints { + bool_or { + literals: -144 + literals: 59 + literals: 73 + } +} +constraints { + bool_or { + literals: -46 + literals: 105 + literals: -86 + } +} +constraints { + bool_or { + literals: 56 + literals: -20 + literals: 45 + } +} +constraints { + bool_or { + literals: 63 + literals: -69 + literals: -110 + } +} +constraints { + bool_or { + literals: 114 + literals: -179 + literals: 168 + } +} +constraints { + bool_or { + literals: -94 + literals: -197 + literals: -20 + } +} +constraints { + bool_or { + literals: -105 + literals: 51 + literals: -110 + } +} +constraints { + bool_or { + literals: 147 + literals: -191 + literals: 113 + } +} +constraints { + bool_or { + literals: 40 + literals: 110 + literals: -54 + } +} +constraints { + bool_or { + literals: 105 + literals: 71 + literals: 185 + } +} +constraints { + bool_or { + literals: 140 + literals: 144 + literals: -127 + } +} +solution_hint { + vars: 0 + vars: 1 + vars: 2 + vars: 3 + vars: 4 + vars: 5 + vars: 6 + vars: 7 + vars: 8 + vars: 9 + vars: 10 + vars: 11 + vars: 12 + vars: 13 + vars: 14 + vars: 15 + vars: 16 + vars: 17 + vars: 18 + vars: 19 + vars: 20 + vars: 21 + vars: 22 + vars: 23 + vars: 24 + vars: 25 + vars: 26 + vars: 27 + vars: 28 + vars: 29 + vars: 30 + vars: 31 + vars: 32 + vars: 33 + vars: 34 + vars: 35 + vars: 36 + vars: 37 + vars: 38 + vars: 39 + vars: 40 + vars: 41 + vars: 42 + vars: 43 + vars: 44 + vars: 45 + vars: 46 + vars: 47 + vars: 48 + vars: 49 + vars: 50 + vars: 51 + vars: 52 + vars: 53 + vars: 54 + vars: 55 + vars: 56 + vars: 57 + vars: 58 + vars: 59 + vars: 60 + vars: 61 + vars: 62 + vars: 63 + vars: 64 + vars: 65 + vars: 66 + vars: 67 + vars: 68 + vars: 69 + vars: 70 + vars: 71 + vars: 72 + vars: 73 + vars: 74 + vars: 75 + vars: 76 + vars: 77 + vars: 78 + vars: 79 + vars: 80 + vars: 81 + vars: 82 + vars: 83 + vars: 84 + vars: 85 + vars: 86 + vars: 87 + vars: 88 + vars: 89 + vars: 90 + vars: 91 + vars: 92 + vars: 93 + vars: 94 + vars: 95 + vars: 96 + vars: 97 + vars: 98 + vars: 99 + vars: 100 + vars: 101 + vars: 102 + vars: 103 + vars: 104 + vars: 105 + vars: 106 + vars: 107 + vars: 108 + vars: 109 + vars: 110 + vars: 111 + vars: 112 + vars: 113 + vars: 114 + vars: 115 + vars: 116 + vars: 117 + vars: 118 + vars: 119 + vars: 120 + vars: 121 + vars: 122 + vars: 123 + vars: 124 + vars: 125 + vars: 126 + vars: 127 + vars: 128 + vars: 129 + vars: 130 + vars: 131 + vars: 132 + vars: 133 + vars: 134 + vars: 135 + vars: 136 + vars: 137 + vars: 138 + vars: 139 + vars: 140 + vars: 141 + vars: 142 + vars: 143 + vars: 144 + vars: 145 + vars: 146 + vars: 147 + vars: 148 + vars: 149 + vars: 150 + vars: 151 + vars: 152 + vars: 153 + vars: 154 + vars: 155 + vars: 156 + vars: 157 + vars: 158 + vars: 159 + vars: 160 + vars: 161 + vars: 162 + vars: 163 + vars: 164 + vars: 165 + vars: 166 + vars: 167 + vars: 168 + vars: 169 + vars: 170 + vars: 171 + vars: 172 + vars: 173 + vars: 174 + vars: 175 + vars: 176 + vars: 177 + vars: 178 + vars: 179 + vars: 180 + vars: 181 + vars: 182 + vars: 183 + vars: 184 + vars: 185 + vars: 186 + vars: 187 + vars: 188 + vars: 189 + vars: 190 + vars: 191 + vars: 192 + vars: 193 + vars: 194 + vars: 195 + vars: 196 + vars: 197 + vars: 198 + vars: 199 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 1 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 1 + values: 1 + values: 0 + values: 0 + values: 1 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 1 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 1 + values: 0 + values: 1 + values: 1 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 0 + values: 0 + values: 1 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 1 + values: 0 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 1 + values: 1 + values: 0 + values: 0 + values: 1 + values: 1 + values: 1 + values: 0 + values: 1 + values: 1 + values: 1 + values: 0 + values: 0 + values: 0 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 1 + values: 1 + values: 0 + values: 1 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 1 + values: 1 + values: 1 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 1 + values: 0 + values: 1 + values: 1 + values: 1 + values: 0 + values: 1 + values: 1 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 1 + values: 1 + values: 0 + values: 0 + values: 0 + values: 1 + values: 0 + values: 1 + values: 0 + values: 0 + values: 0 + values: 1 + values: 0 + values: 0 + values: 0 +} diff --git a/ortools/sat/fuzz_testdata/SolutionHintEnumerateTest b/ortools/sat/fuzz_testdata/SolutionHintEnumerateTest new file mode 100644 index 0000000000..3cf22243ff --- /dev/null +++ b/ortools/sat/fuzz_testdata/SolutionHintEnumerateTest @@ -0,0 +1,27 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + name: "x" + domain: 0 + domain: 10 +} +variables { + name: "y" + domain: 0 + domain: 10 +} +constraints { + linear { + vars: 1 + vars: 0 + coeffs: 1 + coeffs: 1 + domain: 10 + domain: 10 + } +} +solution_hint { + vars: 0 + values: -1 +} diff --git a/ortools/sat/fuzz_testdata/SolutionHintObjectiveTest b/ortools/sat/fuzz_testdata/SolutionHintObjectiveTest new file mode 100644 index 0000000000..555d4451bf --- /dev/null +++ b/ortools/sat/fuzz_testdata/SolutionHintObjectiveTest @@ -0,0 +1,39 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +objective { + vars: 0 + vars: 1 + vars: 2 + vars: 3 + coeffs: 1 + coeffs: 2 + coeffs: 3 + coeffs: 4 +} +solution_hint { + vars: 0 + vars: 1 + vars: 2 + vars: 3 + values: 1 + values: 0 + values: 0 + values: 1 +} diff --git a/ortools/sat/fuzz_testdata/SolutionHintOptimalObjectiveTest b/ortools/sat/fuzz_testdata/SolutionHintOptimalObjectiveTest new file mode 100644 index 0000000000..4e2dc62424 --- /dev/null +++ b/ortools/sat/fuzz_testdata/SolutionHintOptimalObjectiveTest @@ -0,0 +1,39 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +variables { + domain: 0 + domain: 1 +} +objective { + vars: 0 + vars: 1 + vars: 2 + vars: 3 + coeffs: -1 + coeffs: 2 + coeffs: 3 + coeffs: -4 +} +solution_hint { + vars: 0 + vars: 1 + vars: 2 + vars: 3 + values: 1 + values: 0 + values: 0 + values: 1 +} diff --git a/ortools/sat/fuzz_testdata/SolutionsAreCorrectlyPostsolvedInTheObserver b/ortools/sat/fuzz_testdata/SolutionsAreCorrectlyPostsolvedInTheObserver new file mode 100644 index 0000000000..e1d3ba8908 --- /dev/null +++ b/ortools/sat/fuzz_testdata/SolutionsAreCorrectlyPostsolvedInTheObserver @@ -0,0 +1,19 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 1 + domain: 4 +} +variables { + domain: 1 + domain: 1 +} +variables { + domain: 3 + domain: 3 +} +variables { + domain: 1 + domain: 4 +} diff --git a/ortools/sat/fuzz_testdata/TightenedDomains b/ortools/sat/fuzz_testdata/TightenedDomains new file mode 100644 index 0000000000..3df0ce979e --- /dev/null +++ b/ortools/sat/fuzz_testdata/TightenedDomains @@ -0,0 +1,27 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 10 +} +variables { + domain: 1 + domain: 10 +} +variables { + domain: 0 + domain: 10 +} +constraints { + linear { + vars: 0 + vars: 1 + vars: 2 + coeffs: 1 + coeffs: 2 + coeffs: 3 + domain: 0 + domain: 7 + } +} diff --git a/ortools/sat/fuzz_testdata/TightenedDomainsIfInfeasible b/ortools/sat/fuzz_testdata/TightenedDomainsIfInfeasible new file mode 100644 index 0000000000..8ad9704688 --- /dev/null +++ b/ortools/sat/fuzz_testdata/TightenedDomainsIfInfeasible @@ -0,0 +1,27 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 10 +} +variables { + domain: 1 + domain: 10 +} +variables { + domain: 0 + domain: 10 +} +constraints { + linear { + vars: 0 + vars: 1 + vars: 2 + coeffs: 1 + coeffs: 2 + coeffs: 3 + domain: 80 + domain: 87 + } +} diff --git a/ortools/sat/fuzz_testdata/TrivialLinearTranslatedModel b/ortools/sat/fuzz_testdata/TrivialLinearTranslatedModel new file mode 100644 index 0000000000..683c7e6072 --- /dev/null +++ b/ortools/sat/fuzz_testdata/TrivialLinearTranslatedModel @@ -0,0 +1,42 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: -10 + domain: 10 +} +variables { + domain: -10 + domain: 10 +} +variables { + domain: -4611686018427387903 + domain: 4611686018427387903 +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 1 + coeffs: 1 + domain: -4611686018427387903 + domain: 4611686018427387903 + } +} +constraints { + linear { + vars: 0 + vars: 1 + vars: 2 + coeffs: 1 + coeffs: 2 + coeffs: -1 + domain: 0 + domain: 0 + } +} +objective { + vars: -3 + scaling_factor: -1 + coeffs: 1 +} diff --git a/ortools/sat/fuzz_testdata/TrivialModelWithCore b/ortools/sat/fuzz_testdata/TrivialModelWithCore new file mode 100644 index 0000000000..d18325dc55 --- /dev/null +++ b/ortools/sat/fuzz_testdata/TrivialModelWithCore @@ -0,0 +1,11 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 1 + domain: 1 +} +objective { + vars: 0 + coeffs: 1 +} diff --git a/ortools/sat/fuzz_testdata/UnsatProblem b/ortools/sat/fuzz_testdata/UnsatProblem new file mode 100644 index 0000000000..9390f9a6de --- /dev/null +++ b/ortools/sat/fuzz_testdata/UnsatProblem @@ -0,0 +1,21 @@ +# proto-file: ortools/sat/cp_model.proto +# proto-message: operations_research.sat.CpModelProto + +variables { + domain: 0 + domain: 0 +} +variables { + domain: 1 + domain: 1 +} +constraints { + linear { + vars: 0 + vars: 1 + coeffs: 1 + coeffs: 1 + domain: 0 + domain: 0 + } +}