Skip to content

Commit

Permalink
Merge branch 'feat/moo-pb-encodings' into next-major
Browse files Browse the repository at this point in the history
  • Loading branch information
chrjabs committed Aug 15, 2024
2 parents 7ea45da + 04db7e0 commit e85754e
Show file tree
Hide file tree
Showing 27 changed files with 2,705 additions and 161 deletions.
20 changes: 20 additions & 0 deletions data/AP_p-3_n-5_ins-1.dat
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
3
5
[[[6, 1, 20, 2, 3],
[2, 6, 9, 10, 18],
[1, 6, 20, 5, 9],
[6, 8, 6, 9, 6],
[7, 10, 10, 6, 2]]
,
[[17, 20, 8, 8, 20],
[10, 13, 1, 10, 15],
[4, 11, 1, 13, 1],
[19, 13, 7, 18, 17],
[15, 3, 5, 1, 11]]
,
[[10, 7, 1, 19, 12],
[2, 15, 12, 10, 3],
[11, 20, 16, 12, 9],
[10, 15, 20, 11, 7],
[1, 9, 20, 7, 6]]
]
168 changes: 168 additions & 0 deletions data/F5050W01.dat
Original file line number Diff line number Diff line change
@@ -0,0 +1,168 @@
# Problem F5050W01 : N=50/P=2/K=1

# N
50

# P
2

# K
1

# Objectif 1
112
14
156
175
82
221
44
94
292
223
274
61
246
279
104
179
234
289
86
41
78
159
112
223
112
149
158
207
68
197
41
289
29
170
263
164
197
162
149
100
191
100
257
257
102
75
260
23
220
89

# Objectif 2
86
129
32
230
165
260
83
138
236
95
178
105
158
245
244
99
288
149
85
14
39
64
129
185
18
239
287
15
44
241
41
293
73
17
17
81
158
13
228
203
8
107
138
185
140
282
96
43
292
115

# Contrainte 1
280
235
278
37
214
155
216
69
261
202
245
132
82
1
102
253
200
242
289
178
91
200
115
168
65
157
74
225
138
211
88
115
26
44
227
4
69
206
289
254
247
20
121
125
77
62
103
123
199
268

3904
7 changes: 7 additions & 0 deletions data/KP_p-3_n-10_ins-1.dat
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
3
10
2137
[[566, 611, 506, 180, 817, 184, 585, 423, 26, 317],
[62, 84, 977, 979, 874, 54, 269, 93, 881, 563],
[664, 982, 962, 140, 224, 215, 12, 869, 332, 537]]
[557, 898, 148, 63, 78, 964, 246, 662, 386, 272]
24 changes: 24 additions & 0 deletions data/didactic1.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
8
5

7 20 21 53 34
74 71 88 51 35
69 88 87 40 57
86 64 79 81 59
76 67 47 25 76
8 14 76 82 77
69 58 16 75 40
96 24 38 96 13

33 99 45 81 71
66 11 10 90 97
70 15 87 12 10
73 66 89 91 12
2 93 48 90 68
44 22 50 98 45
35 51 6 47 5
55 37 73 37 74

99 27 54 11 29

52 6 21 98 6
Empty file modified data/minisat-segfault.cnf
100755 → 100644
Empty file.
39 changes: 36 additions & 3 deletions src/instances/fio/opb.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ use crate::{
instances::{ManageVars, SatInstance},
types::{
constraints::{CardConstraint, PbConstraint},
Cl, Lit, Var,
Cl, Clause, Lit, Var,
},
};
use anyhow::Context;
Expand Down Expand Up @@ -219,8 +219,8 @@ fn variable(input: &str, opts: Options) -> IResult<&str, Var> {
/// Parses a literal. The spec for linear OPB instances only allows for
/// variables but we allow negated literals with '~' as in non-linear OPB
/// instances.
fn literal(input: &str, opts: Options) -> IResult<&str, Lit> {
match tag::<_, _, NomError<_>>("~")(input) {
pub(crate) fn literal(input: &str, opts: Options) -> IResult<&str, Lit> {
match alt::<_, _, NomError<_>, _>((tag("~"), tag("-")))(input) {
Ok((input, _)) => map_res(|i| variable(i, opts), |v| Ok::<_, ()>(v.neg_lit()))(input),
Err(_) => map_res(|i| variable(i, opts), |v| Ok::<_, ()>(v.pos_lit()))(input),
}
Expand Down Expand Up @@ -358,6 +358,39 @@ fn opb_data(input: &str, opts: Options) -> IResult<&str, OpbData> {
))(input)
}

/// Possible lines that can be written to OPB
pub enum OpbLine<LI: WLitIter> {
/// A comment line
Comment(String),
/// A clausal constraint line
Clause(Clause),
/// A cardinality constraint line
Card(CardConstraint),
/// A PB constraint line
Pb(PbConstraint),
#[cfg(feature = "optimization")]
/// An objective line
Objective(LI),
}

/// Writes an OPB file from an interator over [`OpbLine`]s
pub fn write_opb_lines<W: Write, LI: WLitIter, Iter: Iterator<Item = OpbLine<LI>>>(
writer: &mut W,
data: Iter,
opts: Options,
) -> Result<(), io::Error> {
for dat in data {
match dat {
OpbLine::Comment(c) => writeln!(writer, "* {c}")?,
OpbLine::Clause(cl) => write_clause(writer, &cl, opts)?,
OpbLine::Card(card) => write_card(writer, &card, opts)?,
OpbLine::Pb(pb) => write_pb(writer, &pb, opts)?,
OpbLine::Objective(obj) => write_objective(writer, (obj, 0), opts)?,
}
}
Ok(())
}

/// Writes a [`SatInstance`] to an OPB file
///
/// # Errors
Expand Down
31 changes: 30 additions & 1 deletion src/instances/multiopt.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
//! # Multi-Objective Optimization Instance Representations
use std::{io, path::Path};
use std::{collections::BTreeSet, io, path::Path};

use crate::{
encodings::{card, pb},
Expand Down Expand Up @@ -243,6 +243,35 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
MultiOptInstance { constrs, objs }
}

fn extend_var_set(&self, varset: &mut BTreeSet<Var>) {
self.constrs.extend_var_set(varset);
for o in &self.objs {
o.var_set(varset);
}
}

/// Gets the set of variables in the instance
pub fn var_set(&self) -> BTreeSet<Var> {
let mut varset = BTreeSet::new();
self.extend_var_set(&mut varset);
varset
}

/// Reindex all variables in the instance in order
///
/// If the reindexing variable manager produces new free variables in order, this results in
/// the variable _order_ being preserved with gaps in the variable space being closed
#[must_use]
pub fn reindex_ordered<R: ReindexVars>(self, mut reindexer: R) -> MultiOptInstance<R> {
let mut varset = BTreeSet::new();
self.extend_var_set(&mut varset);
// reindex variables in order to ensure ordered reindexing
for var in varset {
reindexer.reindex(var);
}
self.reindex(reindexer)
}

#[cfg(feature = "rand")]
/// Randomly shuffles the order of constraints and the objective
#[must_use]
Expand Down
Loading

0 comments on commit e85754e

Please sign in to comment.