otter_sat 0.1.0

A library for determining the satisfiability of boolean formulas written in conjunctive normal form, developed to support investigation into solvers by researchers, developers, or anyone curious.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32

use std::{io::BufReader, path::PathBuf, str::FromStr};

use otter_sat::{config::Config, context::Context};

fn main() {
    let args: Vec<String> = std::env::args().collect();
    for arg in &args {
        println!("{arg}");
    }
    let path = match PathBuf::from_str(&args[1]) {
        Ok(path) => path,
        Err(_) => {
            panic!("! Path to CNF required");
        }
    };
    let cnf_file = match std::fs::File::open(path) {
        Ok(path) => path,
        Err(_) => {
            panic!("! Failed to open CNF file");
        }
    };

    let buf_file = BufReader::new(&cnf_file);

    let mut the_context: Context = Context::from_config(Config::default());

    let _ = the_context.read_dimacs(buf_file);

    let result = the_context.solve();

    println!("{result:?}");
}