splr as a library about splr HOT 13 CLOSED

I'm sorry but Splr doesn't have any API as a library so far. But I'll add it if you need it.
Probably it will be something like that:

#[cfg(features = "library_without_IO")]
impl Splr {
    ///```
    /// let _ = Splr::new_solver(3, &[&[1,-2,3], &[-1, -2,-3]]).solve();
    ///```
   fn new_solver(num_vars: usize, vec: &[&[u32]]) -> Self;
   /// re-export from some present trait
   fn solve(&mut self) -> Result<Certificate, ...>;
}

Is this ok? I can start coding after the 0.4.0 release, which will be this week.

from splr.

I think that would be excellent! Not as good as an incremental interface (which would allow better algorithms on my side) but I can see why that can cause problems if SPLR is built specifically as a standalone application. Thanks for looking into this. By the way, the interface has to use i32 if negated literals are negative numbers.

from splr.

I've just added TryFrom<Config, &[Vec<i32>]> for Solver on #45, which would be a much better IF for Rust programmers. Here's an example you can check by yourself now.

• Cargo.toml

[dependencies]                                                                                                      
splr = { git = "https://github.com/shnarazk/splr", branch = "20200429-lib-wo-IO", features = ["no_IO"] }            

• main.rs

use splr::{Certificate, Config, SatSolverIF, Solver};
use std::convert::TryFrom;

macro_rules! run {
    ($vec: expr) => {
        println!(
            "{:>46} =| {:?}",
            format!("{:?}", $vec),
            match Solver::try_from((Config::default(), $vec.as_ref())).map(|mut s| s.solve()) {
                Err(e) => e,
                // Ok(Ok(u @ Certificate::UNSAT)) => Ok(u),
                Ok(s) => s,
            }
        );
    };
}

fn main() {
    let mut v: Vec<Vec<i32>> = Vec::new();
    run!(v);
    v.push(Vec::new());
    run!(v);
    run!(vec![vec![1i32]]);
    run!(vec![vec![1i32], vec![-1]]);
    run!(vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]]);
    run!(vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, -2], vec![-2, -3]]);
    run!(vec![vec![1, 2], vec![-1, 3], vec![-1, -3], vec![-1, -2], vec![1, -2]]);
    // generic interface via `AsRef`
    let (v1, v2, v3, v4, v5) = (vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2], vec![-3]);
    run!(vec![&v1, &v2, &v3, &v4, &v5]); // : Vec<&[i32]>
    run!([&v1, &v2, &v3, &v4, &v5]);     // : [&[i32]; 5]
}

• output of 'Cargo run'

                                            [] =| Ok(SAT([]))
                                          [[]] =| Ok(UNSAT)
                                         [[1]] =| Ok(SAT([1]))
                                   [[1], [-1]] =| Ok(UNSAT)
           [[1, 2], [-1, 3], [1, -3], [-1, 2]] =| Ok(SAT([-1, 2, -3]))
[[1, 2], [-1, 3], [1, -3], [-1, -2], [-2, -3]] =| Ok(SAT([1, -2, 3]))
[[1, 2], [-1, 3], [-1, -3], [-1, -2], [1, -2]] =| Ok(UNSAT)
     [[1, 2], [-1, 3], [1, -3], [-1, 2], [-3]] =| Ok(SAT([-1, 2, -3]))
     [[1, 2], [-1, 3], [1, -3], [-1, 2], [-3]] =| Ok(SAT([-1, 2, -3]))

With feature "no_IO", splr doesn't call file IO. But it still depends on 'structopt' and 'libc' crates. Is this acceptable in WASM environment?

And I have no idea about an incremental interface for now, even though minisat-1.14 has. 😄

from splr.

Thanks! I will give it a try.

from splr.

It works, thanks! I have not tried out the no_std part, but I am afraid that libc is not available in a wasm environment. I have a few questions:

• In the new TryFrom implementation you have both CNFDescription::from(vec) and inject_from_vec(vec). Are you adding the same set of clauses twice maybe?
• You have this Err(SolverError::Inconsistent) => Err(Ok(Certificate::UNSAT)) match, but should the inconsistent be reported as Ok(Certificate::UNSAT)? I am a little unclear of the wrapped Ok/Err part. Does Inconsistent mean that a conflict was discovered during adding clauses?
• Using the SatSolverIF I can build a solver and add (unchecked) clauses as well. Could that be used as an alternative interface then? Maybe that works as an incremental solver as well?

from splr.

It works, thanks!

I'm glad to hear.

I have not tried out the no_std part, but I am afraid that libc is not available in a wasm environment.

I see. Then I will try to remove libc dependency as a part of 'no_IO' or a better feature. 'libc' is required only for timeout handling. It isn't essential.

In the new TryFrom implementation you have both CNFDescription::from(vec) and inject_from_vec(vec). Are you adding the same set of clauses twice maybe?

CNFDescription::from consumes a reference to a vec. And CNFDescription doesn't contain CNF itself. They are stored in Solver::cdb once.

You have this Err(SolverError::Inconsistent) => Err(Ok(Certificate::UNSAT)) match, but should the inconsistent be reported as Ok(Certificate::UNSAT)? I am a little unclear of the wrapped Ok/Err part. Does Inconsistent mean that a conflict was discovered during adding clauses?

Yes. Solver::build executes assignments if it finds unit clauses in a given CNF.
So if it is inconsistent, Solver::build returns SolverError::Inconsistent. I like to map this error to Certificate::UNSATintry_from` because it's a higher-level interface for programmers who don't need a solver.

Using the SatSolverIF I can build a solver and add (unchecked) clauses as well. Could that be used as an alternative interface then? Maybe that works as an incremental solver as well?

I tried the following by myself. Is this an implementation you are imaging? Unfortunately, Splr-0.4.0 didn't work as expected.

use splr::{*, types::Lit};
use std::convert::TryFrom;

fn main() {
    let mut solver = Solver::try_from("tests/uf8.cnf").expect("panic");
    solver.state.config.quiet_mode = true;    // Still annoying! I'll revise it.
    loop {
        match solver.solve() {
            Ok(Certificate::SAT(ans)) => {
                println!("s SATISFIABLE: {:?}", ans);
                let mut reject = ans.iter().map(|i| !Lit::from(*i)).collect();
                solver.add_unchecked_clause(&mut reject);
            }
            Ok(Certificate::UNSAT) => {
                println!("s UNSATISFIABLE");
                break;
            }
            Err(e) => panic!("s UNKNOWN; {}", e),
        }
    }
}

Probably we need an interface to add a clause and update submodules appropriately. I'll make a branch. Do you have any opinions?

from splr.

Sorry, I have to update the previous comment. I forgot to check the return value of add_unchecked_clause!

             Ok(Certificate::SAT(ans)) => {
                 println!("s SATISFIABLE: {:?}", ans);
                 let mut reject = ans.iter().map(|i| !Lit::from(*i)).collect();
-                solver.add_unchecked_clause(&mut reject);
+                if solver.add_unchecked_clause(&mut reject).is_none() {
+                    println!("c no answer");
+                    break;
+                }
             }

About 'tests/uf8.cnf', this shows:

s SATISFIABLE: [-1, 2, 3, -4, -5, -6, -7, -8]
c no answer

And here's another instance uf20-01.cnf.

s SATISFIABLE: [ 1, -2, -3, -4, -5,  6, -7, -8,  9, -10, -11, -12, -13, 14, 15, -16, 17, -18, -19, 20]
s SATISFIABLE: [-1,  2,  3,  4, -5, -6, -7,  8,  9,  10,  11, -12, -13, 14, 15, -16, 17,  18,  19, 20]
s SATISFIABLE: [ 1, -2, -3, -4, -5,  6, -7, -8,  9, -10, -11, -12,  13, 14, 15, -16, 17, -18, -19, 20]
s SATISFIABLE: [ 1, -2, -3, -4, -5,  6, -7, -8, -9, -10, -11, -12,  13, 14, 15, -16, 17, -18, -19, 20]
s SATISFIABLE: [ 1, -2, -3,  4, -5, -6, -7, -8, -9,  10, -11, -12,  13, 14, 15, -16, 17, -18, -19, 20]
s SATISFIABLE: [ 1, -2, -3,  4, -5, -6, -7,  8, -9,  10, -11, -12,  13, 14, 15, -16, 17, -18, -19, 20]
s SATISFIABLE: [ 1, -2, -3,  4, -5,  6, -7, -8, -9,  10, -11, -12,  13, 14, 15, -16, 17, -18, -19, 20]
s SATISFIABLE: [ 1, -2, -3,  4, -5,  6, -7, -8, -9, -10, -11, -12,  13, 14, 15, -16, 17, -18, -19, 20]
s UNSATISFIABLE

They seem good. Of course, we need more test cases.

from splr.

Yes, it cannot be used within wasm32 unfortunately (because of the libc dependency).

Another problem I am facing is how to turn off completely all console reports? I have tried

        let mut config: splr::Config = Default::default();
        config.quiet_mode = true;
        config.use_log = false;
        let mut solver = splr::Solver::try_from((config, self.clauses.as_ref())).unwrap();

but it is not working.

from splr.

Please use the head of branch https://github.com/shnarazk/splr/tree/dev-0.4.1. I think your problems were solved. Cargo.toml was revised.

from splr.

Ok, thanks for reminding me!

I have tried the dev-0.4.1 branch, and it gives a bad answer for my simple test:

input: [[1, 2], [-1, 2], [-1, -2], [-1, 2, 3], [1, -2, 3], [1, 2, -3], [-1, -2, -3]]
output: [-1, 2, -3]

but the output should be [-1,2,3]. What could be the problem?

from splr.

Oops. I fixed the preprocessor's bug. And I've added more tests. Please try again the head of dev-0.4.1.

from splr.

Thanks! It works now. It compiles for wasm32, but I have some other problem (or wasm32 does) and I cannot try it out yet in the browser.

from splr.

I tried wasm-pack myself and found there was time dependency that isn't implemented on WASM. By resolving it at 3490061 on dev-0.4.1, I got this.

extern crate wasm_bindgen;
use wasm_bindgen::prelude::*;
use splr::*;
use std::convert::TryFrom;

#[wasm_bindgen]
extern {
    pub fn alert(s: &str);
}

#[wasm_bindgen]
pub fn greet(name: &str) {
    let v: Vec<Vec<i32>> = vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]]; 
    let res = match Certificate::try_from(v) {
        Ok(Certificate::SAT(ans)) => format!("s SATISFIABLE: {:?}", ans),
        Ok(Certificate::UNSAT) => "UNSATISFIABLE".to_string(),
        Err(_e) => "UNKNOWN".to_string(),
     };
    alert(&format!("Hello, {}\n{:?}!", name, res));
}

'dev-0.4.1' is going to be merged into master as Splr version 0.4.1 today.

from splr.