exec_sat/
lib.rs

1// lib.rs - library to execute and/or parse SAT solver output.
2//
3// exec-sat - Execute SAT Solver and/or parse SAT solver output.
4// Copyright (C) 2022  Mateusz Szpakowski
5//
6// This library is free software; you can redistribute it and/or
7// modify it under the terms of the GNU Lesser General Public
8// License as published by the Free Software Foundation; either
9// version 2.1 of the License, or (at your option) any later version.
10//
11// This library is distributed in the hope that it will be useful,
12// but WITHOUT ANY WARRANTY; without even the implied warranty of
13// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
14// Lesser General Public License for more details.
15//
16// You should have received a copy of the GNU Lesser General Public
17// License along with this library; if not, write to the Free Software
18// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
19
20#![cfg_attr(docsrs, feature(doc_cfg))]
21//! The library to execute SAT solver.
22//!
23//! This library provides routines to parse SAT solver output and to execute SAT solver.
24//! It contains three functions:
25//! * `parse_sat_output` - to parse output from SAT solver after solving instance,
26//! * `exec_sat_simple` - to execute SAT solver program without arguments.
27//! * `exec_sat` - to execute SAT solver program with arguments.
28
29use std::ffi::OsStr;
30use std::io::{self, BufRead, BufReader, Read};
31use std::num::ParseIntError;
32use std::panic;
33use std::process::{Command, Stdio};
34use std::str::FromStr;
35use std::thread;
36
37/// Error type.
38#[derive(thiserror::Error, Debug)]
39pub enum Error {
40    /// Duplicated result.
41    #[error("Too many results")]
42    TooManyResults,
43    /// If some variable has been assigned more than once.
44    #[error("Variable has been assigned more than once")]
45    AssignedMoreThanOnce,
46    /// If not all variables has been assigned.
47    #[error("Not all variables has been assigned")]
48    NotAllAreAssigned,
49    /// Parse error for integers.
50    #[error("Parse error: {0}")]
51    ParseError(#[from] ParseIntError),
52    /// I/O error.
53    #[error("IO error: {0}")]
54    IOError(#[from] io::Error),
55    /// No input available.
56    #[error("No input available from solver")]
57    NoInputAvailable,
58}
59
60/// Sat solver output.
61#[derive(Debug, Clone, PartialEq, Eq)]
62pub enum SatOutput {
63    /// Unknown satisfiability.
64    Unknown,
65    /// Instance is unsatisfiable.
66    Unsatisfiable,
67    /// Instance is satisfiable. Possible assignment given as vector boolean values.
68    /// Index in this vector is literal value. Just `v[2]` gets value of second variable.
69    Satisfiable(Option<Vec<bool>>),
70}
71
72/// Try to parse SAT solver output. It ignores any lines that are not result or
73/// variable assignment.
74pub fn parse_sat_output(r: impl BufRead) -> Result<SatOutput, Error> {
75    let mut assignments = vec![];
76    let mut satisfiable = false;
77    let mut have_result = false;
78    let mut have_assignments = vec![];
79    for line in r.lines() {
80        match line {
81            Ok(line) => match line.chars().next() {
82                Some('s') => {
83                    if have_result {
84                        return Err(Error::TooManyResults);
85                    }
86                    let trimmed = line[1..].trim_start();
87                    if trimmed.starts_with("UNSAT") {
88                        return Ok(SatOutput::Unsatisfiable);
89                    } else if trimmed.starts_with("SAT") {
90                        satisfiable = true;
91                    }
92                    have_result = true;
93                }
94                Some('v') => {
95                    let line = &line[1..];
96                    line.split_whitespace().try_for_each(|x| {
97                        let lit = isize::from_str(x)?;
98                        let varlit = lit.checked_abs().unwrap() as usize;
99                        if varlit != 0 {
100                            let req_size = varlit.checked_add(1).unwrap();
101                            // resize to required size.
102                            if assignments.len() <= req_size {
103                                assignments.resize(req_size, false);
104                                have_assignments.resize(req_size, false);
105                            }
106                            // check if variables already assigned
107                            if have_assignments[varlit] {
108                                return Err(Error::AssignedMoreThanOnce);
109                            }
110                            assignments[varlit] = lit > 0;
111                            have_assignments[varlit] = true;
112                        }
113                        Ok::<(), Error>(())
114                    })?;
115                }
116                _ => {}
117            },
118            Err(err) => {
119                return Err(err.into());
120            }
121        }
122    }
123    if satisfiable {
124        if have_assignments.iter().skip(1).all(|x| *x) {
125            // all variables assigned - ok
126            if !assignments.is_empty() {
127                Ok(SatOutput::Satisfiable(Some(assignments)))
128            } else {
129                Ok(SatOutput::Satisfiable(None))
130            }
131        } else {
132            Err(Error::NotAllAreAssigned)
133        }
134    } else {
135        Ok(SatOutput::Unknown)
136    }
137}
138
139/// Try to execute SAT solver. The input argument should be formulae in CNF format.
140pub fn exec_sat_simple<S, R>(program: S, input: R) -> Result<SatOutput, Error>
141where
142    S: AsRef<OsStr>,
143    R: Read,
144{
145    exec_sat::<_, &str, _, _>(program, [], input)
146}
147
148/// Try to execute SAT solver. The input argument should be formulae in CNF format.
149pub fn exec_sat<S, S2, I, R>(program: S, args: I, mut input: R) -> Result<SatOutput, Error>
150where
151    S: AsRef<OsStr>,
152    S2: AsRef<OsStr>,
153    I: IntoIterator<Item = S2>,
154    R: Read,
155{
156    let mut child = Command::new(program)
157        .args(args)
158        .stdin(Stdio::piped())
159        .stdout(Stdio::piped())
160        .stderr(Stdio::null())
161        .spawn()?;
162    let join = {
163        let mut stdin = child.stdin.take().ok_or(Error::NoInputAvailable)?;
164        let join = thread::spawn(move || child.wait_with_output());
165
166        io::copy(&mut input, &mut stdin)?;
167        join
168    };
169
170    // handle join
171    let output = match join.join() {
172        Ok(t) => t,
173        Err(err) => panic::resume_unwind(err),
174    }?;
175
176    let exp_satisfiable = if let Some(exit_code) = output.status.code() {
177        match exit_code {
178            10 => SatOutput::Satisfiable(None),
179            20 => SatOutput::Unsatisfiable,
180            _ => SatOutput::Unknown,
181        }
182    } else {
183        SatOutput::Unknown
184    };
185
186    if !output.stdout.is_empty() {
187        let sat_out = parse_sat_output(BufReader::new(output.stdout.as_slice()))?;
188        if let SatOutput::Unknown = sat_out {
189            // if satisfiability is unknown from stdout output
190            Ok(exp_satisfiable)
191        } else {
192            Ok(sat_out)
193        }
194    } else {
195        Ok(exp_satisfiable)
196    }
197}
198
199#[cfg(test)]
200mod tests {
201    use super::*;
202
203    #[test]
204    fn test_parse_sat_output() {
205        let example = r#"c blabla
206c bumbum
207s SATISFIABLE
208v -2 1 3 -5 4 0
209c This is end
210"#;
211        assert_eq!(
212            Ok(SatOutput::Satisfiable(Some(vec![
213                false, true, false, true, true, false
214            ]))),
215            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
216        );
217
218        let example = r#"c blabla
219c bumbum
220s SATISFIABLE
221v -2 1 3 -5 0
222c This is end
223"#;
224        assert_eq!(
225            Err("Not all variables has been assigned".to_string()),
226            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
227        );
228
229        let example = r#"c blabla
230c bumbum
231s SATISFIABLE
232v -2 1 3 4 -5 -4 0
233c This is end
234"#;
235        assert_eq!(
236            Err("Variable has been assigned more than once".to_string()),
237            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
238        );
239
240        let example = r#"c blabla
241c bumbum
242s SATISFIABLE
243c This is end
244"#;
245        assert_eq!(
246            Ok(SatOutput::Satisfiable(None)),
247            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
248        );
249
250        let example = r#"c blabla
251c bumbum
252sSATISFIABLE
253v -2 1 3 -5 4 0
254c This is end
255"#;
256        assert_eq!(
257            Ok(SatOutput::Satisfiable(Some(vec![
258                false, true, false, true, true, false
259            ]))),
260            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
261        );
262
263        let example = r#"c blabla
264c bumbam
265s SATISFIABLE
266v -2 1 3
267v -5 4 0
268c This is end
269"#;
270        assert_eq!(
271            Ok(SatOutput::Satisfiable(Some(vec![
272                false, true, false, true, true, false
273            ]))),
274            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
275        );
276
277        let example = r#"c blabla
278c bumbam
279s SATISFIABLE
280v-2  
281v3
282v-5   4 1 0
283c This is end
284"#;
285        assert_eq!(
286            Ok(SatOutput::Satisfiable(Some(vec![
287                false, true, false, true, true, false
288            ]))),
289            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
290        );
291
292        let example = r#"c blablaxx
293c bumbumxxx
294s SATISFIABLE
295o my god
296v -2 1 3
297xxx
298v -5 4 0
299c This is end
300"#;
301        assert_eq!(
302            Ok(SatOutput::Satisfiable(Some(vec![
303                false, true, false, true, true, false
304            ]))),
305            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
306        );
307
308        let example = r#"c blabla
309c bumbum
310s UNSATISFIABLE
311c This is end
312"#;
313        assert_eq!(
314            Ok(SatOutput::Unsatisfiable),
315            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
316        );
317
318        let example = r#"c blabla
319c bumbum
320s SATISFIABLE
321s UNSATISFIABLE
322c This is end
323"#;
324        assert_eq!(
325            Err("Too many results".to_string()),
326            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
327        );
328
329        let example = r#"c blabla
330c bumbum
331sUNSATISFIABLE
332c This is end
333"#;
334        assert_eq!(
335            Ok(SatOutput::Unsatisfiable),
336            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
337        );
338
339        let example = r#"c blabla
340c bumbum
341c This is end
342"#;
343        assert_eq!(
344            Ok(SatOutput::Unknown),
345            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
346        );
347
348        let example = r#"c blabla
349c bumbum
350v -1 -3 4 2
351c This is end
352"#;
353        assert_eq!(
354            Ok(SatOutput::Unknown),
355            parse_sat_output(BufReader::new(example.as_bytes())).map_err(|e| e.to_string())
356        );
357    }
358}
exec_sat/lib.rs

exec_sat/
lib.rs
