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
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
//! Pseudo-Boolean objective function.
use std::{collections::BTreeMap, rc::Rc};
use malachite_bigint::{BigInt, Sign};
use num_traits::{One, Zero};
use crate::prelude::*;
/// A pseudo-Boolean objective consists of a set of terms and a constant term.
///
/// This data structure preserves that the constraint is always stored in normalized form, i.e., the terms are over distinct variables, all coefficients are non-negative, and the terms are sorted by the index of the variable in the variable manager.
#[derive(Debug, Default, PartialEq)]
pub struct PBObjective {
pub terms: BTreeMap<VarIdx, GeneralPBTerm<BigInt>>,
pub constant: BigInt,
}
impl PBObjective {
/// Create a pseudo-Boolean objective by its terms and the constant term.
///
/// The terms do not need to be normalized. This function automatically normalizes the terms of the objective.
///
/// The parameter `is_maximization` determines if the coefficients and constant should be negated, as the objective is always considered to be minimized.
pub fn from_terms(
terms: Vec<GeneralPBTerm<BigInt>>,
mut constant: BigInt,
is_maximization: bool,
) -> Self {
let mut terms_map: BTreeMap<usize, GeneralPBTerm<BigInt>> = BTreeMap::new();
// Add terms to map and merging them if we have multiple terms talking about the same variable.
for term in terms {
if let Some(existing_term) = terms_map.get_mut(&term.lit.get_var()) {
constant += existing_term.add_with(term);
} else {
terms_map.insert(term.lit.get_var(), term);
}
}
// Change maximization to minimization.
if is_maximization {
constant = -constant;
for term in terms_map.values_mut() {
term.coeff = -&term.coeff;
}
}
// Normalize the terms to only have positive coefficients.
terms_map.retain(|_, t| !t.coeff.is_zero());
for term in terms_map.values_mut() {
if term.coeff.sign() == Sign::Minus {
term.change_negation();
constant -= &term.coeff;
}
}
PBObjective {
terms: terms_map,
constant,
}
}
/// Get the objective value for this objective under the `assignment`.
pub fn evaluate(&self, assignment: &Assignment<BooleanVar>) -> BigInt {
let mut value = self.constant.to_owned();
for term in self.terms.values() {
if let BoolValue::Assigned(true) = assignment.get_lit_value(term.lit) {
value += &term.coeff
}
}
value
}
/// Get the objective improving proofgoal with respect to the `substitution`, where the degree is initialized with `degree`.
#[inline]
fn get_proofgoal_init_degree(
&self,
substitution: &Substitution,
mut degree: BigInt,
) -> Rc<DBConstraint> {
let mut terms = Vec::new();
if self.terms.len() > substitution.len() {
// It is more efficient to linearly iterate through the substitution and access the terms.
for var_idx in substitution.support.iter() {
if let Some(term) = self.terms.get(var_idx) {
let var_maps_to = substitution.get(*var_idx).unwrap();
let lit_maps_to = if term.lit.is_negated() {
var_maps_to.into_negation()
} else {
var_maps_to
};
terms.push(term.clone());
match lit_maps_to {
SubstitutionValue::TRUE => degree += &term.coeff,
SubstitutionValue::FALSE => {}
lit => {
terms.push(GeneralPBTerm::new(-term.coeff.clone(), lit.get_lit()));
}
}
}
}
} else {
// It is more efficient to linearly iterate through the terms and access the substitution.
for term in self.terms.values() {
if let Some(lit_maps_to) = substitution.get_lit(term.lit) {
terms.push(term.clone());
match lit_maps_to {
SubstitutionValue::TRUE => degree += &term.coeff,
SubstitutionValue::FALSE => {}
lit => {
terms.push(GeneralPBTerm::new(-term.coeff.clone(), lit.get_lit()));
}
}
}
}
}
Rc::new(constraint_from_terms(terms, degree).into())
}
/// Get the objective improving proofgoal for redundance-based strengthening with respect to the `substitution`.
#[inline]
pub fn get_proofgoal(&self, substitution: &Substitution) -> Rc<DBConstraint> {
let degree = BigInt::zero();
self.get_proofgoal_init_degree(substitution, degree)
}
/// Get the strict objective improving proofgoal used for dominance-based strengthening with respect to the `substitution`.
#[inline]
pub fn get_proofgoal_strict(&self, substitution: &Substitution) -> Rc<DBConstraint> {
let degree = BigInt::one();
self.get_proofgoal_init_degree(substitution, degree)
}
/// Return the number of terms in [`PBObjective`].
#[inline]
pub fn len(&self) -> usize {
self.terms.len()
}
/// Check if [`PBObjective`] has no terms.
#[inline]
pub fn is_empty(&self) -> bool {
self.terms.len() == 0
}
}
impl ToPrettyString for PBObjective {
#[inline]
fn to_pretty_string(&self, var_names: &VarNameManager) -> String {
let mut out = String::with_capacity(self.len() * 4);
for term in self.terms.values() {
out.push_str(&term.coeff.to_string());
out.push(' ');
out.push_str(&term.lit.to_pretty_string(var_names));
out.push(' ');
}
out.push_str(&self.constant.to_string());
out
}
}