home	boolean logic	integer arithmetic	channeling constraints	scheduling	Using the CP-SAT solver	Model manipulation	Troubleshooting	Python API

Boolean logic recipes for the CP-SAT solver.

https://developers.google.com/optimization/

Introduction

The CP-SAT solver can express Boolean variables and constraints. A Boolean variable is an integer variable constrained to be either 0 or 1. A literal is either a Boolean variable or its negation: 0 negated is 1, and vice versa. See https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Basic_definitions_and_terminology.

Boolean variables and literals

We can create a Boolean variable x and a literal not_x equal to the logical negation of x.

Python code

#!/usr/bin/env python3
"""Code sample to demonstrate Boolean variable and literals."""


from ortools.sat.python import cp_model


def literal_sample_sat():
    model = cp_model.CpModel()
    x = model.new_bool_var("x")
    not_x = ~x
    print(x)
    print(not_x)


literal_sample_sat()

C++ code

#include <stdlib.h>

#include "ortools/base/logging.h"
#include "ortools/sat/cp_model.h"

namespace operations_research {
namespace sat {

void LiteralSampleSat() {
  CpModelBuilder cp_model;

  const BoolVar x = cp_model.NewBoolVar().WithName("x");
  const BoolVar not_x = ~x;
  LOG(INFO) << "x = " << x << ", not(x) = " << not_x;
}

}  // namespace sat
}  // namespace operations_research

int main() {
  operations_research::sat::LiteralSampleSat();

  return EXIT_SUCCESS;
}

Java code

package com.google.ortools.sat.samples;

import com.google.ortools.Loader;
import com.google.ortools.sat.BoolVar;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.Literal;

/** Code sample to demonstrate Boolean variable and literals. */
public class LiteralSampleSat {
  public static void main(String[] args) throws Exception {
    Loader.loadNativeLibraries();
    CpModel model = new CpModel();
    BoolVar x = model.newBoolVar("x");
    Literal notX = x.not();
    System.out.println(notX);
  }
}

C# code

using System;
using Google.OrTools.Sat;

public class LiteralSampleSat
{
    static void Main()
    {
        CpModel model = new CpModel();
        BoolVar x = model.NewBoolVar("x");
        ILiteral not_x = x.Not();
    }
}

Go code

// The literal_sample_sat command is a simple example of literals.
package main

import (
	log "github.com/golang/glog"
	"github.com/google/or-tools/ortools/sat/go/cpmodel"
)

func literalSampleSat() {
	model := cpmodel.NewCpModelBuilder()

	x := model.NewBoolVar().WithName("x")
	notX := x.Not()

	log.Infof("x = %d, x.Not() = %d", x.Index(), notX.Index())
}

func main() {
	literalSampleSat()
}

Boolean constraints

For Boolean variables x and y, the following are elementary Boolean constraints:

or(x_1, .., x_n)
and(x_1, .., x_n)
xor(x_1, .., x_n)
not(x)

More complicated constraints can be built up by combining these elementary constraints. For instance, we can add a constraint Or(x, not(y)).

Python code

#!/usr/bin/env python3
"""Code sample to demonstrates a simple Boolean constraint."""


from ortools.sat.python import cp_model


def bool_or_sample_sat():
    model = cp_model.CpModel()

    x = model.new_bool_var("x")
    y = model.new_bool_var("y")

    model.add_bool_or([x, y.negated()])
    # The [] is not mandatory.
    # ~y is equivalent to y.negated()
    model.add_bool_or(x, ~y)


bool_or_sample_sat()

C++ code

#include <stdlib.h>

#include "absl/types/span.h"
#include "ortools/sat/cp_model.h"

namespace operations_research {
namespace sat {

void BoolOrSampleSat() {
  CpModelBuilder cp_model;

  const BoolVar x = cp_model.NewBoolVar();
  const BoolVar y = cp_model.NewBoolVar();
  cp_model.AddBoolOr({x, ~y});
  // You can also use the ~ operator.
  cp_model.AddBoolOr({x, ~y});
}

}  // namespace sat
}  // namespace operations_research

int main() {
  operations_research::sat::BoolOrSampleSat();

  return EXIT_SUCCESS;
}

Java code

package com.google.ortools.sat.samples;

import com.google.ortools.Loader;
import com.google.ortools.sat.BoolVar;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.Literal;

/** Code sample to demonstrates a simple Boolean constraint. */
public class BoolOrSampleSat {
  public static void main(String[] args) throws Exception {
    Loader.loadNativeLibraries();
    CpModel model = new CpModel();
    BoolVar x = model.newBoolVar("x");
    BoolVar y = model.newBoolVar("y");
    model.addBoolOr(new Literal[] {x, y.not()});
  }
}

C# code

using System;
using Google.OrTools.Sat;

public class BoolOrSampleSat
{
    static void Main()
    {
        CpModel model = new CpModel();

        BoolVar x = model.NewBoolVar("x");
        BoolVar y = model.NewBoolVar("y");

        model.AddBoolOr(new ILiteral[] { x, y.Not() });
    }
}

Go code

// The bool_or_sample_sat command is simple example of the BoolOr constraint.
package main

import (
	"github.com/google/or-tools/ortools/sat/go/cpmodel"
)

func boolOrSampleSat() {
	model := cpmodel.NewCpModelBuilder()

	x := model.NewBoolVar()
	y := model.NewBoolVar()

	model.AddBoolOr(x, y.Not())
}

func main() {
	boolOrSampleSat()
}

Reified constraints

The CP-SAT solver supports half-reified constraints, also called implications, which are of the form:

x implies constraint

where the constraint must hold if x is true.

Please note that this is not an equivalence relation. The constraint can still be true if x is false.

So we can write b => And(x, not y). That is, if b is true, then x is true and y is false. Note that in this particular example, there are multiple ways to express this constraint: you can also write (b => x) and (b => not y), which then is written as Or(not b, x) and Or(not b, not y).

Python code

#!/usr/bin/env python3
"""Simple model with a reified constraint."""

from ortools.sat.python import cp_model


def reified_sample_sat():
    """Showcase creating a reified constraint."""
    model = cp_model.CpModel()

    x = model.new_bool_var("x")
    y = model.new_bool_var("y")
    b = model.new_bool_var("b")

    # First version using a half-reified bool and.
    model.add_bool_and(x, ~y).only_enforce_if(b)

    # Second version using implications.
    model.add_implication(b, x)
    model.add_implication(b, ~y)

    # Third version using bool or.
    model.add_bool_or(~b, x)
    model.add_bool_or(~b, ~y)


reified_sample_sat()

C++ code

#include <stdlib.h>

#include "absl/types/span.h"
#include "ortools/sat/cp_model.h"

namespace operations_research {
namespace sat {

void ReifiedSampleSat() {
  CpModelBuilder cp_model;

  const BoolVar x = cp_model.NewBoolVar();
  const BoolVar y = cp_model.NewBoolVar();
  const BoolVar b = cp_model.NewBoolVar();

  // First version using a half-reified bool and.
  cp_model.AddBoolAnd({x, ~y}).OnlyEnforceIf(b);

  // Second version using implications.
  cp_model.AddImplication(b, x);
  cp_model.AddImplication(b, ~y);

  // Third version using bool or.
  cp_model.AddBoolOr({~b, x});
  cp_model.AddBoolOr({~b, ~y});
}

}  // namespace sat
}  // namespace operations_research

int main() {
  operations_research::sat::ReifiedSampleSat();

  return EXIT_SUCCESS;
}

Java code

package com.google.ortools.sat.samples;

import com.google.ortools.Loader;
import com.google.ortools.sat.BoolVar;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.Literal;

/**
 * Reification is the action of associating a Boolean variable to a constraint. This boolean
 * enforces or prohibits the constraint according to the value the Boolean variable is fixed to.
 *
 * <p>Half-reification is defined as a simple implication: If the Boolean variable is true, then the
 * constraint holds, instead of an complete equivalence.
 *
 * <p>The SAT solver offers half-reification. To implement full reification, two half-reified
 * constraints must be used.
 */
public class ReifiedSampleSat {
  public static void main(String[] args) throws Exception {
    Loader.loadNativeLibraries();
    CpModel model = new CpModel();

    BoolVar x = model.newBoolVar("x");
    BoolVar y = model.newBoolVar("y");
    BoolVar b = model.newBoolVar("b");

    // Version 1: a half-reified boolean and.
    model.addBoolAnd(new Literal[] {x, y.not()}).onlyEnforceIf(b);

    // Version 2: implications.
    model.addImplication(b, x);
    model.addImplication(b, y.not());

    // Version 3: boolean or.
    model.addBoolOr(new Literal[] {b.not(), x});
    model.addBoolOr(new Literal[] {b.not(), y.not()});
  }
}

C# code

using System;
using Google.OrTools.Sat;

public class ReifiedSampleSat
{
    static void Main()
    {
        CpModel model = new CpModel();

        BoolVar x = model.NewBoolVar("x");
        BoolVar y = model.NewBoolVar("y");
        BoolVar b = model.NewBoolVar("b");

        //  First version using a half-reified bool and.
        model.AddBoolAnd(new ILiteral[] { x, y.Not() }).OnlyEnforceIf(b);

        // Second version using implications.
        model.AddImplication(b, x);
        model.AddImplication(b, y.Not());

        // Third version using bool or.
        model.AddBoolOr(new ILiteral[] { b.Not(), x });
        model.AddBoolOr(new ILiteral[] { b.Not(), y.Not() });
    }
}

Go code

// The reified_sample_sat command is a simple example of implication constraints.
package main

import (
	"github.com/google/or-tools/ortools/sat/go/cpmodel"
)

func reifiedSampleSat() {
	model := cpmodel.NewCpModelBuilder()

	x := model.NewBoolVar()
	y := model.NewBoolVar()
	b := model.NewBoolVar()

	// First version using a half-reified bool and.
	model.AddBoolAnd(x, y.Not()).OnlyEnforceIf(b)

	// Second version using implications.
	model.AddImplication(b, x)
	model.AddImplication(b, y.Not())

	// Third version using bool or.
	model.AddBoolOr(b.Not(), x)
	model.AddBoolOr(b.Not(), y.Not())
}

func main() {
	reifiedSampleSat()
}

Product of two Boolean Variables

A useful construct is the product p of two Boolean variables x and y.

p == x * y

This is equivalent to the logical relation

p <=> x and y

This is encoded using one bool_or constraint and two implications. The following code samples output this truth table:

x = 0   y = 0   p = 0
x = 1   y = 0   p = 0
x = 0   y = 1   p = 0
x = 1   y = 1   p = 1

Python code

#!/usr/bin/env python3
"""Code sample that encodes the product of two Boolean variables."""


from ortools.sat.python import cp_model


def boolean_product_sample_sat():
    """Encoding of the product of two Boolean variables.

    p == x * y, which is the same as p <=> x and y
    """
    model = cp_model.CpModel()
    x = model.new_bool_var("x")
    y = model.new_bool_var("y")
    p = model.new_bool_var("p")

    # x and y implies p, rewrite as not(x and y) or p.
    model.add_bool_or(~x, ~y, p)

    # p implies x and y, expanded into two implications.
    model.add_implication(p, x)
    model.add_implication(p, y)

    # Create a solver and solve.
    solver = cp_model.CpSolver()
    solution_printer = cp_model.VarArraySolutionPrinter([x, y, p])
    solver.parameters.enumerate_all_solutions = True
    solver.solve(model, solution_printer)


boolean_product_sample_sat()

Go code

// The boolean_product_sample_sat command is a simple example of the product of two literals.
package main

import (
	"fmt"

	log "github.com/golang/glog"
	"github.com/google/or-tools/ortools/sat/go/cpmodel"
	sppb "github.com/google/or-tools/ortools/sat/proto/satparameters"
	"google.golang.org/protobuf/proto"
)

func booleanProductSample() error {
	model := cpmodel.NewCpModelBuilder()

	x := model.NewBoolVar().WithName("x")
	y := model.NewBoolVar().WithName("y")
	p := model.NewBoolVar().WithName("p")

	// x and y implies p, rewrite as not(x and y) or p.
	model.AddBoolOr(x.Not(), y.Not(), p)

	// p implies x and y, expanded into two implications.
	model.AddImplication(p, x)
	model.AddImplication(p, y)

	// Solve.
	m, err := model.Model()
	if err != nil {
		return fmt.Errorf("failed to instantiate the CP model: %w", err)
	}
	// Set `fill_additional_solutions_in_response` and `enumerate_all_solutions` to true so
	// the solver returns all solutions found.
	params := &sppb.SatParameters{
		FillAdditionalSolutionsInResponse: proto.Bool(true),
		EnumerateAllSolutions:             proto.Bool(true),
		SolutionPoolSize:                  proto.Int32(4),
	}
	response, err := cpmodel.SolveCpModelWithParameters(m, params)
	if err != nil {
		return fmt.Errorf("failed to solve the model: %w", err)
	}

	fmt.Printf("Status: %v\n", response.GetStatus())

	for _, additionalSolution := range response.GetAdditionalSolutions() {
		fmt.Printf("x: %v", additionalSolution.GetValues()[x.Index()])
		fmt.Printf(" y: %v", additionalSolution.GetValues()[y.Index()])
		fmt.Printf(" p: %v\n", additionalSolution.GetValues()[p.Index()])
	}

	return nil
}

func main() {
	err := booleanProductSample()
	if err != nil {
		log.Exitf("booleanProductSample returned with error: %v", err)
	}
}

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

boolean_logic.md

boolean_logic.md

Boolean logic recipes for the CP-SAT solver.

Introduction

Boolean variables and literals

Python code

C++ code

Java code

C# code

Go code

Boolean constraints

Python code

C++ code

Java code

C# code

Go code

Reified constraints

Python code

C++ code

Java code

C# code

Go code

Product of two Boolean Variables

Python code

Go code

Files

boolean_logic.md

Latest commit

History

boolean_logic.md

File metadata and controls

Boolean logic recipes for the CP-SAT solver.

Introduction

Boolean variables and literals

Python code

C++ code

Java code

C# code

Go code

Boolean constraints

Python code

C++ code

Java code

C# code

Go code

Reified constraints

Python code

C++ code

Java code

C# code

Go code

Product of two Boolean Variables

Python code

Go code