Trait NegatableConstraint 

pub trait NegatableConstraint: Constraint {
    type NegatedConstraint: NegatableConstraint + 'static;

    // Required method
    fn negation(&self) -> Self::NegatedConstraint;

    // Provided method
    fn reify(
        self,
        solver: &mut Solver,
        reification_literal: Literal,
    ) -> Result<(), ConstraintOperationError>
       where Self: Sized { ... }
}

A Constraint which has a well-defined negation.

Having a negation means the Constraint can be fully reified; i.e., a constraint C can be turned into r <-> C where r is a reification literal.

For example, the negation of the Constraint a = b is (well-)defined as a != b.

Required Associated Types

type NegatedConstraint: NegatableConstraint + 'static

Required Methods

fn negation(&self) -> Self::NegatedConstraint

Provided Methods

fn reify( self, solver: &mut Solver, reification_literal: Literal, ) -> Result<(), ConstraintOperationError>

where Self: Sized,

Add the reified version of the Constraint to the Solver; i.e. post the constraint r <-> constraint where r is a reification literal.

This method returns a ConstraintOperationError if the addition of the Constraint led to a root-level conflict.

The tag allows inferences to be traced to the constraint that implies them. They will show up in the proof log.

Examples found in repository

examples/disjunctive_scheduling.rs (line 77)

fn main() {
    let mut args = std::env::args();

    let n_tasks = args
        .nth(1)
        .expect("Please provide a number of tasks")
        .parse::<usize>()
        .expect("Not a valid usized");
    let processing_times = args
        .take(n_tasks)
        .map(|arg| arg.parse::<usize>())
        .collect::<Result<Vec<_>, _>>()
        .expect("The provided processing times are not valid unsigned integers");
    assert_eq!(
        processing_times.len(),
        n_tasks,
        "Provided fewer than `n_tasks` processing times."
    );

    let horizon = processing_times.iter().sum::<usize>();

    let mut solver = Solver::default();

    // Creates a dummy constraint tag; since this example does not support proof logging the
    // constraint tag does not matter.
    let constraint_tag = solver.new_constraint_tag();

    let start_variables = (0..n_tasks)
        .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
        .collect::<Vec<_>>();

    // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
    // starts)
    let precedence_literals = (0..n_tasks)
        .map(|_| {
            (0..n_tasks)
                .map(|_| solver.new_literal())
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>();

    for x in 0..n_tasks {
        for y in 0..n_tasks {
            if x == y {
                continue;
            }
            // precedence_literals[x][y] <=> x ends before y starts
            let literal = precedence_literals[x][y];
            // literal <=> (s_x + p_x <= s_y)
            // equivelent to literal <=> (s_x - s_y <= -p_x)
            // So the variables are -s_y and s_x, and the rhs is -p_x
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(
                variables,
                -(processing_times[x] as i32),
                constraint_tag,
            )
            .reify(&mut solver, literal);

            // Either x starts before y or y start before x
            let _ = solver.add_clause(
                [
                    literal.get_true_predicate(),
                    precedence_literals[y][x].get_true_predicate(),
                ],
                constraint_tag,
            );
        }
    }

    let mut brancher = solver.default_brancher();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable(_, _),
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(satisfiable) => {
            let solution = satisfiable.solution();

            let mut start_variables_and_processing_times = start_variables
                .iter()
                .zip(processing_times)
                .collect::<Vec<_>>();
            start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
                solution
                    .get_integer_value(**s1)
                    .cmp(&solution.get_integer_value(**s2))
            });

            println!(
                "{}",
                start_variables_and_processing_times
                    .iter()
                    .map(|(var, processing_time)| format!(
                        "[{}, {}]",
                        solution.get_integer_value(**var),
                        solution.get_integer_value(**var) + *processing_time as i32
                    ))
                    .collect::<Vec<_>>()
                    .join(" - ")
            );
        }
        SatisfactionResult::Unsatisfiable(_, _) => panic!("Infeasibility Detected"),
        SatisfactionResult::Unknown(_, _) => println!("Timeout."),
    };
}

Implementors