// Copyright 2010-2025 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.

// Protocol buffer to encode a Boolean satisfiability/optimization problem.

syntax = "proto2";

package operations_research.sat;

option csharp_namespace = "Google.OrTools.Sat";
option java_package = "com.google.ortools.sat";
option java_multiple_files = true;

// A linear Boolean constraint which is a bounded sum of linear terms. Each term
// beeing a literal times an integer coefficient. If we assume that a literal
// takes the value 1 if it is true and 0 otherwise, the constraint is:
//   lower_bound <= ... + coefficients[i] * literals[i] + ... <= upper_bound
message LinearBooleanConstraint {
  // Linear terms involved in this constraint.
  //
  // literals[i] is the signed representation of the i-th literal of the
  // constraint and coefficients[i] its coefficients. The signed representation
  // is as follow: for a 0-based variable index x, (x + 1) represents the
  // variable x and -(x + 1) represents its negation.
  //
  // Note that the same variable shouldn't appear twice and that zero
  // coefficients are not allowed.
  repeated int32 literals = 1;
  repeated int64 coefficients = 2;

  // Optional lower (resp. upper) bound of the constraint. If not present, it
  // means that the constraint is not bounded in this direction. The bounds
  // are INCLUSIVE.
  optional int64 lower_bound = 3;
  optional int64 upper_bound = 4;

  // The name of this constraint.
  optional string name = 5 [default = ""];
}

// The objective of an optimization problem.
message LinearObjective {
  // The goal is always to minimize the linear Boolean formula defined by these
  // two fields: sum_i literal_i * coefficient_i where literal_i is 1 iff
  // literal_i is true in a given assignment.
  //
  // Note that the same variable shouldn't appear twice and that zero
  // coefficients are not allowed.
  repeated int32 literals = 1;
  repeated int64 coefficients = 2;

  // For a given variable assignment, the "real" problem objective value is
  // 'scaling_factor * (minimization_objective + offset)' where
  // 'minimization_objective is the one defined just above.
  //
  // Note that this is not what we minimize, but it is what we display.
  // In particular if scaling_factor is negative, then the "real" problem is
  // a maximization problem, even if the "internal" objective is minimized.
  optional double offset = 3 [default = 0.0];
  optional double scaling_factor = 4 [default = 1.0];
}

// Stores an assignment of variables as a list of true literals using their
// signed representation. There will be at most one literal per variable. The
// literals will be sorted by increasing variable index. The assignment may be
// partial in the sense that some variables may not appear and thus not be
// assigned.
message BooleanAssignment {
  repeated int32 literals = 1;
}

// A linear Boolean problem.
message LinearBooleanProblem {
  // The name of the problem.
  optional string name = 1 [default = ""];

  // The number of variables in the problem.
  // All the signed representation of the problem literals must be in
  // [-num_variables, num_variables], excluding 0.
  optional int32 num_variables = 3;

  // The constraints of the problem.
  repeated LinearBooleanConstraint constraints = 4;

  // The objective of the problem.
  // If left empty, we just have a satisfiability problem.
  optional LinearObjective objective = 5;

  // The names of the problem variables. The variables index are 0-based and
  // var_names[i] will be the name of the i-th variable which correspond to
  // literals +(i + 1) or -(i + 1). This is optional and can be left empty.
  repeated string var_names = 6;

  // Stores an assignment of the problem variables. That may be an initial
  // feasible solution, just a partial assignment or the optimal solution.
  optional BooleanAssignment assignment = 7;

  // Hack: When converting a wcnf formulat to a LinearBooleanProblem, extra
  // variables need to be created. This stores the number of variables in the
  // original problem (which are in one to one correspondence with the first
  // variables of this problem).
  optional int32 original_num_variables = 8;
}