Commit a0c50601 authored by Ranadeep Biswas's avatar Ranadeep Biswas
Browse files

Uses minisat lib

parent 1d6fd8ff
...@@ -6,6 +6,7 @@ authors = ["Ranadeep Biswas <ranadip.bswas@gmail.com>"] ...@@ -6,6 +6,7 @@ authors = ["Ranadeep Biswas <ranadip.bswas@gmail.com>"]
[dependencies] [dependencies]
rand = "0.7.2" rand = "0.7.2"
clap = "2.33.0" clap = "2.33.0"
minisat = "0.4.4"
serde = "1.0.103" serde = "1.0.103"
serde_derive = "1.0.103" serde_derive = "1.0.103"
serde_json = "1.0.44" serde_json = "1.0.44"
......
use std::collections::{HashMap, HashSet}; use std::collections::{HashMap, HashSet};
use std::fs;
use std::fs::{File, OpenOptions};
use std::default::Default; use std::default::Default;
use std::process::{Command, Stdio}; use minisat::{Bool, Solver};
use std::path::PathBuf;
use std::io::BufRead;
use std::io::{BufReader, BufWriter};
use std::io::Write;
#[derive(Hash, Ord, PartialOrd, Eq, PartialEq, Clone, Copy, Debug)] #[derive(Hash, Ord, PartialOrd, Eq, PartialEq, Clone, Copy, Debug)]
pub enum Edge { pub enum Edge {
...@@ -44,28 +35,24 @@ impl CNF { ...@@ -44,28 +35,24 @@ impl CNF {
self.clauses.push(Vec::new()); self.clauses.push(Vec::new());
} }
fn write_to_file(&mut self, path: &PathBuf) { fn add_to_solver(&mut self, solver: &mut Solver) -> HashMap<usize, Bool> {
let mut file = BufWriter::new( let mut literal_map = HashMap::new();
OpenOptions::new()
.write(true) for mut clause in self.clauses.drain(..).rev().skip(1) {
.create(true) let solver_clause : Vec<_> = clause.drain(..).map(|(sign, literal)| {
.truncate(true) let solver_lit = literal_map
.open(path) .entry(literal)
.expect("couldn't create"), .or_insert_with(|| solver.new_lit());
);
writeln!(file, "p cnf {} {}", self.n_variable, self.clauses.len() - 1)
.expect("failed to write parameters");
for clause in self.clauses.drain(..).rev().skip(1) {
for (sign, literal) in clause {
if sign { if sign {
write!(file, "{} ", literal).expect("failed to write cnf to file"); *solver_lit
} else { } else {
write!(file, "-{} ", literal).expect("failed to write cnf to file"); !*solver_lit
} }
} }).collect();
writeln!(file, "0").expect("failed to write cnf to file"); solver.add_clause(solver_clause);
} }
literal_map
} }
} }
...@@ -262,110 +249,64 @@ impl Sat { ...@@ -262,110 +249,64 @@ impl Sat {
self.add_clauses(&clauses); self.add_clauses(&clauses);
} }
pub fn solve(&mut self, path: &PathBuf) -> Option<Vec<(usize, usize)>> { pub fn solve(&mut self) -> Option<Vec<(usize, usize)>> {
let inp_cnf = path.join("history.cnf"); let mut solver = minisat::Solver::new();
let out_cnf = path.join("result.cnf"); let lit_map = self.cnf.add_to_solver(&mut solver);
self.cnf.write_to_file(&inp_cnf);
if let Ok(mut child) = Command::new("minisat")
.arg(&inp_cnf)
.arg(&out_cnf)
.stdout(Stdio::null())
.spawn()
{
child.wait().expect("failed to execute process");
} else {
panic!("failed to execute process")
}
fs::remove_file(inp_cnf).expect("couldn't delete input cnf");
// println!("status: {}", output.status); match solver.solve() {
// println!("stdout: {}", String::from_utf8_lossy(&output.stdout)); Ok(m) => {
// println!("stderr: {}", String::from_utf8_lossy(&output.stderr)); let edges: Vec<_> = self
.edge_variable
let result = File::open(&out_cnf).expect("file couldn't open"); .iter()
.filter_map(|(&k, &v)| {
let reader = BufReader::new(&result); if k.0 == Edge::CO {
assert!(k.1 != k.2);
let mut lines = reader.lines().map(|l| l.unwrap()); Some(if m.value(&lit_map[&v]) {
(k.1, k.2)
let mut assignments = HashMap::new(); } else {
(k.2, k.1)
match lines.next() { })
Some(ref e) if e.as_str() == "SAT" => { } else {
for line in lines { None
for var_st in line.split_whitespace() {
let var: isize = var_st.parse().unwrap();
if var != 0 {
assignments.insert(var.abs() as usize, var > 0);
} }
} })
} .collect();
}
Some(ref e) if e.as_str() == "UNSAT" => {
// println!("{:?}", e);
// for line in lines {
// println!("{}", line);
// }
}
_ => {
unreachable!();
}
}
if !assignments.is_empty() { // edges.sort_unstable();
let edges: Vec<_> = self
.edge_variable
.iter()
.filter_map(|(&k, &v)| {
if k.0 == Edge::CO {
assert!(k.1 != k.2);
Some(if assignments[&v] {
(k.1, k.2)
} else {
(k.2, k.1)
})
} else {
None
}
})
.collect();
// edges.sort_unstable(); // building co
let mut parents: HashMap<(usize, usize), HashSet<(usize, usize)>> =
Default::default();
for e in &edges {
parents
.entry(e.1)
.or_insert_with(Default::default)
.insert(e.0);
// building co parents.entry(e.0).or_insert_with(Default::default);
let mut parents: HashMap<(usize, usize), HashSet<(usize, usize)>> = Default::default(); }
for e in &edges {
parents
.entry(e.1)
.or_insert_with(Default::default)
.insert(e.0);
parents.entry(e.0).or_insert_with(Default::default); let mut lin = Vec::new();
}
let mut lin = Vec::new(); while !parents.is_empty() {
let next_t: Vec<_> = parents
.iter()
.filter_map(|(t1, t2s)| if t2s.is_empty() { Some(*t1) } else { None })
.collect();
assert_eq!(next_t.len(), 1);
while !parents.is_empty() { parents.retain(|_, t2s| !t2s.is_empty());
let next_t: Vec<_> = parents
.iter()
.filter_map(|(t1, t2s)| if t2s.is_empty() { Some(*t1) } else { None })
.collect();
assert_eq!(next_t.len(), 1);
parents.retain(|_, t2s| !t2s.is_empty()); for (_, t2s) in parents.iter_mut() {
t2s.remove(&next_t[0]);
}
for (_, t2s) in parents.iter_mut() { lin.push(next_t[0]);
t2s.remove(&next_t[0]);
} }
lin.push(next_t[0]); Some(lin)
} }
Err(()) => None,
Some(lin)
} else {
None
} }
} }
......
extern crate rand; extern crate rand;
extern crate chrono; extern crate chrono;
extern crate minisat;
extern crate rayon; extern crate rayon;
pub mod consistency; pub mod consistency;
......
...@@ -424,7 +424,7 @@ impl Verifier { ...@@ -424,7 +424,7 @@ impl Verifier {
_ => unreachable!(), _ => unreachable!(),
} }
if sat_solver.solve(&self.dir).is_some() { if sat_solver.solve().is_some() {
None None
} else { } else {
Some(self.consistency_model) Some(self.consistency_model)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment