rustsat_tools/encodings/cnf/
knapsack.rs

1//! # CNF (Multi-Criteria) Knapsack Encoding
2
3use rustsat::{
4    clause,
5    encodings::pb,
6    instances::{fio::dimacs, BasicVarManager, Cnf, ManageVars},
7    types::{constraints::PbConstraint, Lit},
8};
9
10use crate::encodings::knapsack::Knapsack;
11
12enum Clause {
13    /// Clause of the capacity encoding
14    Capacity(<Cnf as IntoIterator>::IntoIter),
15    /// Soft clause for item and objective
16    Soft(usize, usize),
17}
18
19pub struct Encoding {
20    data: Knapsack,
21    next_clause: Clause,
22}
23
24impl Encoding {
25    pub fn new<PBE>(data: Knapsack) -> Self
26    where
27        PBE: pb::BoundUpper + FromIterator<(Lit, usize)>,
28    {
29        let mut vm = BasicVarManager::default();
30        let cap_constr = match PbConstraint::new_ub(
31            data.items
32                .iter()
33                .map(|item| (vm.new_var().pos_lit(), item.weight as isize)),
34            data.capacity as isize,
35        ) {
36            PbConstraint::Ub(constr) => constr,
37            _ => unreachable!(),
38        };
39        let mut cap_cnf = Cnf::new();
40        PBE::encode_ub_constr(cap_constr, &mut cap_cnf, &mut vm).unwrap();
41        Self {
42            data,
43            next_clause: Clause::Capacity(cap_cnf.into_iter()),
44        }
45    }
46}
47
48impl Iterator for Encoding {
49    type Item = dimacs::McnfLine;
50
51    fn next(&mut self) -> Option<Self::Item> {
52        loop {
53            match &mut self.next_clause {
54                Clause::Capacity(iter) => {
55                    let next = iter.next();
56                    if next.is_some() {
57                        return next.map(dimacs::McnfLine::Hard);
58                    }
59                    self.next_clause = Clause::Soft(0, 0);
60                }
61                Clause::Soft(iidx, oidx) => {
62                    let iidx = *iidx;
63                    let oidx = *oidx;
64                    if iidx >= self.data.items.len() {
65                        return None;
66                    }
67                    if oidx >= self.data.items[iidx].values.len() {
68                        self.next_clause = Clause::Soft(iidx + 1, 0);
69                        continue;
70                    }
71                    self.next_clause = Clause::Soft(iidx, oidx + 1);
72                    return Some(dimacs::McnfLine::Soft(
73                        clause![Lit::positive(iidx as u32)],
74                        self.data.items[iidx].values[oidx],
75                        oidx,
76                    ));
77                }
78            }
79        }
80    }
81}
rustsat_tools/encodings/cnf/knapsack.rs

rustsat_tools/encodings/cnf/
knapsack.rs
