pumpkin-core 0.4.0

The core of the Pumpkin 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
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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
use super::independent_variable_value_brancher::IndependentVariableValueBrancher;
use crate::DefaultBrancher;
use crate::basic_types::DeletablePredicateIdGenerator;
use crate::basic_types::PredicateId;
use crate::basic_types::SolutionReference;
use crate::branching::Brancher;
use crate::branching::BrancherEvent;
use crate::branching::SelectionContext;
use crate::branching::value_selection::RandomSplitter;
use crate::branching::variable_selection::RandomSelector;
use crate::containers::KeyValueHeap;
use crate::containers::StorageKey;
use crate::create_statistics_struct;
use crate::engine::Assignments;
use crate::engine::predicates::predicate::Predicate;
use crate::propagation::ReadDomains;
use crate::results::Solution;
use crate::statistics::Statistic;
use crate::statistics::StatisticLogger;
use crate::statistics::moving_averages::CumulativeMovingAverage;
use crate::statistics::moving_averages::MovingAverage;
use crate::variables::DomainId;
/// A [`Brancher`] that combines [VSIDS \[1\]](https://dl.acm.org/doi/pdf/10.1145/378239.379017)
/// and [Solution-based phase saving \[2\]](https://people.eng.unimelb.edu.au/pstuckey/papers/lns-restarts.pdf).
///
/// There are three components:
/// 1. Predicate selection
/// 2. Truth value assignment
/// 3. Backup Selection
///
/// # Predicate selection
/// The VSIDS algorithm is an adaptation for the CP case. It determines which
/// [`Predicate`] should be branched on based on how often it appears in conflicts.
///
/// Intuitively, the more often a [`Predicate`] appears in *recent* conflicts, the more "important"
/// it is during the search process. VSIDS is originally from the SAT field (see \[1\]) but we
/// adapted it for constraint programming by considering [`Predicate`]s from recent conflicts
/// directly rather than Boolean variables.
///
/// # Truth value assignment
/// The truth value for the [`Predicate`] is selected to be consistent with the
/// best solution known so far. In this way, the search is directed around this existing solution.
///
/// In case where there is no known solution, then the predicate is assigned to true. This resembles
/// a fail-first strategy with the idea that the given predicate was encountered in conflicts, so
/// assigning it to true may cause another conflict soon.
///
/// # Backup selection
/// VSIDS relies on [`Predicate`]s appearing in conflicts to discover which [`Predicate`]s are
/// "important". However, it could be the case that all [`Predicate`]s which VSIDS has discovered
/// are already assigned.
///
/// In this case, [`AutonomousSearch`] defaults either to the backup described in
/// [`DefaultBrancher`] (when created using [`AutonomousSearch::default_over_all_variables`]) or it
/// defaults to the [`Brancher`] provided to [`AutonomousSearch::new`].
///
/// # Bibliography
/// \[1\] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, ‘Chaff: Engineering an
/// efficient SAT solver’, in Proceedings of the 38th annual Design Automation Conference, 2001.
///
/// \[2\] E. Demirović, G. Chu, and P. J. Stuckey, ‘Solution-based phase saving for CP: A
/// value-selection heuristic to simulate local search behavior in complete solvers’, in the
/// proceedings of the Principles and Practice of Constraint Programming (CP 2018).
#[derive(Debug)]
pub struct AutonomousSearch<BackupBrancher> {
    /// Predicates are mapped to ids. This is used internally in the heap.
    predicate_id_info: DeletablePredicateIdGenerator,
    /// Stores the activities for a predicate, represented with its id.
    heap: KeyValueHeap<PredicateId, f64>,
    /// After popping predicates off the heap that current have a truth value, the predicates are
    /// labelled as dormant because they do not contribute to VSIDS at the moment. When
    /// backtracking, dormant predicates are examined and readded to the heap. Dormant predicates
    /// with low activities are removed.
    dormant_predicates: Vec<Predicate>,
    /// How much the activity of a predicate is increased when it appears in a conflict.
    /// This value changes during search (see [`Vsids::decay_activities`]).
    increment: f64,
    /// The maximum allowed [`Vsids`] value, if this value is reached then all of the values are
    /// divided by this value. The increment is constant.
    max_threshold: f64,
    /// Whenever a conflict is found, the [`Vsids::increment`] is multiplied by
    /// 1 / [`Vsids::decay_factor`] (this is synonymous with increasing the
    /// [`Vsids::increment`] since 0 <= [`Vsids::decay_factor`] <= 1).
    /// The decay factor is constant.
    decay_factor: f64,
    /// Contains the best-known solution or [`None`] if no solution has been found.
    best_known_solution: Option<Solution>,
    /// If the heap does not contain any more unfixed predicates then this backup_brancher will be
    /// used instead.
    backup_brancher: BackupBrancher,
    /// The statistics gathered by the autonomous search
    statistics: AutonomousSearchStatistics,
    /// Whether synchronisation should take place in the next call to
    /// [`AutonomousSearch::next_decision`].
    ///
    /// This is used to prevent unnecessary work when [`AutonomousSearch::synchronise`] is called
    /// multiple times in a row without a call to [`AutonomousSearch::next_decision`].
    should_synchronise: bool,
}

create_statistics_struct!(AutonomousSearchStatistics {
    num_backup_called: usize,
    num_predicates_removed: usize,
    num_calls: usize,
    num_predicates_added: usize,
    average_size_of_heap: CumulativeMovingAverage<usize>,
    num_assigned_predicates_encountered: usize,
});

const DEFAULT_VSIDS_INCREMENT: f64 = 1.0;
const DEFAULT_VSIDS_MAX_THRESHOLD: f64 = 1e100;
const DEFAULT_VSIDS_DECAY_FACTOR: f64 = 0.95;
const DEFAULT_VSIDS_VALUE: f64 = 0.0;

impl DefaultBrancher {
    /// Creates a new instance with default values for
    /// the parameters (`1.0` for the increment, `1e100` for the max threshold,
    /// `0.95` for the decay factor and `0.0` for the initial VSIDS value).
    ///
    /// If there are no more predicates left to select, this [`Brancher`] switches to
    /// [`RandomSelector`] with [`RandomSplitter`].
    pub fn default_over_all_variables(assignments: &Assignments) -> DefaultBrancher {
        AutonomousSearch {
            predicate_id_info: DeletablePredicateIdGenerator::default(),
            heap: KeyValueHeap::default(),
            dormant_predicates: vec![],
            increment: DEFAULT_VSIDS_INCREMENT,
            max_threshold: DEFAULT_VSIDS_MAX_THRESHOLD,
            decay_factor: DEFAULT_VSIDS_DECAY_FACTOR,
            best_known_solution: None,
            should_synchronise: false,
            backup_brancher: IndependentVariableValueBrancher::new(
                RandomSelector::new(assignments.get_domains()),
                RandomSplitter,
            ),
            statistics: Default::default(),
        }
    }

    pub fn add_domain(&mut self, domain: DomainId) {
        self.backup_brancher.variable_selector.add_domain(domain);
    }
}

impl<BackupSelector> AutonomousSearch<BackupSelector> {
    /// Creates a new instance with default values for
    /// the parameters (`1.0` for the increment, `1e100` for the max threshold,
    /// `0.95` for the decay factor and `0.0` for the initial VSIDS value).
    ///
    /// Uses the `backup_brancher` in case there are no more predicates to be selected by VSIDS.
    pub fn new(backup_brancher: BackupSelector) -> Self {
        AutonomousSearch {
            predicate_id_info: DeletablePredicateIdGenerator::default(),
            heap: KeyValueHeap::default(),
            dormant_predicates: vec![],
            increment: DEFAULT_VSIDS_INCREMENT,
            max_threshold: DEFAULT_VSIDS_MAX_THRESHOLD,
            decay_factor: DEFAULT_VSIDS_DECAY_FACTOR,
            best_known_solution: None,
            should_synchronise: false,
            backup_brancher,
            statistics: Default::default(),
        }
    }

    /// Resizes the heap to accommodate for the id.
    /// Recall that the underlying heap uses direct hashing.
    fn resize_heap(&mut self, id: PredicateId) {
        while self.heap.len() <= id.index() {
            self.heap.grow(id, DEFAULT_VSIDS_VALUE);
        }
    }

    /// Bumps the activity of a predicate by [`Vsids::increment`].
    /// Used when a predicate is encountered during a conflict.
    fn bump_activity(&mut self, predicate: Predicate) {
        self.statistics.num_predicates_added +=
            (!self.predicate_id_info.has_id_for_predicate(predicate)) as usize;
        let id = self.predicate_id_info.get_id(predicate);
        self.resize_heap(id);
        self.heap.restore_key(id);

        // Scale the activities if the values are too large.
        // Also remove predicates that have activities close to zero.
        let activity = self.heap.get_value(id);
        if activity + self.increment >= self.max_threshold {
            // Adjust heap values.
            self.heap.divide_values(self.max_threshold);

            // Adjust increment. It is important to adjust the increment after the above code.
            self.increment /= self.max_threshold;
        }
        // Now perform the standard bumping
        self.heap.increment(id, self.increment);
    }

    /// Decays the activities (i.e. increases the [`Vsids::increment`] by multiplying it
    /// with 1 / [`Vsids::decay_factor`]) such that future bumps (see
    /// [`Vsids::bump_activity`]) is more impactful.
    ///
    /// Doing it in this manner is cheaper than dividing each activity value eagerly.
    fn decay_activities(&mut self) {
        self.increment *= 1.0 / self.decay_factor;
    }

    fn next_candidate_predicate(&mut self, context: &mut SelectionContext) -> Option<Predicate> {
        loop {
            // We peek the next variable, since we do not pop since we do not (yet) want to
            // remove the value from the heap.
            if let Some((candidate, _)) = self.heap.peek_max() {
                let predicate = self
                    .predicate_id_info
                    .get_predicate(*candidate)
                    .expect("Expected predicate id to exist");
                if context.is_predicate_assigned(predicate) {
                    self.statistics.num_assigned_predicates_encountered += 1;
                    let _ = self.heap.pop_max();

                    // We know that this predicate is now dormant
                    let predicate_id = self.predicate_id_info.get_id(predicate);
                    self.heap.delete_key(predicate_id);
                    self.predicate_id_info.delete_id(predicate_id);
                    self.dormant_predicates.push(predicate);
                } else {
                    return Some(predicate);
                }
            } else {
                return None;
            }
        }
    }

    /// Determines whether the provided [`Predicate`] should be returned as is or whether its
    /// negation should be returned. This is determined based on its assignment in the best-known
    /// solution.
    ///
    /// For example, if we have found the solution `x = 5` then the call `determine_polarity([x >=
    /// 3])` would return `true`.
    fn determine_polarity(&self, predicate: Predicate) -> Predicate {
        if let Some(solution) = &self.best_known_solution {
            // We have a solution
            if !solution.contains_domain_id(predicate.get_domain()) {
                // This can occur if an encoding is used
                return predicate;
            }
            // Match the truth value according to the best solution.
            if solution.evaluate_predicate(predicate) == Some(true) {
                predicate
            } else {
                !predicate
            }
        } else {
            // We do not have a solution to match against, we simply return the predicate with
            // positive polarity
            predicate
        }
    }

    fn synchronise_internal(&mut self) {
        // We drain the dormant predicates and add them back to the heap; we could check here
        // whether the predicates are already satisfied but this appeared to introduce too much
        // overhead in some cases.
        self.dormant_predicates.drain(..).for_each(|predicate| {
            let id = self.predicate_id_info.get_id(predicate);

            while self.heap.len() <= id.index() {
                self.heap.grow(id, DEFAULT_VSIDS_VALUE);
            }

            self.heap.restore_key(id);
        });
    }
}

impl<BackupBrancher: Brancher> Brancher for AutonomousSearch<BackupBrancher> {
    fn next_decision(&mut self, context: &mut SelectionContext) -> Option<Predicate> {
        if self.should_synchronise {
            self.synchronise_internal();
            self.should_synchronise = false;
        }
        self.statistics.num_calls += 1;
        self.statistics
            .average_size_of_heap
            .add_term(self.heap.num_nonremoved_elements());
        let result = self
            .next_candidate_predicate(context)
            .map(|predicate| self.determine_polarity(predicate));
        if result.is_none() && !context.are_all_variables_assigned() {
            // There are variables for which we do not have a predicate, rely on the backup
            self.statistics.num_backup_called += 1;
            self.backup_brancher.next_decision(context)
        } else {
            result
        }
    }

    fn log_statistics(&self, statistic_logger: StatisticLogger) {
        let statistic_logger = statistic_logger.attach_to_prefix("AutonomousSearch");
        self.statistics.log(statistic_logger);
    }

    fn on_backtrack(&mut self) {
        self.backup_brancher.on_backtrack()
    }

    /// Restores dormant predicates after backtracking.
    fn synchronise(&mut self, context: &mut SelectionContext) {
        self.should_synchronise = true;
        self.backup_brancher.synchronise(context);
    }

    fn on_conflict(&mut self) {
        self.decay_activities();
        self.backup_brancher.on_conflict();
    }

    fn on_solution(&mut self, solution: SolutionReference) {
        // We store the best known solution
        self.best_known_solution = Some(solution.into());
        self.backup_brancher.on_solution(solution);
    }

    fn on_appearance_in_conflict_predicate(&mut self, predicate: Predicate) {
        self.bump_activity(predicate);
        self.backup_brancher
            .on_appearance_in_conflict_predicate(predicate);
    }

    fn on_restart(&mut self) {
        self.backup_brancher.on_restart();
    }

    fn on_unassign_integer(&mut self, variable: DomainId, value: i32) {
        self.backup_brancher.on_unassign_integer(variable, value)
    }

    fn is_restart_pointless(&mut self) -> bool {
        false
    }

    fn subscribe_to_events(&self) -> Vec<BrancherEvent> {
        [
            BrancherEvent::Solution,
            BrancherEvent::Conflict,
            BrancherEvent::Backtrack,
            BrancherEvent::Synchronise,
            BrancherEvent::AppearanceInConflictPredicate,
        ]
        .into_iter()
        .chain(self.backup_brancher.subscribe_to_events())
        .collect()
    }
}

#[cfg(test)]
mod tests {
    use super::AutonomousSearch;
    use crate::basic_types::tests::TestRandom;
    use crate::branching::Brancher;
    use crate::branching::SelectionContext;
    use crate::engine::Assignments;
    use crate::engine::notifications::NotificationEngine;
    use crate::predicate;
    use crate::results::SolutionReference;

    #[test]
    fn brancher_picks_bumped_values() {
        let mut assignments = Assignments::default();
        let x = assignments.grow(0, 10);
        let y = assignments.grow(-10, 0);

        let mut brancher = AutonomousSearch::default_over_all_variables(&assignments);
        brancher.on_appearance_in_conflict_predicate(predicate!(x >= 5));
        brancher.on_appearance_in_conflict_predicate(predicate!(x >= 5));
        brancher.on_appearance_in_conflict_predicate(predicate!(y >= -5));

        (0..100).for_each(|_| brancher.on_conflict());
    }

    #[test]
    fn dormant_values() {
        let mut notification_engine = NotificationEngine::default();
        let mut assignments = Assignments::default();
        let x = assignments.grow(0, 10);
        notification_engine.grow();

        let mut brancher = AutonomousSearch::default_over_all_variables(&assignments);

        let predicate = predicate!(x >= 5);
        brancher.on_appearance_in_conflict_predicate(predicate);
        let decision = brancher.next_decision(&mut SelectionContext::new(
            &assignments,
            &mut TestRandom::default(),
        ));
        assert_eq!(decision, Some(predicate));

        assignments.new_checkpoint();
        // Decision Level 1
        let _ = assignments.post_predicate(predicate!(x >= 5), None, &mut notification_engine);

        assignments.new_checkpoint();
        // Decision Level 2
        let _ = assignments.post_predicate(predicate!(x >= 7), None, &mut notification_engine);

        assignments.new_checkpoint();
        // Decision Level 3
        let _ = assignments.post_predicate(predicate!(x >= 10), None, &mut notification_engine);

        assignments.new_checkpoint();
        // We end at decision level 4

        let decision = brancher.next_decision(&mut SelectionContext::new(
            &assignments,
            &mut TestRandom::default(),
        ));
        assert!(decision.is_none());
        assert!(brancher.dormant_predicates.contains(&predicate));

        let _ = assignments.synchronise(3, &mut notification_engine);

        let decision = brancher.next_decision(&mut SelectionContext::new(
            &assignments,
            &mut TestRandom::default(),
        ));
        assert!(decision.is_none());
        assert!(brancher.dormant_predicates.contains(&predicate));

        let _ = assignments.synchronise(0, &mut notification_engine);
        brancher.synchronise(&mut SelectionContext::new(
            &assignments,
            &mut TestRandom::default(),
        ));

        let decision = brancher.next_decision(&mut SelectionContext::new(
            &assignments,
            &mut TestRandom::default(),
        ));
        assert_eq!(decision, Some(predicate));
        assert!(!brancher.dormant_predicates.contains(&predicate));
    }

    #[test]
    fn uses_fallback() {
        let mut assignments = Assignments::default();
        let x = assignments.grow(0, 10);

        let mut brancher = AutonomousSearch::default_over_all_variables(&assignments);

        let result = brancher.next_decision(&mut SelectionContext::new(
            &assignments,
            &mut TestRandom {
                integers: vec![2],
                usizes: vec![0],
                bools: vec![false],
                weighted_choice: |_| unreachable!(),
            },
        ));

        assert_eq!(result, Some(predicate!(x <= 2)));
    }

    #[test]
    fn uses_stored_solution() {
        let mut notification_engine = NotificationEngine::default();
        let mut assignments = Assignments::default();
        let x = assignments.grow(0, 10);
        notification_engine.grow();

        assignments.new_checkpoint();
        let _ = assignments.post_predicate(predicate!(x == 7), None, &mut notification_engine);

        let mut brancher = AutonomousSearch::default_over_all_variables(&assignments);

        brancher.on_solution(SolutionReference::new(&assignments));

        let _ = assignments.synchronise(0, &mut notification_engine);

        assert_eq!(
            predicate!(x >= 5),
            brancher.determine_polarity(predicate!(x >= 5))
        );
        assert_eq!(
            !predicate!(x >= 10),
            brancher.determine_polarity(predicate!(x >= 10))
        );
        assert_eq!(
            predicate!(x <= 8),
            brancher.determine_polarity(predicate!(x <= 8))
        );
        assert_eq!(
            !predicate!(x <= 5),
            brancher.determine_polarity(predicate!(x <= 5))
        );

        brancher.on_appearance_in_conflict_predicate(predicate!(x >= 5));

        let result = brancher.next_decision(&mut SelectionContext::new(
            &assignments,
            &mut TestRandom::default(),
        ));
        assert_eq!(result, Some(predicate!(x >= 5)));
    }
}