pumpkin-solver 0.5.0

The Pumpkin combinatorial optimisation solver library.
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

#![cfg(test)] // workaround for https://github.com/rust-lang/rust-clippy/issues/11024

use std::path::PathBuf;

use pumpkin_conflict_resolvers::resolvers::ResolutionResolver;
use pumpkin_solver::Solver;
use pumpkin_solver::core::options::SolverOptions;
use pumpkin_solver::core::predicate;
use pumpkin_solver::core::proof::ProofLog;
use pumpkin_solver::core::results::SatisfactionResult;
use pumpkin_solver::core::termination::Indefinite;

#[test]
fn proof_with_reified_literals() {
    let mut solver = Solver::with_options(SolverOptions {
        proof_log: ProofLog::cp(&PathBuf::from("/tmp/solver_proof.drcp"), true)
            .expect("created proof"),
        ..Default::default()
    });

    let constraint_tag = solver.new_constraint_tag();
    let variable = solver.new_named_bounded_integer(1, 10, "var");
    let literal = solver.new_literal_for_predicate(predicate![variable == 5], constraint_tag);

    solver
        .add_constraint(pumpkin_constraints::clause(vec![literal], constraint_tag))
        .post();

    solver
        .add_constraint(pumpkin_constraints::not_equals(
            [variable],
            5,
            constraint_tag,
        ))
        .post();

    let mut brancher = solver.default_brancher();
    let mut resolver = ResolutionResolver::default();

    let result = solver.satisfy(&mut brancher, &mut Indefinite, &mut resolver);
    assert!(matches!(result, SatisfactionResult::Unsatisfiable(_, _, _)));
}

#[test]
fn proof_with_equality_unit_nogood_step() {
    let mut solver = Solver::with_options(SolverOptions {
        proof_log: ProofLog::cp(&PathBuf::from("/tmp/solver_proof.drcp"), true)
            .expect("created proof"),
        ..Default::default()
    });

    let constraint_tag = solver.new_constraint_tag();

    let x1 = solver.new_named_bounded_integer(1, 2, "x1");
    let x2 = solver.new_named_bounded_integer(1, 1, "x2");
    solver
        .add_constraint(pumpkin_constraints::binary_not_equals(
            x1,
            x2,
            constraint_tag,
        ))
        .post();

    solver
        .add_constraint(pumpkin_constraints::less_than_or_equals(
            [x1],
            1,
            constraint_tag,
        ))
        .post();

    let mut brancher = solver.default_brancher();
    let mut resolver = ResolutionResolver::default();

    let result = solver.satisfy(&mut brancher, &mut Indefinite, &mut resolver);
    assert!(matches!(result, SatisfactionResult::Unsatisfiable(_, _, _)));
}