1// Copyright 2010-2021 Google LLC
2// Licensed under the Apache License, Version 2.0 (the "License");
3// you may not use this file except in compliance with the License.
4// You may obtain a copy of the License at
5//
6//     http://www.apache.org/licenses/LICENSE-2.0
7//
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
14// Protocol buffer to encode a Boolean satisfiability/optimization problem.
15
16syntax = "proto2";
17
18package operations_research.sat;
19
20option csharp_namespace = "Google.OrTools.Sat";
21option java_package = "com.google.ortools.sat";
22option java_multiple_files = true;
23
24// A linear Boolean constraint which is a bounded sum of linear terms. Each term
25// beeing a literal times an integer coefficient. If we assume that a literal
26// takes the value 1 if it is true and 0 otherwise, the constraint is:
27//   lower_bound <= ... + coefficients[i] * literals[i] + ... <= upper_bound
28message LinearBooleanConstraint {
29  // Linear terms involved in this constraint.
30  //
31  // literals[i] is the signed representation of the i-th literal of the
32  // constraint and coefficients[i] its coefficients. The signed representation
33  // is as follow: for a 0-based variable index x, (x + 1) represents the
34  // variable x and -(x + 1) represents its negation.
35  //
36  // Note that the same variable shouldn't appear twice and that zero
37  // coefficients are not allowed.
38  repeated int32 literals = 1;
39  repeated int64 coefficients = 2;
40
41  // Optional lower (resp. upper) bound of the constraint. If not present, it
42  // means that the constraint is not bounded in this direction. The bounds
43  // are INCLUSIVE.
44  optional int64 lower_bound = 3;
45  optional int64 upper_bound = 4;
46
47  // The name of this constraint.
48  optional string name = 5 [default = ""];
49}
50
51// The objective of an optimization problem.
52message LinearObjective {
53  // The goal is always to minimize the linear Boolean formula defined by these
54  // two fields: sum_i literal_i * coefficient_i where literal_i is 1 iff
55  // literal_i is true in a given assignment.
56  //
57  // Note that the same variable shouldn't appear twice and that zero
58  // coefficients are not allowed.
59  repeated int32 literals = 1;
60  repeated int64 coefficients = 2;
61
62  // For a given variable assignment, the "real" problem objective value is
63  // 'scaling_factor * (minimization_objective + offset)' where
64  // 'minimization_objective is the one defined just above.
65  //
66  // Note that this is not what we minimize, but it is what we display.
67  // In particular if scaling_factor is negative, then the "real" problem is
68  // a maximization problem, even if the "internal" objective is minimized.
69  optional double offset = 3 [default = 0.0];
70  optional double scaling_factor = 4 [default = 1.0];
71}
72
73// Stores an assignment of variables as a list of true literals using their
74// signed representation. There will be at most one literal per variable. The
75// literals will be sorted by increasing variable index. The assignment may be
76// partial in the sense that some variables may not appear and thus not be
77// assigned.
78message BooleanAssignment {
79  repeated int32 literals = 1;
80}
81
82// A linear Boolean problem.
83message LinearBooleanProblem {
84  // The name of the problem.
85  optional string name = 1 [default = ""];
86
87  // The number of variables in the problem.
88  // All the signed representation of the problem literals must be in
89  // [-num_variables, num_variables], excluding 0.
90  optional int32 num_variables = 3;
91
92  // The constraints of the problem.
93  repeated LinearBooleanConstraint constraints = 4;
94
95  // The objective of the problem.
96  // If left empty, we just have a satisfiability problem.
97  optional LinearObjective objective = 5;
98
99  // The names of the problem variables. The variables index are 0-based and
100  // var_names[i] will be the name of the i-th variable which correspond to
101  // literals +(i + 1) or -(i + 1). This is optional and can be left empty.
102  repeated string var_names = 6;
103
104  // Stores an assignement of the problem variables. That may be an initial
105  // feasible solution, just a partial assignement or the optimal solution.
106  optional BooleanAssignment assignment = 7;
107
108  // Hack: When converting a wcnf formulat to a LinearBooleanProblem, extra
109  // variables need to be created. This stores the number of variables in the
110  // original problem (which are in one to one correspondence with the first
111  // variables of this problem).
112  optional int32 original_num_variables = 8;
113}
114