pub trait ProblemSolution: HasAssignments {
// Provided methods
fn num_domains(&self) -> usize { ... }
fn get_integer_value<Var>(&self, var: Var) -> i32
where Var: IntegerVariable { ... }
fn get_literal_value(&self, literal: Literal) -> bool { ... }
}Expand description
A trait which specifies the common behaviours of Solution and SolutionReference.
Provided Methods§
Sourcefn num_domains(&self) -> usize
fn num_domains(&self) -> usize
Returns the number of defined DomainIds.
Sourcefn get_integer_value<Var>(&self, var: Var) -> i32where
Var: IntegerVariable,
fn get_integer_value<Var>(&self, var: Var) -> i32where
Var: IntegerVariable,
Examples found in repository?
examples/nqueens.rs (line 97)
25fn main() {
26 let Cli {
27 n,
28 proof: proof_path,
29 } = Cli::parse();
30
31 if n < 2 {
32 println!("Please provide an 'n > 1'");
33 return;
34 }
35
36 let Ok(proof_log) = proof_path
37 .as_ref()
38 .map(|path| ProofLog::cp(path, true))
39 .transpose()
40 .map(|proof| proof.unwrap_or_default())
41 else {
42 eprintln!(
43 "Failed to create proof file at {}",
44 proof_path.unwrap().display()
45 );
46 return;
47 };
48
49 let mut solver = Solver::with_options(SolverOptions {
50 proof_log,
51 ..Default::default()
52 });
53
54 // Create the constraint tags for the three all_different constraints.
55 let c1_tag = solver.new_constraint_tag();
56 let c2_tag = solver.new_constraint_tag();
57 let c3_tag = solver.new_constraint_tag();
58
59 let variables = (0..n)
60 .map(|i| solver.new_named_bounded_integer(0, n as i32 - 1, format!("q{i}")))
61 .collect::<Vec<_>>();
62
63 let _ = solver
64 .add_constraint(constraints::all_different(variables.clone(), c1_tag))
65 .post();
66
67 let diag1 = variables
68 .iter()
69 .cloned()
70 .enumerate()
71 .map(|(i, var)| var.offset(i as i32))
72 .collect::<Vec<_>>();
73 let diag2 = variables
74 .iter()
75 .cloned()
76 .enumerate()
77 .map(|(i, var)| var.offset(-(i as i32)))
78 .collect::<Vec<_>>();
79
80 let _ = solver
81 .add_constraint(constraints::all_different(diag1, c2_tag))
82 .post();
83 let _ = solver
84 .add_constraint(constraints::all_different(diag2, c3_tag))
85 .post();
86
87 let mut brancher = solver.default_brancher();
88 match solver.satisfy(&mut brancher, &mut Indefinite) {
89 SatisfactionResult::Satisfiable(satisfiable) => {
90 let solution = satisfiable.solution();
91
92 let row_separator = format!("{}+", "+---".repeat(n as usize));
93
94 for row in 0..n {
95 println!("{row_separator}");
96
97 let queen_col = solution.get_integer_value(variables[row as usize]) as u32;
98
99 for col in 0..n {
100 let string = if queen_col == col { "| * " } else { "| " };
101
102 print!("{string}");
103 }
104
105 println!("|");
106 }
107
108 println!("{row_separator}");
109 }
110 SatisfactionResult::Unsatisfiable(_, _) => {
111 println!("{n}-queens is unsatisfiable.");
112 }
113 SatisfactionResult::Unknown(_, _) => {
114 println!("Timeout.");
115 }
116 };
117}More examples
examples/bibd.rs (line 159)
75fn main() {
76 env_logger::init();
77
78 let Some(bibd) = Bibd::from_args() else {
79 eprintln!("Usage: {} <v> <k> <l>", std::env::args().next().unwrap());
80 return;
81 };
82
83 println!(
84 "bibd: (v = {}, b = {}, r = {}, k = {}, l = {})",
85 bibd.rows, bibd.columns, bibd.row_sum, bibd.column_sum, bibd.max_dot_product
86 );
87
88 let mut solver = Solver::default();
89
90 // Creates a dummy constraint tag; since this example does not support proof logging the
91 // constraint tag does not matter.
92 let constraint_tag = solver.new_constraint_tag();
93
94 // Create 0-1 integer variables that make up the matrix.
95 let matrix = create_matrix(&mut solver, &bibd);
96
97 // Enforce the row sum.
98 for row in matrix.iter() {
99 let _ = solver
100 .add_constraint(constraints::equals(
101 row.clone(),
102 bibd.row_sum as i32,
103 constraint_tag,
104 ))
105 .post();
106 }
107
108 // Enforce the column sum.
109 for row in transpose(&matrix) {
110 let _ = solver
111 .add_constraint(constraints::equals(
112 row,
113 bibd.column_sum as i32,
114 constraint_tag,
115 ))
116 .post();
117 }
118
119 // Enforce the dot product constraint.
120 // pairwise_product[r1][r2][col] = matrix[r1][col] * matrix[r2][col]
121 let pairwise_product = (0..bibd.rows)
122 .map(|_| create_matrix(&mut solver, &bibd))
123 .collect::<Vec<_>>();
124
125 for r1 in 0..bibd.rows as usize {
126 for r2 in r1 + 1..bibd.rows as usize {
127 for col in 0..bibd.columns as usize {
128 let _ = solver
129 .add_constraint(constraints::times(
130 matrix[r1][col],
131 matrix[r2][col],
132 pairwise_product[r1][r2][col],
133 constraint_tag,
134 ))
135 .post();
136 }
137
138 let _ = solver
139 .add_constraint(constraints::less_than_or_equals(
140 pairwise_product[r1][r2].clone(),
141 bibd.max_dot_product as i32,
142 constraint_tag,
143 ))
144 .post();
145 }
146 }
147
148 let mut brancher = solver.default_brancher();
149 match solver.satisfy(&mut brancher, &mut Indefinite) {
150 SatisfactionResult::Satisfiable(satisfiable) => {
151 let solution = satisfiable.solution();
152
153 let row_separator = format!("{}+", "+---".repeat(bibd.columns as usize));
154
155 for row in matrix.iter() {
156 let line = row
157 .iter()
158 .map(|var| {
159 if solution.get_integer_value(*var) == 1 {
160 String::from("| * ")
161 } else {
162 String::from("| ")
163 }
164 })
165 .collect::<String>();
166
167 println!("{row_separator}\n{line}|");
168 }
169
170 println!("{row_separator}");
171 }
172 SatisfactionResult::Unsatisfiable(_, _) => {
173 println!("UNSATISFIABLE")
174 }
175 SatisfactionResult::Unknown(_, _) => {
176 println!("UNKNOWN")
177 }
178 };
179}examples/disjunctive_scheduling.rs (line 107)
20fn main() {
21 let mut args = std::env::args();
22
23 let n_tasks = args
24 .nth(1)
25 .expect("Please provide a number of tasks")
26 .parse::<usize>()
27 .expect("Not a valid usized");
28 let processing_times = args
29 .take(n_tasks)
30 .map(|arg| arg.parse::<usize>())
31 .collect::<Result<Vec<_>, _>>()
32 .expect("The provided processing times are not valid unsigned integers");
33 assert_eq!(
34 processing_times.len(),
35 n_tasks,
36 "Provided fewer than `n_tasks` processing times."
37 );
38
39 let horizon = processing_times.iter().sum::<usize>();
40
41 let mut solver = Solver::default();
42
43 // Creates a dummy constraint tag; since this example does not support proof logging the
44 // constraint tag does not matter.
45 let constraint_tag = solver.new_constraint_tag();
46
47 let start_variables = (0..n_tasks)
48 .map(|i| solver.new_bounded_integer(0, (horizon - processing_times[i]) as i32))
49 .collect::<Vec<_>>();
50
51 // Literal which indicates precedence (i.e. precedence_literals[x][y] <=> x ends before y
52 // starts)
53 let precedence_literals = (0..n_tasks)
54 .map(|_| {
55 (0..n_tasks)
56 .map(|_| solver.new_literal())
57 .collect::<Vec<_>>()
58 })
59 .collect::<Vec<_>>();
60
61 for x in 0..n_tasks {
62 for y in 0..n_tasks {
63 if x == y {
64 continue;
65 }
66 // precedence_literals[x][y] <=> x ends before y starts
67 let literal = precedence_literals[x][y];
68 // literal <=> (s_x + p_x <= s_y)
69 // equivelent to literal <=> (s_x - s_y <= -p_x)
70 // So the variables are -s_y and s_x, and the rhs is -p_x
71 let variables = vec![start_variables[y].scaled(-1), start_variables[x].scaled(1)];
72 let _ = constraints::less_than_or_equals(
73 variables,
74 -(processing_times[x] as i32),
75 constraint_tag,
76 )
77 .reify(&mut solver, literal);
78
79 // Either x starts before y or y start before x
80 let _ = solver.add_clause(
81 [
82 literal.get_true_predicate(),
83 precedence_literals[y][x].get_true_predicate(),
84 ],
85 constraint_tag,
86 );
87 }
88 }
89
90 let mut brancher = solver.default_brancher();
91 if matches!(
92 solver.satisfy(&mut brancher, &mut Indefinite),
93 SatisfactionResult::Unsatisfiable(_, _),
94 ) {
95 panic!("Infeasibility Detected")
96 }
97 match solver.satisfy(&mut brancher, &mut Indefinite) {
98 SatisfactionResult::Satisfiable(satisfiable) => {
99 let solution = satisfiable.solution();
100
101 let mut start_variables_and_processing_times = start_variables
102 .iter()
103 .zip(processing_times)
104 .collect::<Vec<_>>();
105 start_variables_and_processing_times.sort_by(|(s1, _), (s2, _)| {
106 solution
107 .get_integer_value(**s1)
108 .cmp(&solution.get_integer_value(**s2))
109 });
110
111 println!(
112 "{}",
113 start_variables_and_processing_times
114 .iter()
115 .map(|(var, processing_time)| format!(
116 "[{}, {}]",
117 solution.get_integer_value(**var),
118 solution.get_integer_value(**var) + *processing_time as i32
119 ))
120 .collect::<Vec<_>>()
121 .join(" - ")
122 );
123 }
124 SatisfactionResult::Unsatisfiable(_, _) => panic!("Infeasibility Detected"),
125 SatisfactionResult::Unknown(_, _) => println!("Timeout."),
126 };
127}fn get_literal_value(&self, literal: Literal) -> bool
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.