cp_sat 0.4.0

Rust bindings to the Google CP-SAT constraint programming solver.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
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

use cp_sat::builder::CpModelBuilder;
use cp_sat::proto::{CpSolverStatus, SatParameters};

#[test]
fn presentation_problem() {
    let mut model = CpModelBuilder::default();
    let domain = [(0, 2)];
    let x = model.new_int_var_with_name(domain, "x");
    let y = model.new_int_var_with_name(domain, "y");
    let z = model.new_int_var_with_name(domain, "z");

    model.add_ne(x, y);

    let response = model.solve();
    println!("{:?}", response);

    assert_eq!(response.status(), CpSolverStatus::Optimal);
    let x_val = x.solution_value(&response);
    let y_val = y.solution_value(&response);
    let z_val = z.solution_value(&response);
    println!("x = {}", x_val);
    println!("y = {}", y_val);
    println!("z = {}", z_val);

    assert!(x_val != y_val);
    assert!(0 <= x_val && x_val <= 2);
    assert!(0 <= y_val && y_val <= 2);
    assert!(0 <= z_val && z_val <= 2);
}

#[test]
fn solving_a_cp_problem() {
    let mut model = CpModelBuilder::default();
    let var_upper_bound = vec![50, 45, 37].into_iter().max().unwrap();
    let x = model.new_int_var_with_name([(0, var_upper_bound)], "x");
    let y = model.new_int_var_with_name([(0, var_upper_bound)], "y");
    let z = model.new_int_var_with_name([(0, var_upper_bound)], "z");

    model.add_le([(2, x), (7, y), (3, z)], 50);
    model.add_le([(3, x), (-5, y), (7, z)], 45);
    model.add_le([(5, x), (2, y), (-6, z)], 37);

    model.maximize([(2, x), (2, y), (3, z)]);

    let response = model.solve();
    assert_eq!(response.status(), CpSolverStatus::Optimal);
    let x_val = x.solution_value(&response);
    let y_val = y.solution_value(&response);
    let z_val = z.solution_value(&response);
    println!("objective: {}", response.objective_value);
    println!("x = {}", x_val);
    println!("y = {}", y_val);
    println!("z = {}", z_val);

    assert_eq!(35., response.objective_value);
    assert!(2 * x_val + 7 * y_val + 3 * z_val <= 50);
    assert!(3 * x_val - 5 * y_val + 7 * z_val <= 45);
    assert!(5 * x_val + 2 * y_val - 6 * z_val <= 37);
}

#[test]
fn solve_with_time_limit_sample_sat() {
    let mut model = CpModelBuilder::default();
    let domain = [(0, 2)];
    let x = model.new_int_var_with_name(domain, "x");
    let y = model.new_int_var_with_name(domain, "y");
    let z = model.new_int_var_with_name(domain, "z");

    model.add_ne(x, y);

    let mut params = SatParameters::default();
    params.max_time_in_seconds = Some(10.);

    let response = model.solve_with_parameters(&params);
    println!("{:?}", response);

    assert_eq!(response.status(), CpSolverStatus::Optimal);
    let x_val = x.solution_value(&response);
    let y_val = y.solution_value(&response);
    let z_val = z.solution_value(&response);
    println!("x = {}", x_val);
    println!("y = {}", y_val);
    println!("z = {}", z_val);
}