sddrs/manager/
dimacs.rs

1//! DIMACS module responsible for parsing DIMACS CNF problem files.
2use crate::literal::{Polarity, VariableIdx};
3use crate::manager::SddManager;
4use crate::sdd::SddRef;
5
6use anyhow::{bail, Result};
7
8/// Preamble of the DIMACS file.
9#[derive(Debug, PartialEq, Eq)]
10pub struct Preamble {
11    pub clauses: usize,
12    pub variables: usize,
13}
14
15/// Single clause -- disjunction of literals.
16#[derive(Debug, PartialEq, Eq)]
17pub(crate) struct Clause {
18    pub(crate) var_label_polarities: Vec<Polarity>,
19    pub(crate) var_label_indices: Vec<u32>,
20}
21
22impl Clause {
23    #[must_use]
24    pub(crate) fn to_sdd(&self, manager: &SddManager) -> SddRef {
25        let mut sdd = manager.contradiction();
26
27        for (idx, polarity) in self
28            .var_label_indices
29            .iter()
30            .zip(self.var_label_polarities.iter())
31        {
32            // DIMACS variables are indexed from 1 but our variables start at 0.
33            let lit = manager.literal_from_idx(VariableIdx(idx - 1), *polarity);
34            sdd = manager.disjoin(&sdd, &lit);
35        }
36
37        sdd
38    }
39}
40
41/// Current state of the DIMACS reader.
42#[derive(PartialEq, Eq)]
43enum DimacsParserState {
44    Initialized,
45    PreambleParsed,
46    ParsingClauses,
47    Finished,
48}
49
50/// DIMACS parser.
51#[allow(clippy::module_name_repetitions)]
52pub struct DimacsParser<'a> {
53    reader: &'a mut dyn std::io::BufRead,
54    state: DimacsParserState,
55}
56
57impl<'a> DimacsParser<'a> {
58    #[must_use]
59    pub fn new(reader: &'a mut dyn std::io::BufRead) -> Self {
60        DimacsParser {
61            state: DimacsParserState::Initialized,
62            reader,
63        }
64    }
65
66    /// Parse preamble of the DIMACS file.
67    ///
68    /// # Errors
69    ///
70    /// Returns an error if:
71    /// * the preamble has already been parsed,
72    /// * the preamble is missing a 'problem line',
73    /// * could not skip over comments in the preamble
74    /// * could not parse a 'problem line'
75    pub fn parse_preamble(&mut self) -> Result<Preamble> {
76        if self.state != DimacsParserState::Initialized {
77            bail!("preamble already parsed");
78        }
79
80        // Consume comments and advance to the problem line.
81        while match peek_line(self.reader).get(0..1) {
82            None => bail!("preamble is missing a problem line"),
83            Some(first_char) => first_char == "c",
84        } {
85            let mut buf = String::new();
86            match self.reader.read_line(&mut buf) {
87                Ok(..) => {}
88                Err(err) => bail!("could not parse preamble comment: {err}"),
89            }
90        }
91
92        let mut problem = String::new();
93        match self.reader.read_line(&mut problem) {
94            Ok(..) => self.parse_problem_line(problem.trim()),
95            Err(err) => bail!("could not parse problem line: {err}"),
96        }
97    }
98
99    /// Parse the next clause.
100    pub(crate) fn parse_next_clause(&mut self) -> Result<Option<Clause>> {
101        assert!(self.state != DimacsParserState::Initialized);
102
103        if self.state == DimacsParserState::Finished {
104            return Ok(None);
105        }
106
107        let mut clause = String::new();
108        match self.reader.read_line(&mut clause) {
109            Ok(read) => {
110                if read == 0 {
111                    self.state = DimacsParserState::Finished;
112                    Ok(None)
113                } else {
114                    self.state = DimacsParserState::ParsingClauses;
115                    let clause = clause.trim().to_owned();
116                    if clause == "%" {
117                        let mut zero = String::new();
118                        let _ = self.reader.read_line(&mut zero);
119                        if zero.trim() == "0" {
120                            return Ok(None);
121                        }
122                        bail!("expected '0' after '%' but found '{zero}' instead");
123                    }
124
125                    DimacsParser::parse_clause_line(&clause)
126                }
127            }
128            Err(err) => bail!("could not parse clause: {err}"),
129        }
130    }
131
132    fn parse_problem_line(&mut self, line: &str) -> Result<Preamble> {
133        let items: Vec<_> = line
134            .split(' ')
135            .filter(|element| !element.trim().is_empty())
136            .collect();
137        if items.len() != 4 {
138            bail!("problem line must contain exactly 4 fields: 'p cnf VARIABLES CLAUSES'");
139        }
140
141        if *items.first().unwrap() != "p" {
142            bail!("first field of problem line must be 'p'");
143        }
144
145        if *items.get(1).unwrap() != "cnf" {
146            bail!("second field of problem line must be 'cnf'");
147        }
148
149        let variables = match items.get(2).unwrap().parse::<usize>() {
150            Ok(variables) => variables,
151            Err(err) => bail!("could not parse number of variables: {err}"),
152        };
153
154        let clauses = match items.get(3).unwrap().parse::<usize>() {
155            Ok(variables) => variables,
156            Err(err) => bail!("could not parse number of clauses: {err}"),
157        };
158
159        self.state = DimacsParserState::PreambleParsed;
160        Ok(Preamble { clauses, variables })
161    }
162
163    fn parse_clause_line(line: &str) -> Result<Option<Clause>> {
164        let tokens: Vec<_> = line
165            .split(' ')
166            .filter(|token| *token != "0" && token.trim() != "")
167            .collect();
168
169        let literals: Vec<_> = tokens
170            .iter()
171            .map(|variable_idx| match variable_idx.trim().parse::<i32>() {
172                Err(err) => bail!("literal '{variable_idx}' is invalid: {err}"),
173                Ok(idx) => Ok((Polarity::from(!variable_idx.starts_with('-')), idx)),
174            })
175            .collect();
176
177        // We must have parsed a line that had only a '0'.
178        if literals.is_empty() {
179            return Ok(None);
180        }
181
182        let mut clause = Clause {
183            var_label_indices: Vec::new(),
184            var_label_polarities: Vec::new(),
185        };
186
187        for literal in &literals {
188            match literal {
189                Ok((polarity, idx)) => {
190                    clause.var_label_indices.push(idx.unsigned_abs());
191                    clause.var_label_polarities.push(*polarity);
192                }
193                Err(err) => bail!("could not parse clause: {err}"),
194            }
195        }
196
197        Ok(Some(clause))
198    }
199}
200
201#[must_use]
202fn peek_line(reader: &mut dyn std::io::BufRead) -> &str {
203    std::str::from_utf8(reader.fill_buf().unwrap()).unwrap()
204}
205
206#[cfg(test)]
207mod test {
208    use pretty_assertions::assert_eq;
209
210    use std::io::BufReader;
211
212    use super::{DimacsParser, Preamble};
213    use crate::{literal::Polarity, manager::dimacs::Clause};
214
215    fn collect_clauses(dimacs: &mut DimacsParser) -> Vec<Clause> {
216        let mut clauses = Vec::new();
217
218        loop {
219            match dimacs.parse_next_clause() {
220                Ok(Some(clause)) => clauses.push(clause),
221                Ok(None) => break,
222                Err(err) => panic!("{err}"),
223            }
224        }
225
226        clauses
227    }
228
229    #[test]
230    fn dimacs_ok() {
231        let contents = "c Example CNF format file
232c
233p cnf 4 3
2341 3 -4 0
2354 0
2362 -3 0";
237        let mut reader = BufReader::new(contents.as_bytes());
238        let mut dimacs = DimacsParser::new(&mut reader);
239
240        assert_eq!(
241            dimacs.parse_preamble().unwrap(),
242            Preamble {
243                variables: 4,
244                clauses: 3
245            }
246        );
247
248        let clauses = collect_clauses(&mut dimacs);
249
250        assert_eq!(
251            clauses,
252            vec![
253                Clause {
254                    var_label_indices: vec![1, 3, 4],
255                    var_label_polarities: vec![
256                        Polarity::Positive,
257                        Polarity::Positive,
258                        Polarity::Negative
259                    ],
260                },
261                Clause {
262                    var_label_indices: vec![4],
263                    var_label_polarities: vec![Polarity::Positive,],
264                },
265                Clause {
266                    var_label_indices: vec![2, 3],
267                    var_label_polarities: vec![Polarity::Positive, Polarity::Negative],
268                },
269            ]
270        );
271    }
272
273    #[test]
274    fn preamble_with_whitespace() {
275        let contents = "c Example CNF format file
276c
277p   cnf  4   3
2781 3 -4 0
2794 0 2
280-3 0";
281        let mut reader = BufReader::new(contents.as_bytes());
282        let mut dimacs = DimacsParser::new(&mut reader);
283
284        assert_eq!(
285            dimacs.parse_preamble().unwrap(),
286            Preamble {
287                variables: 4,
288                clauses: 3
289            }
290        );
291    }
292
293    #[test]
294    fn clauses_with_whitespace() {
295        let contents = "c Example CNF format file
296c
297p cnf 4 2
2981  3  -4 0
299  4 0
300";
301        let mut reader = BufReader::new(contents.as_bytes());
302        let mut dimacs = DimacsParser::new(&mut reader);
303
304        assert_eq!(
305            dimacs.parse_preamble().unwrap(),
306            Preamble {
307                variables: 4,
308                clauses: 2
309            }
310        );
311    }
312
313    #[test]
314    fn trailing_eof_syntax() {
315        // This weird format with trailing '%\n0\n' is in the SATLIB benchmarks: https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html
316        let contents = "c Example CNF format file
317c
318p cnf 4 2
3191 3 -4 0
3204 0
321%
3220
323";
324        let mut reader = BufReader::new(contents.as_bytes());
325        let mut dimacs = DimacsParser::new(&mut reader);
326
327        assert_eq!(
328            dimacs.parse_preamble().unwrap(),
329            Preamble {
330                variables: 4,
331                clauses: 2
332            }
333        );
334
335        let clauses = collect_clauses(&mut dimacs);
336
337        assert_eq!(
338            clauses,
339            vec![
340                Clause {
341                    var_label_indices: vec![1, 3, 4],
342                    var_label_polarities: vec![
343                        Polarity::Positive,
344                        Polarity::Positive,
345                        Polarity::Negative
346                    ],
347                },
348                Clause {
349                    var_label_indices: vec![4],
350                    var_label_polarities: vec![Polarity::Positive],
351                },
352            ]
353        );
354    }
355
356    #[test]
357    fn trailing_zeros() {
358        let contents = "c Example CNF format file
359c
360p cnf 4 2
3611 3 -4 0
3624 0
363";
364        let mut reader = BufReader::new(contents.as_bytes());
365        let mut dimacs = DimacsParser::new(&mut reader);
366
367        assert_eq!(
368            dimacs.parse_preamble().unwrap(),
369            Preamble {
370                variables: 4,
371                clauses: 2
372            }
373        );
374
375        let clauses = collect_clauses(&mut dimacs);
376
377        assert_eq!(
378            clauses,
379            vec![
380                Clause {
381                    var_label_indices: vec![1, 3, 4],
382                    var_label_polarities: vec![
383                        Polarity::Positive,
384                        Polarity::Positive,
385                        Polarity::Negative
386                    ],
387                },
388                Clause {
389                    var_label_indices: vec![4],
390                    var_label_polarities: vec![Polarity::Positive],
391                },
392            ]
393        );
394    }
395}
sddrs/manager/dimacs.rs

sddrs/manager/
dimacs.rs
