hal8174/simple-sat-solver
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Clean up and preperations for cdcl

Browse source
This commit is contained in:
hal8174 2024-10-22 14:45:02 +02:00
parent 9d9f75dd20
commit 830a3387b0
6 changed files with 93 additions and 122 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/cdcl.rs Normal file
View file

@ -0,0 +1,21 @@
use crate::{dpll::Index, normal_form::NormalForm};
enum Result {
Complete,
Conflict(Vec<Index>),
}
fn cdcl_internal(
cnf: &NormalForm,
solution: &mut Vec<Index>,
graph: Vec<(Index, Index)>,
) -> Result {
todo!()
}
pub fn cdcl(cnf: &NormalForm, solution: &mut Vec<Index>) -> bool {
match cdcl_internal(cnf, solution, vec![]) {
Result::Complete => true,
Result::Conflict(_) => false,
}
}

1
src/dpll.rs
View file

@ -21,7 +21,6 @@ fn unit_propagate(cnf: &mut Vec<Vec<Index>>, solution: &mut Vec<Index>) {
{
let l = cnf[i][0];
solution.push(l);
cnf.swap_remove(i);
remvove_literal(cnf, l);
unit_propagate(cnf, solution);
}

4
src/dpll_normal_form.rs
View file

@ -1,6 +1,4 @@
use std::{
borrow::BorrowMut, cell::RefCell, collections::HashSet, ops::DerefMut, sync::RwLockWriteGuard,
};
use std::{cell::RefCell, collections::HashSet};
use crate::{dpll::Index, normal_form::NormalForm};

84
src/expr.rs
View file

@ -1,6 +1,5 @@
use crate::{dpll::Index, mapping::Mapping, normal_form::NormalForm};
use miette::{miette, Context, Result};
use std::collections::HashMap;
#[derive(Debug, Clone)]
pub enum Expr<'s> {
@ -171,25 +170,25 @@ impl<'s> Expr<'s> {
}
}
pub fn disjunctiveNormalForm(self) -> Self {
pub fn disjunctive_normal_form(self) -> Self {
// dbg!(&self);
match self {
Expr::Literal(_) => self,
Expr::Not(n) => match *n {
Expr::Literal(_) => Expr::Not(n),
Expr::Not(i) => i.disjunctiveNormalForm(),
Expr::Not(i) => i.disjunctive_normal_form(),
Expr::And(v) => Expr::Or(
v.into_iter()
.map(|e| Expr::Not(Box::new(e)).disjunctiveNormalForm())
.map(|e| Expr::Not(Box::new(e)).disjunctive_normal_form())
.collect(),
)
.disjunctiveNormalForm(),
.disjunctive_normal_form(),
Expr::Or(v) => Expr::And(
v.into_iter()
.map(|e| Expr::Not(Box::new(e)).disjunctiveNormalForm())
.map(|e| Expr::Not(Box::new(e)).disjunctive_normal_form())
.collect(),
)
.disjunctiveNormalForm(),
.disjunctive_normal_form(),
},
Expr::And(v) => {
let v = v
@ -213,7 +212,7 @@ impl<'s> Expr<'s> {
v.into_iter().next().unwrap()
} else {
let mut iter = v.into_iter();
let mut v = match iter.next().unwrap().disjunctiveNormalForm() {
let mut v = match iter.next().unwrap().disjunctive_normal_form() {
Expr::Literal(s) => vec![Expr::Literal(s)],
Expr::Not(n) => vec![Expr::Not(n)],
Expr::And(_) => unreachable!(),
@ -223,16 +222,16 @@ impl<'s> Expr<'s> {
for e in iter {
v = v
.into_iter()
.map(|i| Expr::And(vec![e.clone(), i]).disjunctiveNormalForm())
.map(|i| Expr::And(vec![e.clone(), i]).disjunctive_normal_form())
.collect()
}
Expr::Or(v).disjunctiveNormalForm()
Expr::Or(v).disjunctive_normal_form()
}
}
Expr::Or(v) => Expr::Or(
v.into_iter()
.flat_map(|e| match e.disjunctiveNormalForm() {
.flat_map(|e| match e.disjunctive_normal_form() {
Expr::Literal(s) => vec![Expr::Literal(s)].into_iter(),
Expr::Not(n) => vec![Expr::Not(n)].into_iter(),
Expr::And(_) => unreachable!(),
@ -243,7 +242,7 @@ impl<'s> Expr<'s> {
}
}
pub fn disjunctiveNormalForm2(self, mapping: &mut Mapping<'s>) -> NormalForm {
pub fn disjunctive_normal_form2(self, mapping: &mut Mapping<'s>) -> NormalForm {
match self {
Expr::Literal(l) => {
let mut n = NormalForm::new();
@ -256,12 +255,12 @@ impl<'s> Expr<'s> {
n.add_clause(&[-mapping.forward(l)]);
n
}
Expr::Not(n) => n.disjunctiveNormalForm2(mapping),
Expr::Not(n) => n.disjunctive_normal_form2(mapping),
Expr::And(v) => {
let mut n = NormalForm::new();
for e in v
.into_iter()
.map(|e| Expr::Not(Box::new(e)).disjunctiveNormalForm2(mapping))
.map(|e| Expr::Not(Box::new(e)).disjunctive_normal_form2(mapping))
{
for (s, _, _) in e.iter() {
n.add_clause(s);
@ -271,12 +270,12 @@ impl<'s> Expr<'s> {
}
Expr::Or(v) => Expr::And(v.into_iter().map(|e| Expr::Not(Box::new(e))).collect())
.disjunctiveNormalForm2(mapping),
.disjunctive_normal_form2(mapping),
},
Expr::And(v) => {
let mut v: Vec<_> = v
.into_iter()
.map(|e| e.disjunctiveNormalForm2(mapping))
.map(|e| e.disjunctive_normal_form2(mapping))
.collect();
let mut n = v.pop().unwrap();
@ -305,7 +304,7 @@ impl<'s> Expr<'s> {
Expr::Or(v) => {
let mut n = NormalForm::new();
for e in v {
let on = e.disjunctiveNormalForm2(mapping);
let on = e.disjunctive_normal_form2(mapping);
for (s, _, _) in on.iter() {
n.add_clause(s);
}
@ -316,8 +315,8 @@ impl<'s> Expr<'s> {
}
}
pub fn conjunctiveNormalForm(self) -> Self {
if let Expr::Or(v) = Expr::Not(Box::new(self)).disjunctiveNormalForm() {
pub fn conjunctive_normal_form(self) -> Self {
if let Expr::Or(v) = Expr::Not(Box::new(self)).disjunctive_normal_form() {
Expr::And(
v.into_iter()
.map(|e| match e {
@ -348,51 +347,37 @@ impl<'s> Expr<'s> {
}
}
pub fn to_dpll_cnf_normal_form(self) -> (NormalForm, Mapping<'s>) {
pub fn cnf_normal_form(self) -> (NormalForm, Mapping<'s>) {
let mut mapping = Mapping::new();
let mut cnf = Expr::Not(Box::new(self)).disjunctiveNormalForm2(&mut mapping);
let mut cnf = Expr::Not(Box::new(self)).disjunctive_normal_form2(&mut mapping);
cnf.negate();
(cnf, mapping)
}
pub fn to_dpll_cnf(self) -> (Vec<Vec<Index>>, HashMap<&'s str, Index>) {
let mut map = HashMap::new();
pub fn cnf(self) -> (Vec<Vec<Index>>, Mapping<'s>) {
let mut map = Mapping::new();
let mut cnf = Vec::new();
let v = if let Expr::And(v) = self.conjunctiveNormalForm() {
let v = if let Expr::And(v) = self.conjunctive_normal_form() {
v
} else {
unreachable!()
};
let mut nextfree = 1;
for e in v {
let s = match e {
Expr::Or(v) => {
let mut s = Vec::new();
for l in v {
if let Expr::Literal(l) = l {
if let Some(&i) = map.get(&l) {
s.push(i);
} else {
map.insert(l, nextfree);
s.push(nextfree);
nextfree += 1;
}
s.push(map.forward(l));
} else if let Expr::Not(n) = l {
if let Expr::Literal(l) = *n {
if let Some(&i) = map.get(&l) {
s.push(-i);
} else {
map.insert(l, nextfree);
s.push(-nextfree);
nextfree += 1;
}
s.push(-map.forward(l));
} else {
unreachable!()
}
@ -401,28 +386,15 @@ impl<'s> Expr<'s> {
}
}
s.sort();
s.dedup();
s
}
Expr::Literal(l) => {
if let Some(&i) = map.get(&l) {
vec![-i]
} else {
map.insert(l, nextfree);
let i = nextfree;
nextfree += 1;
vec![-i]
}
vec![-map.forward(l)]
}
Expr::Not(n) => {
if let Expr::Literal(l) = *n {
if let Some(&i) = map.get(&l) {
vec![i]
} else {
map.insert(l, nextfree);
let i = nextfree;
nextfree += 1;
vec![i]
}
vec![map.forward(l)]
} else {
unreachable!()
}

103
src/main.rs
View file

@ -1,88 +1,71 @@
use std::collections::HashMap;
use clap::Parser;
use dpll::dpll;
use expr::{Expr, Tokanizer};
use mapping::Mapping;
use clap::{Parser, ValueEnum};
use expr::Expr;
use miette::{IntoDiagnostic, Result};
use normal_form::NormalForm;
mod cdcl;
mod dpll;
mod dpll_normal_form;
mod expr;
mod mapping;
mod normal_form;
mod expr;
#[derive(ValueEnum, Clone)]
enum Method {
DpllExpr,
Dpll,
Cdcl,
}
#[derive(Parser)]
struct Args {
method: Method,
inputfile: std::path::PathBuf,
}
fn main() -> Result<()> {
let args = Args::parse();
let start = std::time::Instant::now();
let s = std::fs::read_to_string(args.inputfile).into_diagnostic()?;
let e = Expr::parse(&s)?;
println!("Expression parsed succesfully.");
// dbg!(&e);
// dbg!(Expr::Not(Box::new(e.clone())).disjunctiveNormalForm());
let (cnf, map) = e.to_dpll_cnf_normal_form();
println!("Normal form created.");
cnf.stats();
let elapsed = start.elapsed();
println!("Expression parsed succesfully in {elapsed:?}");
let mut solution = Vec::new();
let start = std::time::Instant::now();
dbg!(crate::dpll_normal_form::dpll(&cnf, &mut solution));
let (result, map) = match args.method {
Method::DpllExpr => {
let (cnf, map) = e.cnf();
(crate::dpll::dpll(&cnf, &mut solution), map)
}
Method::Dpll => {
let (cnf, map) = e.cnf_normal_form();
(crate::dpll_normal_form::dpll(&cnf, &mut solution), map)
}
Method::Cdcl => {
let (cnf, map) = e.cnf_normal_form();
(crate::cdcl::cdcl(&cnf, &mut solution), map)
}
};
let elapsed = start.elapsed();
println!("Time dpll: {elapsed:?}");
println!("Time: {elapsed:?}");
// dbg!(&solution);
// dbg!(e.clone().conjunctiveNormalForm());
// let (cnf, map) = e.to_dpll_cnf();
// dbg!(&cnf, &map);
// println!("cnf clauses: {}", cnf.len());
// let mut solution = Vec::new();
// dpll(&cnf, &mut solution);
// dbg!(solution);
// let inv_map: HashMap<_, _> = map.into_iter().map(|(k, v)| (v, k)).collect();
// dbg!(&solution);
let mut s = Vec::new();
for i in solution {
if i > 0 {
s.push((map.backward(i), true));
} else {
s.push((map.backward(i.abs()), false));
if result {
println!("Solution found:");
let mut s = Vec::new();
for i in solution {
if i > 0 {
s.push((map.backward(i), true));
} else {
s.push((map.backward(i.abs()), false));
}
}
s.sort();
for (s, b) in s {
println!("{s}: {b}");
}
}
s.sort();
for (s, b) in s {
println!("{s}: {b}");
}
// let mut nf = NormalForm::from_slices(&cnf);
// dbg!(&nf);
// nf.remove_literal(-1);
// dbg!(&nf);
// let mut s2 = Vec::new();
// dbg!(dpll_normal_form::dpll(&nf, &mut s2));
// dbg!(s2 == solution);
Ok(())
}

2
src/normal_form.rs
View file

@ -1,5 +1,3 @@
use std::ops::Neg;
use crate::dpll::Index;
#[derive(Debug, Clone)]