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

Add expression manipulation

Browse source
This commit is contained in:
hal8174 2024-10-09 01:02:48 +02:00
parent 959ac83124
commit 34ad3315b3
3 changed files with 198 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/dpll.rs
View file

@ -1,6 +1,6 @@
use std::collections::HashSet;
type Index = i16;
pub type Index = i16;
fn remvove_literal(cnf: &mut Vec<Vec<Index>>, l: Index) {
cnf.retain(|c| c.binary_search(&l).is_err());

157
src/expr.rs Normal file
View file

@ -0,0 +1,157 @@
use std::collections::HashMap;
use crate::dpll::Index;
#[derive(Debug, Clone)]
pub enum Expr {
Literal(String),
Not(Box<Expr>),
And(Vec<Expr>),
Or(Vec<Expr>),
}
impl Expr {
pub fn disjunctiveNormalForm(self) -> Self {
match self {
Expr::Literal(_) => self,
Expr::Not(n) => match *n {
Expr::Literal(_) => Expr::Not(n),
Expr::Not(i) => i.disjunctiveNormalForm(),
Expr::And(v) => Expr::Or(v.into_iter().map(|e| Expr::Not(Box::new(e))).collect())
.disjunctiveNormalForm(),
Expr::Or(v) => Expr::And(v.into_iter().map(|e| Expr::Not(Box::new(e))).collect())
.disjunctiveNormalForm(),
},
Expr::And(v) => {
let v = v
.into_iter()
.flat_map(|e| {
if let Expr::And(v) = e {
v.into_iter()
} else {
vec![e].into_iter()
}
})
.collect::<Vec<_>>();
if v.iter()
.all(|e| matches!(e, Expr::Literal(_) | Expr::Not(_)))
{
return Expr::Or(vec![Expr::And(v)]);
}
if v.len() == 1 {
v.into_iter().next().unwrap()
} else {
let mut iter = v.into_iter();
let mut v = match iter.next().unwrap().disjunctiveNormalForm() {
Expr::Literal(s) => vec![Expr::Literal(s)],
Expr::Not(n) => vec![Expr::Not(n)],
Expr::And(_) => unreachable!(),
Expr::Or(v) => v,
};
for e in iter {
v = v
.into_iter()
.map(|i| Expr::And(vec![e.clone(), i]).disjunctiveNormalForm())
.collect()
}
Expr::Or(v).disjunctiveNormalForm()
}
}
Expr::Or(v) => Expr::Or(
v.into_iter()
.flat_map(|e| match e.disjunctiveNormalForm() {
Expr::Literal(s) => vec![Expr::Literal(s)].into_iter(),
Expr::Not(n) => vec![Expr::Not(n)].into_iter(),
Expr::And(_) => unreachable!(),
Expr::Or(o) => o.into_iter(),
})
.collect(),
),
}
}
pub fn conjunctiveNormalForm(self) -> Self {
if let Expr::Or(v) = Expr::Not(Box::new(self)).disjunctiveNormalForm() {
Expr::And(
v.into_iter()
.map(|e| {
if let Expr::And(v) = e {
Expr::Or(
v.into_iter()
.map(|e| match e {
Expr::Literal(s) => Expr::Not(Box::new(Expr::Literal(s))),
Expr::Not(n) => *n,
Expr::And(_) => unreachable!(),
Expr::Or(_) => unreachable!(),
})
.collect(),
)
} else {
unreachable!()
}
})
.collect(),
)
} else {
unreachable!()
}
}
pub fn to_dpll_cnf(self) -> (Vec<Vec<Index>>, HashMap<String, Index>) {
let mut map = HashMap::new();
let mut cnf = Vec::new();
let v = if let Expr::And(v) = self.conjunctiveNormalForm() {
v
} else {
unreachable!()
};
let mut nextfree = 1;
for e in v {
let mut s = Vec::new();
let v = if let Expr::Or(v) = e {
v
} else {
unreachable!()
};
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;
}
} 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;
}
} else {
unreachable!()
}
} else {
unreachable!()
}
}
cnf.push(s);
}
(cnf, map)
}
}

52
src/main.rs
View file

@ -1,22 +1,50 @@
use dpll::dpll;
use expr::Expr;
mod dpll;
mod expr;
fn main() {
let v = Expr::Not(Box::new(Expr::And(vec![
Expr::Or(vec![
Expr::Literal(String::from("a")),
Expr::Literal(String::from("b")),
]),
Expr::Or(vec![
Expr::Literal(String::from("c")),
Expr::Literal(String::from("d")),
]),
])));
dbg!(&v);
dbg!(v.clone().disjunctiveNormalForm());
dbg!(v.clone().conjunctiveNormalForm());
let (cnf, _) = dbg!(v.clone().to_dpll_cnf());
let mut solution = Vec::new();
let cnf = vec![
vec![-1, 2, 3],
vec![1, 3, 4],
vec![-4, 1, 3],
vec![-3, 1, 4],
vec![-4, -3, 1],
vec![-3, -2, 4],
vec![-3, -1, 2],
vec![-2, -1, 3],
];
dbg!(dpll(&cnf, &mut solution));
dbg!(solution);
}
// fn main() {
// let mut solution = Vec::new();
// let cnf = vec![
// vec![-1, 2, 3],
// vec![1, 3, 4],
// vec![-4, 1, 3],
// vec![-3, 1, 4],
// vec![-4, -3, 1],
// vec![-3, -2, 4],
// vec![-3, -1, 2],
// vec![-2, -1, 3],
// ];
// dbg!(dpll(&cnf, &mut solution));
// dbg!(solution);
// }