check_solution/
check-solution.rs

1//! # `check-solution`
2//!
3//! A small tool for checking solutions to SAT and optimization instances.
4
5use std::{io, path::PathBuf};
6
7use clap::{Parser, ValueEnum};
8use rustsat::{
9    instances::{
10        fio::{self, opb::Options as OpbOptions},
11        MultiOptInstance, OptInstance, SatInstance,
12    },
13    types::Assignment,
14};
15
16#[derive(Copy, Clone, PartialEq, Eq, ValueEnum)]
17pub enum FileFormat {
18    /// Infer the file format from the file extension according to the following rules:
19    /// - `.cnf`: DIMACS CNF file
20    /// - `.wcnf`: Weighted DIMACS CNF (MaxSAT) file
21    /// - `.mcnf`: Multi-objective MaxSAT file
22    /// - `.opb`: OPB file (without an objective)
23    /// - `.mopb` / `.pbmo`: Multi-objective OPB file
24    ///
25    /// All file extensions can also be appended with `.bz2`, `.xz`, or `.gz` if compression is used.
26    Infer,
27    /// A DIMACS CNF file
28    Cnf,
29    /// A DIMACS WCNF file
30    Wcnf,
31    /// A DIMACS MCNF file
32    Mcnf,
33    /// An OPB file with zero or more objectives
34    Opb,
35}
36
37#[derive(Parser)]
38#[command(author, version, about, long_about = None)]
39struct Args {
40    /// The instance to check the solution against
41    instance: PathBuf,
42    /// The solution specified as one or multiple v-lines. If not specified, will be read from
43    /// `stdin`.
44    solution: Option<PathBuf>,
45    /// The file format of the instance. With infer, the file format is
46    /// inferred from the file extension.
47    #[arg(long, value_enum, default_value_t = FileFormat::Infer)]
48    file_format: FileFormat,
49    /// The index in the OPB file to treat as the lowest variable
50    #[arg(long, default_value_t = 1)]
51    opb_first_var_idx: u32,
52}
53
54fn main() -> anyhow::Result<()> {
55    let args = Args::parse();
56    let opb_opts = OpbOptions {
57        first_var_idx: args.opb_first_var_idx,
58        ..OpbOptions::default()
59    };
60    let (constrs, objs) = parse_instance(args.instance, args.file_format, opb_opts)?.decompose();
61
62    let mut reader = if let Some(solution) = args.solution {
63        fio::open_compressed_uncompressed_read(solution)?
64    } else {
65        Box::new(io::BufReader::new(io::stdin()))
66    };
67
68    let mut sol = Assignment::default();
69    loop {
70        let mut buf = String::new();
71        let read = reader.read_line(&mut buf)?;
72        if read == 0 {
73            break;
74        }
75        if buf.starts_with('v') {
76            sol.extend_from_vline(&buf)?;
77        }
78    }
79
80    if let Some(constr) = constrs.unsat_constraint(&sol) {
81        println!("unsatisfied constraint: {constr}");
82        std::process::exit(1);
83    }
84    print!("objective values: ");
85    for i in 0..objs.len() {
86        if i < objs.len() - 1 {
87            print!("{}, ", objs[i].evaluate(&sol))
88        } else {
89            print!("{}", objs[i].evaluate(&sol));
90        }
91    }
92    println!();
93    Ok(())
94}
95
96macro_rules! is_one_of {
97    ($a:expr, $($b:expr),*) => {
98        $( $a == $b || )* false
99    }
100}
101
102fn parse_instance(
103    inst_path: PathBuf,
104    file_format: FileFormat,
105    opb_opts: fio::opb::Options,
106) -> anyhow::Result<MultiOptInstance> {
107    match file_format {
108        FileFormat::Infer => {
109            if let Some(ext) = inst_path.extension() {
110                let path_without_compr = inst_path.with_extension("");
111                let ext = if is_one_of!(ext, "gz", "bz2", "xz") {
112                    // Strip compression extension
113                    match path_without_compr.extension() {
114                        Some(ext) => ext,
115                        None => anyhow::bail!("no file extension after compression extension"),
116                    }
117                } else {
118                    ext
119                };
120                let inst = if is_one_of!(ext, "cnf", "dimacs") {
121                    let inst = SatInstance::from_dimacs_path(inst_path)?;
122                    MultiOptInstance::compose(inst, vec![])
123                } else if is_one_of!(ext, "wcnf") {
124                    let (inst, obj) = OptInstance::from_dimacs_path(inst_path)?.decompose();
125                    MultiOptInstance::compose(inst, vec![obj])
126                } else if is_one_of!(ext, "mcnf") {
127                    MultiOptInstance::from_dimacs_path(inst_path)?
128                } else if is_one_of!(ext, "opb", "mopb", "pbmo") {
129                    MultiOptInstance::from_opb_path(inst_path, opb_opts)?
130                } else {
131                    anyhow::bail!("unknown file extension")
132                };
133                Ok(inst)
134            } else {
135                anyhow::bail!("no file extension")
136            }
137        }
138        FileFormat::Cnf => {
139            let inst = SatInstance::from_dimacs_path(inst_path)?;
140            Ok(MultiOptInstance::compose(inst, vec![]))
141        }
142        FileFormat::Wcnf => {
143            let (inst, obj) = OptInstance::from_dimacs_path(inst_path)?.decompose();
144            Ok(MultiOptInstance::compose(inst, vec![obj]))
145        }
146        FileFormat::Mcnf => MultiOptInstance::from_dimacs_path(inst_path),
147        FileFormat::Opb => MultiOptInstance::from_opb_path(inst_path, opb_opts),
148    }
149}
check_solution/check-solution.rs

check_solution/
check-solution.rs
