pumpkin_solver

Struct Solver

Source 
pub struct Solver { /* private fields */ }
Expand description

The main interaction point which allows the creation of variables, the addition of constraints, and solving problems.

§Creating Variables

As stated in crate::variables, we can create two types of variables: propositional variables and integer variables.

let mut solver = Solver::default();

// Integer Variables

// We can create an integer variable with a domain in the range [0, 10]
let integer_between_bounds = solver.new_bounded_integer(0, 10);

// We can also create such a variable with a name
let named_integer_between_bounds = solver.new_named_bounded_integer(0, 10, "x");

// We can also create an integer variable with a non-continuous domain in the follow way
let mut sparse_integer = solver.new_sparse_integer(vec![0, 3, 5]);

// We can also create such a variable with a name
let named_sparse_integer = solver.new_named_sparse_integer(vec![0, 3, 5], "y");

// Additionally, we can also create an affine view over a variable with both a scale and an offset (or either)
let view_over_integer = integer_between_bounds.scaled(-1).offset(15);


// Propositional Variable

// We can create a literal
let literal = solver.new_literal();

// We can also create such a variable with a name
let named_literal = solver.new_named_literal("z");

// We can also get the propositional variable from the literal
let propositional_variable = literal.get_propositional_variable();

// We can also create an iterator of new literals and get a number of them at once
let list_of_5_literals = solver.new_literals().take(5).collect::<Vec<_>>();
assert_eq!(list_of_5_literals.len(), 5);

§Using the Solver

For examples on how to use the solver, see the root-level crate documentation or one of these examples.

Implementations§

Source§

impl Solver

Source

pub fn with_options( learning_options: LearningOptions, solver_options: SolverOptions, ) -> Self

Creates a solver with the provided LearningOptions and SolverOptions.

Examples found in repository?
examples/nqueens.rs (lines 51-57)
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
fn main() {
    let Cli {
        n,
        proof: proof_path,
    } = Cli::parse();

    if n < 2 {
        println!("Please provide an 'n > 1'");
        return;
    }

    let Ok(proof_log) = proof_path
        .as_ref()
        .map(|path| ProofLog::cp(path, Format::Text, true, true))
        .transpose()
        .map(|proof| proof.unwrap_or_default())
    else {
        eprintln!(
            "Failed to create proof file at {}",
            proof_path.unwrap().display()
        );
        return;
    };

    let mut solver = Solver::with_options(
        LearningOptions::default(),
        pumpkin_solver::options::SolverOptions {
            proof_log,
            ..Default::default()
        },
    );

    let variables = (0..n)
        .map(|i| solver.new_named_bounded_integer(0, n as i32 - 1, format!("q{i}")))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(variables.clone()))
        .with_tag(NonZero::new(1).unwrap())
        .post();

    let diag1 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(i as i32))
        .collect::<Vec<_>>();
    let diag2 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(-(i as i32)))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(diag1))
        .with_tag(NonZero::new(2).unwrap())
        .post();
    let _ = solver
        .add_constraint(constraints::all_different(diag2))
        .with_tag(NonZero::new(3).unwrap())
        .post();

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(solution) => {
            let row_separator = format!("{}+", "+---".repeat(n as usize));

            for row in 0..n {
                println!("{row_separator}");

                let queen_col = solution.get_integer_value(variables[row as usize]) as u32;

                for col in 0..n {
                    let string = if queen_col == col { "| * " } else { "|   " };

                    print!("{string}");
                }

                println!("|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable => {
            println!("{n}-queens is unsatisfiable.");
        }
        SatisfactionResult::Unknown => {
            println!("Timeout.");
        }
    }
}
Source

pub fn with_solution_callback( &mut self, solution_callback: impl Fn(SolutionCallbackArguments<'_, '_>) + 'static, )

Adds a call-back to the Solver which is called every time that a solution is found when optimising using Solver::maximise or Solver::minimise.

Note that this will also perform the call-back on the optimal solution which is returned in OptimisationResult::Optimal.

Source

pub fn log_statistics_with_objective(&self, objective_value: i64)

Logs the statistics currently present in the solver with the provided objective value.

Source

pub fn log_statistics(&self)

Logs the statistics currently present in the solver.

Source§

impl Solver

Methods to retrieve information about variables

Source

pub fn get_literal(&self, predicate: Predicate) -> Literal

Get the literal corresponding to the given predicate. As the literal may need to be created, this possibly mutates the solver.

§Example
let mut solver = Solver::default();

let x = solver.new_bounded_integer(0, 10);

// We can get the literal representing the predicate `[x >= 3]` via the Solver
let literal = solver.get_literal(predicate!(x >= 3));

// Note that we can also get a literal which is always true
let true_lower_bound_literal = solver.get_literal(predicate!(x >= 0));
assert_eq!(true_lower_bound_literal, solver.get_true_literal());
Source

pub fn get_literal_value(&self, literal: Literal) -> Option<bool>

Get the value of the given Literal at the root level (after propagation), which could be unassigned.

Source

pub fn get_true_literal(&self) -> Literal

Get a literal which is globally true.

Source

pub fn get_false_literal(&self) -> Literal

Get a literal which is globally false.

Source

pub fn lower_bound(&self, variable: &impl IntegerVariable) -> i32

Get the lower-bound of the given IntegerVariable at the root level (after propagation).

Source

pub fn upper_bound(&self, variable: &impl IntegerVariable) -> i32

Get the upper-bound of the given IntegerVariable at the root level (after propagation).

Source§

impl Solver

Functions to create and retrieve integer and propositional variables.

Source

pub fn new_literals(&mut self) -> impl Iterator<Item = Literal> + '_

Returns an infinite iterator of positive literals of new variables. The new variables will be unnamed.

§Example
let mut solver = Solver::default();
let literals: Vec<Literal> = solver.new_literals().take(5).collect();

// `literals` contains 5 positive literals of newly created propositional variables.
assert_eq!(literals.len(), 5);

Note that this method captures the lifetime of the immutable reference to self.

Source

pub fn new_literal(&mut self) -> Literal

Create a fresh propositional variable and return the literal with positive polarity.

§Example
let mut solver = Solver::default();

// We can create a literal
let literal = solver.new_literal();
Examples found in repository?
examples/disjunctive_scheduling.rs (line 46)
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
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();

    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. if precedence_literals[x][y] => s_y + p_y <= s_x
    // which is equal to s_y - s_x <= -p_y)
    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;
            }
            let literal = precedence_literals[x][y];
            let variables = vec![start_variables[y].scaled(1), start_variables[x].scaled(-1)];
            // literal => s_y - s_x <= -p_y)
            let _ =
                constraints::less_than_or_equals(variables.clone(), -(processing_times[y] as i32))
                    .implied_by(&mut solver, literal, None);

            //-literal => -s_y + s_x <= p_y)
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(variables.clone(), processing_times[y] as i32)
                .implied_by(&mut solver, literal, None);

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

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable,
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::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."),
    }
}
Source

pub fn new_named_literal(&mut self, name: impl Into<String>) -> Literal

Create a fresh propositional variable with a given name and return the literal with positive polarity.

§Example
let mut solver = Solver::default();

// We can also create such a variable with a name
let named_literal = solver.new_named_literal("z");
Source

pub fn new_bounded_integer( &mut self, lower_bound: i32, upper_bound: i32, ) -> DomainId

Create a new integer variable with the given bounds.

§Example
let mut solver = Solver::default();

// We can create an integer variable with a domain in the range [0, 10]
let integer_between_bounds = solver.new_bounded_integer(0, 10);
Examples found in repository?
examples/bibd.rs (line 70)
66
67
68
69
70
71
72
73
74
fn create_matrix(solver: &mut Solver, bibd: &BIBD) -> Vec<Vec<DomainId>> {
    (0..bibd.rows)
        .map(|_| {
            (0..bibd.columns)
                .map(|_| solver.new_bounded_integer(0, 1))
                .collect::<Vec<_>>()
        })
        .collect::<Vec<_>>()
}
More examples
Hide additional examples
examples/disjunctive_scheduling.rs (line 38)
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
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();

    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. if precedence_literals[x][y] => s_y + p_y <= s_x
    // which is equal to s_y - s_x <= -p_y)
    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;
            }
            let literal = precedence_literals[x][y];
            let variables = vec![start_variables[y].scaled(1), start_variables[x].scaled(-1)];
            // literal => s_y - s_x <= -p_y)
            let _ =
                constraints::less_than_or_equals(variables.clone(), -(processing_times[y] as i32))
                    .implied_by(&mut solver, literal, None);

            //-literal => -s_y + s_x <= p_y)
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(variables.clone(), processing_times[y] as i32)
                .implied_by(&mut solver, literal, None);

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

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable,
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::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."),
    }
}
Source

pub fn new_named_bounded_integer( &mut self, lower_bound: i32, upper_bound: i32, name: impl Into<String>, ) -> DomainId

Create a new named integer variable with the given bounds.

§Example
let mut solver = Solver::default();

// We can also create such a variable with a name
let named_integer_between_bounds = solver.new_named_bounded_integer(0, 10, "x");
Examples found in repository?
examples/nqueens.rs (line 60)
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
fn main() {
    let Cli {
        n,
        proof: proof_path,
    } = Cli::parse();

    if n < 2 {
        println!("Please provide an 'n > 1'");
        return;
    }

    let Ok(proof_log) = proof_path
        .as_ref()
        .map(|path| ProofLog::cp(path, Format::Text, true, true))
        .transpose()
        .map(|proof| proof.unwrap_or_default())
    else {
        eprintln!(
            "Failed to create proof file at {}",
            proof_path.unwrap().display()
        );
        return;
    };

    let mut solver = Solver::with_options(
        LearningOptions::default(),
        pumpkin_solver::options::SolverOptions {
            proof_log,
            ..Default::default()
        },
    );

    let variables = (0..n)
        .map(|i| solver.new_named_bounded_integer(0, n as i32 - 1, format!("q{i}")))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(variables.clone()))
        .with_tag(NonZero::new(1).unwrap())
        .post();

    let diag1 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(i as i32))
        .collect::<Vec<_>>();
    let diag2 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(-(i as i32)))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(diag1))
        .with_tag(NonZero::new(2).unwrap())
        .post();
    let _ = solver
        .add_constraint(constraints::all_different(diag2))
        .with_tag(NonZero::new(3).unwrap())
        .post();

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(solution) => {
            let row_separator = format!("{}+", "+---".repeat(n as usize));

            for row in 0..n {
                println!("{row_separator}");

                let queen_col = solution.get_integer_value(variables[row as usize]) as u32;

                for col in 0..n {
                    let string = if queen_col == col { "| * " } else { "|   " };

                    print!("{string}");
                }

                println!("|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable => {
            println!("{n}-queens is unsatisfiable.");
        }
        SatisfactionResult::Unknown => {
            println!("Timeout.");
        }
    }
}
Source

pub fn new_sparse_integer(&mut self, values: impl Into<Vec<i32>>) -> DomainId

Create a new integer variable which has a domain of predefined values. We remove duplicates by converting to a hash set

§Example
let mut solver = Solver::default();

// We can also create an integer variable with a non-continuous domain in the follow way
let mut sparse_integer = solver.new_sparse_integer(vec![0, 3, 5]);
Source

pub fn new_named_sparse_integer( &mut self, values: impl Into<Vec<i32>>, name: impl Into<String>, ) -> DomainId

Create a new named integer variable which has a domain of predefined values.

§Example
let mut solver = Solver::default();

// We can also create such a variable with a name
let named_sparse_integer = solver.new_named_sparse_integer(vec![0, 3, 5], "y");
Source§

impl Solver

Functions for solving with the constraints that have been added to the Solver.

Source

pub fn satisfy<B: Brancher, T: TerminationCondition>( &mut self, brancher: &mut B, termination: &mut T, ) -> SatisfactionResult

Solves the current model in the Solver until it finds a solution (or is indicated to terminate by the provided TerminationCondition) and returns a SatisfactionResult which can be used to obtain the found solution or find other solutions.

Examples found in repository?
examples/nqueens.rs (line 91)
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
fn main() {
    let Cli {
        n,
        proof: proof_path,
    } = Cli::parse();

    if n < 2 {
        println!("Please provide an 'n > 1'");
        return;
    }

    let Ok(proof_log) = proof_path
        .as_ref()
        .map(|path| ProofLog::cp(path, Format::Text, true, true))
        .transpose()
        .map(|proof| proof.unwrap_or_default())
    else {
        eprintln!(
            "Failed to create proof file at {}",
            proof_path.unwrap().display()
        );
        return;
    };

    let mut solver = Solver::with_options(
        LearningOptions::default(),
        pumpkin_solver::options::SolverOptions {
            proof_log,
            ..Default::default()
        },
    );

    let variables = (0..n)
        .map(|i| solver.new_named_bounded_integer(0, n as i32 - 1, format!("q{i}")))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(variables.clone()))
        .with_tag(NonZero::new(1).unwrap())
        .post();

    let diag1 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(i as i32))
        .collect::<Vec<_>>();
    let diag2 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(-(i as i32)))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(diag1))
        .with_tag(NonZero::new(2).unwrap())
        .post();
    let _ = solver
        .add_constraint(constraints::all_different(diag2))
        .with_tag(NonZero::new(3).unwrap())
        .post();

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(solution) => {
            let row_separator = format!("{}+", "+---".repeat(n as usize));

            for row in 0..n {
                println!("{row_separator}");

                let queen_col = solution.get_integer_value(variables[row as usize]) as u32;

                for col in 0..n {
                    let string = if queen_col == col { "| * " } else { "|   " };

                    print!("{string}");
                }

                println!("|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable => {
            println!("{n}-queens is unsatisfiable.");
        }
        SatisfactionResult::Unknown => {
            println!("Timeout.");
        }
    }
}
More examples
Hide additional examples
examples/bibd.rs (line 136)
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
fn main() {
    env_logger::init();

    let Some(bibd) = BIBD::from_args() else {
        eprintln!("Usage: {} <v> <k> <l>", std::env::args().next().unwrap());
        return;
    };

    println!(
        "bibd: (v = {}, b = {}, r = {}, k = {}, l = {})",
        bibd.rows, bibd.columns, bibd.row_sum, bibd.column_sum, bibd.max_dot_product
    );

    let mut solver = Solver::default();

    // Create 0-1 integer variables that make up the matrix.
    let matrix = create_matrix(&mut solver, &bibd);

    // Enforce the row sum.
    for row in matrix.iter() {
        let _ = solver
            .add_constraint(constraints::equals(row.clone(), bibd.row_sum as i32))
            .post();
    }

    // Enforce the column sum.
    for row in transpose(&matrix) {
        let _ = solver
            .add_constraint(constraints::equals(row, bibd.column_sum as i32))
            .post();
    }

    // Enforce the dot product constraint.
    // pairwise_product[r1][r2][col] = matrix[r1][col] * matrix[r2][col]
    let pairwise_product = (0..bibd.rows)
        .map(|_| create_matrix(&mut solver, &bibd))
        .collect::<Vec<_>>();

    for r1 in 0..bibd.rows as usize {
        for r2 in r1 + 1..bibd.rows as usize {
            for col in 0..bibd.columns as usize {
                let _ = solver
                    .add_constraint(constraints::times(
                        matrix[r1][col],
                        matrix[r2][col],
                        pairwise_product[r1][r2][col],
                    ))
                    .post();
            }

            let _ = solver
                .add_constraint(constraints::less_than_or_equals(
                    pairwise_product[r1][r2].clone(),
                    bibd.max_dot_product as i32,
                ))
                .post();
        }
    }

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(solution) => {
            let row_separator = format!("{}+", "+---".repeat(bibd.columns as usize));

            for row in matrix.iter() {
                let line = row
                    .iter()
                    .map(|var| {
                        if solution.get_integer_value(*var) == 1 {
                            String::from("| * ")
                        } else {
                            String::from("|   ")
                        }
                    })
                    .collect::<String>();

                println!("{row_separator}\n{line}|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable => {
            println!("UNSATISFIABLE")
        }
        SatisfactionResult::Unknown => {
            println!("UNKNOWN")
        }
    }
}
examples/disjunctive_scheduling.rs (line 75)
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
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();

    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. if precedence_literals[x][y] => s_y + p_y <= s_x
    // which is equal to s_y - s_x <= -p_y)
    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;
            }
            let literal = precedence_literals[x][y];
            let variables = vec![start_variables[y].scaled(1), start_variables[x].scaled(-1)];
            // literal => s_y - s_x <= -p_y)
            let _ =
                constraints::less_than_or_equals(variables.clone(), -(processing_times[y] as i32))
                    .implied_by(&mut solver, literal, None);

            //-literal => -s_y + s_x <= p_y)
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(variables.clone(), processing_times[y] as i32)
                .implied_by(&mut solver, literal, None);

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

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable,
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::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."),
    }
}
Source

pub fn get_solution_iterator<'this, 'brancher, 'termination, B: Brancher, T: TerminationCondition>( &'this mut self, brancher: &'brancher mut B, termination: &'termination mut T, ) -> SolutionIterator<'this, 'brancher, 'termination, B, T>

Source

pub fn satisfy_under_assumptions<'this, 'brancher, B: Brancher, T: TerminationCondition>( &'this mut self, brancher: &'brancher mut B, termination: &mut T, assumptions: &[Literal], ) -> SatisfactionResultUnderAssumptions<'this, 'brancher, B>

Solves the current model in the Solver until it finds a solution (or is indicated to terminate by the provided TerminationCondition) and returns a SatisfactionResult which can be used to obtain the found solution or find other solutions.

This method takes as input a list of Literals which represent so-called assumptions (see [1] for a more detailed explanation). The Literals corresponding to Predicates over IntegerVariables (e.g. lower-bound predicates) can be retrieved from the Solver using Solver::get_literal.

§Bibliography

[1] N. Eén and N. Sörensson, ‘Temporal induction by incremental SAT solving’, Electronic Notes in Theoretical Computer Science, vol. 89, no. 4, pp. 543–560, 2003.

Source

pub fn minimise( &mut self, brancher: &mut impl Brancher, termination: &mut impl TerminationCondition, objective_variable: impl IntegerVariable, ) -> OptimisationResult

Solves the model currently in the Solver to optimality where the provided objective_variable is minimised (or is indicated to terminate by the provided TerminationCondition).

It returns an OptimisationResult which can be used to retrieve the optimal solution if it exists.

Source

pub fn maximise( &mut self, brancher: &mut impl Brancher, termination: &mut impl TerminationCondition, objective_variable: impl IntegerVariable, ) -> OptimisationResult

Solves the model currently in the Solver to optimality where the provided objective_variable is maximised (or is indicated to terminate by the provided TerminationCondition).

It returns an OptimisationResult which can be used to retrieve the optimal solution if it exists.

Source§

impl Solver

Functions for adding new constraints to the solver.

Source

pub fn add_constraint<Constraint>( &mut self, constraint: Constraint, ) -> ConstraintPoster<'_, Constraint>

Add a constraint to the solver. This returns a ConstraintPoster which enables control on whether to add the constraint as-is, or whether to (half) reify it.

If none of the methods on ConstraintPoster are used, the constraint is not actually added to the solver. In this case, a warning is emitted.

§Example
let mut solver = Solver::default();

let a = solver.new_bounded_integer(0, 3);
let b = solver.new_bounded_integer(0, 3);

solver.add_constraint(constraints::equals([a, b], 0)).post();
Examples found in repository?
examples/nqueens.rs (line 64)
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
fn main() {
    let Cli {
        n,
        proof: proof_path,
    } = Cli::parse();

    if n < 2 {
        println!("Please provide an 'n > 1'");
        return;
    }

    let Ok(proof_log) = proof_path
        .as_ref()
        .map(|path| ProofLog::cp(path, Format::Text, true, true))
        .transpose()
        .map(|proof| proof.unwrap_or_default())
    else {
        eprintln!(
            "Failed to create proof file at {}",
            proof_path.unwrap().display()
        );
        return;
    };

    let mut solver = Solver::with_options(
        LearningOptions::default(),
        pumpkin_solver::options::SolverOptions {
            proof_log,
            ..Default::default()
        },
    );

    let variables = (0..n)
        .map(|i| solver.new_named_bounded_integer(0, n as i32 - 1, format!("q{i}")))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(variables.clone()))
        .with_tag(NonZero::new(1).unwrap())
        .post();

    let diag1 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(i as i32))
        .collect::<Vec<_>>();
    let diag2 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(-(i as i32)))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(diag1))
        .with_tag(NonZero::new(2).unwrap())
        .post();
    let _ = solver
        .add_constraint(constraints::all_different(diag2))
        .with_tag(NonZero::new(3).unwrap())
        .post();

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(solution) => {
            let row_separator = format!("{}+", "+---".repeat(n as usize));

            for row in 0..n {
                println!("{row_separator}");

                let queen_col = solution.get_integer_value(variables[row as usize]) as u32;

                for col in 0..n {
                    let string = if queen_col == col { "| * " } else { "|   " };

                    print!("{string}");
                }

                println!("|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable => {
            println!("{n}-queens is unsatisfiable.");
        }
        SatisfactionResult::Unknown => {
            println!("Timeout.");
        }
    }
}
More examples
Hide additional examples
examples/bibd.rs (line 97)
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
fn main() {
    env_logger::init();

    let Some(bibd) = BIBD::from_args() else {
        eprintln!("Usage: {} <v> <k> <l>", std::env::args().next().unwrap());
        return;
    };

    println!(
        "bibd: (v = {}, b = {}, r = {}, k = {}, l = {})",
        bibd.rows, bibd.columns, bibd.row_sum, bibd.column_sum, bibd.max_dot_product
    );

    let mut solver = Solver::default();

    // Create 0-1 integer variables that make up the matrix.
    let matrix = create_matrix(&mut solver, &bibd);

    // Enforce the row sum.
    for row in matrix.iter() {
        let _ = solver
            .add_constraint(constraints::equals(row.clone(), bibd.row_sum as i32))
            .post();
    }

    // Enforce the column sum.
    for row in transpose(&matrix) {
        let _ = solver
            .add_constraint(constraints::equals(row, bibd.column_sum as i32))
            .post();
    }

    // Enforce the dot product constraint.
    // pairwise_product[r1][r2][col] = matrix[r1][col] * matrix[r2][col]
    let pairwise_product = (0..bibd.rows)
        .map(|_| create_matrix(&mut solver, &bibd))
        .collect::<Vec<_>>();

    for r1 in 0..bibd.rows as usize {
        for r2 in r1 + 1..bibd.rows as usize {
            for col in 0..bibd.columns as usize {
                let _ = solver
                    .add_constraint(constraints::times(
                        matrix[r1][col],
                        matrix[r2][col],
                        pairwise_product[r1][r2][col],
                    ))
                    .post();
            }

            let _ = solver
                .add_constraint(constraints::less_than_or_equals(
                    pairwise_product[r1][r2].clone(),
                    bibd.max_dot_product as i32,
                ))
                .post();
        }
    }

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(solution) => {
            let row_separator = format!("{}+", "+---".repeat(bibd.columns as usize));

            for row in matrix.iter() {
                let line = row
                    .iter()
                    .map(|var| {
                        if solution.get_integer_value(*var) == 1 {
                            String::from("| * ")
                        } else {
                            String::from("|   ")
                        }
                    })
                    .collect::<String>();

                println!("{row_separator}\n{line}|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable => {
            println!("UNSATISFIABLE")
        }
        SatisfactionResult::Unknown => {
            println!("UNKNOWN")
        }
    }
}
Source

pub fn add_clause( &mut self, clause: impl IntoIterator<Item = Literal>, ) -> Result<(), ConstraintOperationError>

Creates a clause from literals and adds it to the current formula.

If the formula becomes trivially unsatisfiable, a ConstraintOperationError will be returned. Subsequent calls to this method will always return an error, and no modification of the solver will take place.

Examples found in repository?
examples/disjunctive_scheduling.rs (line 69)
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
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();

    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. if precedence_literals[x][y] => s_y + p_y <= s_x
    // which is equal to s_y - s_x <= -p_y)
    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;
            }
            let literal = precedence_literals[x][y];
            let variables = vec![start_variables[y].scaled(1), start_variables[x].scaled(-1)];
            // literal => s_y - s_x <= -p_y)
            let _ =
                constraints::less_than_or_equals(variables.clone(), -(processing_times[y] as i32))
                    .implied_by(&mut solver, literal, None);

            //-literal => -s_y + s_x <= p_y)
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(variables.clone(), processing_times[y] as i32)
                .implied_by(&mut solver, literal, None);

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

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable,
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::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."),
    }
}
Source§

impl Solver

Default brancher implementation

Source

pub fn default_brancher_over_all_propositional_variables( &self, ) -> DefaultBrancher

Creates a default IndependentVariableValueBrancher which uses Vsids as VariableSelector and SolutionGuidedValueSelector (with PhaseSaving as its back-up selector) as its ValueSelector; it searches over all PropositionalVariables defined in the provided solver.

Examples found in repository?
examples/nqueens.rs (line 90)
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
fn main() {
    let Cli {
        n,
        proof: proof_path,
    } = Cli::parse();

    if n < 2 {
        println!("Please provide an 'n > 1'");
        return;
    }

    let Ok(proof_log) = proof_path
        .as_ref()
        .map(|path| ProofLog::cp(path, Format::Text, true, true))
        .transpose()
        .map(|proof| proof.unwrap_or_default())
    else {
        eprintln!(
            "Failed to create proof file at {}",
            proof_path.unwrap().display()
        );
        return;
    };

    let mut solver = Solver::with_options(
        LearningOptions::default(),
        pumpkin_solver::options::SolverOptions {
            proof_log,
            ..Default::default()
        },
    );

    let variables = (0..n)
        .map(|i| solver.new_named_bounded_integer(0, n as i32 - 1, format!("q{i}")))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(variables.clone()))
        .with_tag(NonZero::new(1).unwrap())
        .post();

    let diag1 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(i as i32))
        .collect::<Vec<_>>();
    let diag2 = variables
        .iter()
        .cloned()
        .enumerate()
        .map(|(i, var)| var.offset(-(i as i32)))
        .collect::<Vec<_>>();

    let _ = solver
        .add_constraint(constraints::all_different(diag1))
        .with_tag(NonZero::new(2).unwrap())
        .post();
    let _ = solver
        .add_constraint(constraints::all_different(diag2))
        .with_tag(NonZero::new(3).unwrap())
        .post();

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(solution) => {
            let row_separator = format!("{}+", "+---".repeat(n as usize));

            for row in 0..n {
                println!("{row_separator}");

                let queen_col = solution.get_integer_value(variables[row as usize]) as u32;

                for col in 0..n {
                    let string = if queen_col == col { "| * " } else { "|   " };

                    print!("{string}");
                }

                println!("|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable => {
            println!("{n}-queens is unsatisfiable.");
        }
        SatisfactionResult::Unknown => {
            println!("Timeout.");
        }
    }
}
More examples
Hide additional examples
examples/bibd.rs (line 135)
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
fn main() {
    env_logger::init();

    let Some(bibd) = BIBD::from_args() else {
        eprintln!("Usage: {} <v> <k> <l>", std::env::args().next().unwrap());
        return;
    };

    println!(
        "bibd: (v = {}, b = {}, r = {}, k = {}, l = {})",
        bibd.rows, bibd.columns, bibd.row_sum, bibd.column_sum, bibd.max_dot_product
    );

    let mut solver = Solver::default();

    // Create 0-1 integer variables that make up the matrix.
    let matrix = create_matrix(&mut solver, &bibd);

    // Enforce the row sum.
    for row in matrix.iter() {
        let _ = solver
            .add_constraint(constraints::equals(row.clone(), bibd.row_sum as i32))
            .post();
    }

    // Enforce the column sum.
    for row in transpose(&matrix) {
        let _ = solver
            .add_constraint(constraints::equals(row, bibd.column_sum as i32))
            .post();
    }

    // Enforce the dot product constraint.
    // pairwise_product[r1][r2][col] = matrix[r1][col] * matrix[r2][col]
    let pairwise_product = (0..bibd.rows)
        .map(|_| create_matrix(&mut solver, &bibd))
        .collect::<Vec<_>>();

    for r1 in 0..bibd.rows as usize {
        for r2 in r1 + 1..bibd.rows as usize {
            for col in 0..bibd.columns as usize {
                let _ = solver
                    .add_constraint(constraints::times(
                        matrix[r1][col],
                        matrix[r2][col],
                        pairwise_product[r1][r2][col],
                    ))
                    .post();
            }

            let _ = solver
                .add_constraint(constraints::less_than_or_equals(
                    pairwise_product[r1][r2].clone(),
                    bibd.max_dot_product as i32,
                ))
                .post();
        }
    }

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::Satisfiable(solution) => {
            let row_separator = format!("{}+", "+---".repeat(bibd.columns as usize));

            for row in matrix.iter() {
                let line = row
                    .iter()
                    .map(|var| {
                        if solution.get_integer_value(*var) == 1 {
                            String::from("| * ")
                        } else {
                            String::from("|   ")
                        }
                    })
                    .collect::<String>();

                println!("{row_separator}\n{line}|");
            }

            println!("{row_separator}");
        }
        SatisfactionResult::Unsatisfiable => {
            println!("UNSATISFIABLE")
        }
        SatisfactionResult::Unknown => {
            println!("UNKNOWN")
        }
    }
}
examples/disjunctive_scheduling.rs (line 73)
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
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();

    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. if precedence_literals[x][y] => s_y + p_y <= s_x
    // which is equal to s_y - s_x <= -p_y)
    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;
            }
            let literal = precedence_literals[x][y];
            let variables = vec![start_variables[y].scaled(1), start_variables[x].scaled(-1)];
            // literal => s_y - s_x <= -p_y)
            let _ =
                constraints::less_than_or_equals(variables.clone(), -(processing_times[y] as i32))
                    .implied_by(&mut solver, literal, None);

            //-literal => -s_y + s_x <= p_y)
            let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
            let _ = constraints::less_than_or_equals(variables.clone(), processing_times[y] as i32)
                .implied_by(&mut solver, literal, None);

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

    let mut brancher = solver.default_brancher_over_all_propositional_variables();
    if matches!(
        solver.satisfy(&mut brancher, &mut Indefinite),
        SatisfactionResult::Unsatisfiable,
    ) {
        panic!("Infeasibility Detected")
    }
    match solver.satisfy(&mut brancher, &mut Indefinite) {
        SatisfactionResult::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."),
    }
}

Trait Implementations§

Source§

impl Debug for Solver

Source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more
Source§

impl Default for Solver

Source§

fn default() -> Self

Returns the “default value” for a type. Read more

Auto Trait Implementations§

§

impl Freeze for Solver

§

impl !RefUnwindSafe for Solver

§

impl !Send for Solver

§

impl !Sync for Solver

§

impl Unpin for Solver

§

impl !UnwindSafe for Solver

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T> IntoEither for T

Source§

fn into_either(self, into_left: bool) -> Either<Self, Self>

Converts self into a Left variant of Either<Self, Self> if into_left is true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more
Source§

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
where F: FnOnce(&Self) -> bool,

Converts self into a Left variant of Either<Self, Self> if into_left(&self) returns true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
Source§

impl<V, T> VZip<V> for T
where V: MultiLane<T>,

Source§

fn vzip(self) -> V