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