boolean_circuit/file_formats/
dimacs.rs

1use std::{
2    collections::HashMap,
3    io::{BufRead, Read, Write},
4};
5
6use itertools::Itertools;
7
8use crate::Literal;
9
10/// Writes the given CNF into a writer in DIMACS format and returns
11/// a mapping from variable IDs to their names.
12pub fn to_dimacs(mut w: impl Write, cnf: &[Vec<Literal>]) -> HashMap<u32, String> {
13    let var_map = var_mapping(cnf);
14    writeln!(w, "p cnf {} {}", var_map.len(), cnf.len()).unwrap();
15
16    for clause in cnf {
17        for literal in clause {
18            if literal.is_negated() {
19                write!(w, "-").unwrap();
20            }
21            write!(w, "{} ", var_map[literal.var()]).unwrap();
22        }
23        writeln!(w, "0").unwrap();
24    }
25    // Invert the mapping
26    var_map
27        .into_iter()
28        .map(|(name, id)| (id, name.to_string()))
29        .collect()
30}
31
32fn var_mapping(cnf: &[Vec<Literal>]) -> HashMap<String, u32> {
33    cnf.iter()
34        .flatten()
35        .map(|literal| literal.var())
36        .unique()
37        .enumerate()
38        .map(|(i, var)| (var.to_string(), (i + 1) as u32))
39        .collect()
40}
41
42/// Parses a DIMACS file and returns it in CNF.
43/// Variable names are kept as decimal numbers.
44pub fn from_dimacs(i: impl Read) -> Result<Vec<Vec<Literal>>, String> {
45    let mut reader = std::io::BufReader::new(i);
46    let mut header = Default::default();
47    reader.read_line(&mut header).map_err(|e| e.to_string())?;
48    if !header.starts_with("p cnf") {
49        return Err("Invalid DIMACS header, expected to start with 'p cnf'.".to_string());
50    }
51    // We ignore the number of clauses and variables, since it is not relevant.
52    reader
53        .lines()
54        .map(|line| {
55            let line = line.map_err(|e| e.to_string())?;
56            let mut items = line.split_whitespace();
57            if items.next_back() != Some("0") {
58                return Err("Invalid DIMACS clause, expected to end with '0'.".to_string());
59            }
60            items
61                .map(|item| {
62                    if item == "0" {
63                        Err(format!(
64                            "Invalid DIMACS clause, inner literal {item} not allowed."
65                        ))
66                    } else if let Some(name) = item.strip_prefix('-') {
67                        Ok(!Literal::from(name))
68                    } else {
69                        Ok(Literal::from(item))
70                    }
71                })
72                .collect::<Result<Vec<_>, String>>()
73        })
74        .collect::<Result<Vec<_>, String>>()
75}
76
77#[cfg(test)]
78mod test {
79    use super::*;
80
81    #[test]
82    fn test_var_mapping() {
83        let cnf = vec![vec!["a".into(), "b".into(), !Literal::from("a")]];
84        let var_map = var_mapping(&cnf);
85        assert_eq!(var_map.len(), 2);
86        assert_eq!(var_map["a"], 1);
87        assert_eq!(var_map["b"], 2);
88    }
89
90    #[test]
91    fn test_to_dimacs() {
92        let x: Literal = "x".into();
93        let y: Literal = "y".into();
94        let z: Literal = "z".into();
95
96        let cnf = vec![
97            vec![x.clone(), y.clone()],
98            vec![!x.clone(), z.clone()],
99            vec![y.clone(), z.clone()],
100            vec![],
101        ];
102        let mut buf = Vec::new();
103        let var_map = to_dimacs(&mut buf, &cnf);
104        let expected = "p cnf 3 4\n1 2 0\n-1 3 0\n2 3 0\n0\n";
105        assert_eq!(String::from_utf8(buf).unwrap(), expected);
106        assert_eq!(var_map.len(), 3);
107        assert_eq!(var_map[&1], "x");
108        assert_eq!(var_map[&2], "y");
109        assert_eq!(var_map[&3], "z");
110    }
111
112    #[test]
113    fn test_from_dimacs() {
114        let input = "p cnf 2 4\n1 2 0\n-2 0\n1 0\n0\n";
115        let cnf = from_dimacs(input.as_bytes()).unwrap();
116        assert_eq!(
117            cnf,
118            vec![
119                vec![Literal::from("1"), Literal::from("2")],
120                vec![!Literal::from("2")],
121                vec![Literal::from("1")],
122                vec![],
123            ]
124        );
125        let mut buf = Vec::new();
126        to_dimacs(&mut buf, &cnf);
127        assert_eq!(String::from_utf8(buf).unwrap(), input);
128    }
129}
boolean_circuit/file_formats/dimacs.rs

boolean_circuit/file_formats/
dimacs.rs
