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 19, 2024
2 parents 7ea45da + 04db7e0 commit aac7f37
Show file tree
Hide file tree
Showing 27 changed files with 2,746 additions and 198 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.
88 changes: 80 additions & 8 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 All @@ -35,8 +35,6 @@ use std::{
use crate::instances::MultiOptInstance;
#[cfg(feature = "optimization")]
use crate::instances::{Objective, OptInstance};
#[cfg(feature = "optimization")]
use crate::types::WLitIter;

/// Options for reading and writing OPB files
/// Possible relational operators
Expand Down Expand Up @@ -219,8 +217,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 +356,80 @@ fn opb_data(input: &str, opts: Options) -> IResult<&str, OpbData> {
))(input)
}

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

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

/// Writes an OPB file from an interator over [`OpbLine`]s
#[cfg(not(feature = "optimization"))]
pub fn write_opb_lines<W, LI, Iter>(
writer: &mut W,
data: Iter,
opts: Options,
) -> Result<(), io::Error>
where
W: Write,
Iter: Iterator<Item = OpbLine>,
{
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)?,
}
}
Ok(())
}

/// Writes an OPB file from an interator over [`OpbLine`]s
#[cfg(feature = "optimization")]
pub fn write_opb_lines<W, LI, Iter>(
writer: &mut W,
data: Iter,
opts: Options,
) -> Result<(), io::Error>
where
W: Write,
LI: crate::types::WLitIter,
Iter: Iterator<Item = OpbLine<LI>>,
{
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 Expand Up @@ -423,7 +495,7 @@ pub fn write_opt<W, VM, LI>(
) -> Result<(), io::Error>
where
W: Write,
LI: WLitIter,
LI: crate::types::WLitIter,
VM: ManageVars,
{
let cnf = &constrs.cnf;
Expand Down Expand Up @@ -474,7 +546,7 @@ where
W: Write,
VM: ManageVars,
Iter: Iterator<Item = (LI, isize)>,
LI: WLitIter,
LI: crate::types::WLitIter,
{
let cnf = &constrs.cnf;
let cards = &constrs.cards;
Expand Down Expand Up @@ -733,7 +805,7 @@ fn write_pb<W: Write>(writer: &mut W, pb: &PbConstraint, opts: Options) -> Resul
/// # Errors
///
/// If writing fails, returns [`io::Error`].
fn write_objective<W: Write, LI: WLitIter>(
fn write_objective<W: Write, LI: crate::types::WLitIter>(
writer: &mut W,
softs: (LI, isize),
opts: Options,
Expand Down
Loading

0 comments on commit aac7f37

Please sign in to comment.