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

//! Contains the representation of a unsatisfiable solution.

#[cfg(doc)]
use crate::Solver;
use crate::branching::Brancher;
use crate::engine::ConstraintSatisfactionSolver;
use crate::engine::constraint_satisfaction_solver::CoreExtractionResult;
use crate::predicates::Predicate;

/// A struct which allows the retrieval of an unsatisfiable core consisting of the provided
/// assumptions passed to the initial [`Solver::satisfy_under_assumptions`].
///
/// Note that when this struct is dropped (using [`Drop`]) then the [`Solver`] is reset.
#[derive(Debug)]
pub struct UnsatisfiableUnderAssumptions<'solver, 'brancher, B: Brancher> {
    pub(crate) solver: &'solver mut ConstraintSatisfactionSolver,
    pub(crate) brancher: &'brancher mut B,
}

impl<'solver, 'brancher, B: Brancher> UnsatisfiableUnderAssumptions<'solver, 'brancher, B> {
    pub fn new(
        solver: &'solver mut ConstraintSatisfactionSolver,
        brancher: &'brancher mut B,
    ) -> Self {
        UnsatisfiableUnderAssumptions { solver, brancher }
    }

    /// Extract an unsatisfiable core in terms of the assumptions.
    ///
    /// In general, a core is a (sub)set of the constraints which together are unsatisfiable; in the
    /// case of constraint programming, this means a set of constraints which are together
    /// unsatisfiable; for example, if we have one variable `x ∈ [0, 10]` and we have the two
    /// constraints `5 * x >= 25` and `[x <= 4]` then it can be observed that these constraints can
    /// never be true at the same time.
    ///
    /// In an assumption-based solver, a core is defined as a (sub)set of assumptions which, given a
    /// set of constraints, when set together will lead to an unsatisfiable instance. For
    /// example, if we three variables `x, y, z ∈ {0, 1, 2}` and we have the constraint
    /// `all-different(x, y, z)` then the assumptions `[[x = 1], [y <= 1], [y != 0]]` would
    /// constitute an unsatisfiable core since the constraint and the assumptions can never be
    /// satisfied at the same time.
    ///
    /// One of the main examples in which this assumption interface is used is MaxSAT in which
    /// core-guided solvers generate multiple cores while to solve the instance \[1\]. This
    /// core-guided search technique has been translated to CP in \[2\].
    ///
    ///
    /// # Bibliography
    /// \[1\] Z. Fu and S. Malik, ‘On solving the partial MAX-SAT problem’, in International
    /// Conference on Theory and Applications of Satisfiability Testing, 2006, pp. 252–265.
    ///
    /// \[2\] G. Gange, J. Berg, E. Demirović, and P. J. Stuckey, ‘Core-guided and core-boosted
    /// search for CP’, in Integration of Constraint Programming, Artificial Intelligence, and
    /// Operations Research: 17th International Conference, CPAIOR 2020, Vienna, Austria, September
    /// 21--24, 2020, Proceedings 17, 2020, pp. 205–221.
    pub fn extract_core(&mut self) -> Box<[Predicate]> {
        match self.solver.extract_clausal_core(self.brancher) {
            CoreExtractionResult::ConflictingAssumption(conflicting_assumption) => {
                panic!(
                    "Conflicting assumptions were provided, found both {conflicting_assumption:?} and {:?}",
                    !conflicting_assumption
                )
            }
            CoreExtractionResult::Core(core) => core.into(),
        }
    }
}

impl<B: Brancher> Drop for UnsatisfiableUnderAssumptions<'_, '_, B> {
    fn drop(&mut self) {
        self.solver.restore_state_at_root(self.brancher)
    }
}