Skip to content

Commit

Permalink
Add testing for encodings of propositional logic formulae
Browse files Browse the repository at this point in the history
  • Loading branch information
@Dekker1
Dekker1 committed May 6, 2024
1 parent c687528 commit 1e90f85
Showing 1 changed file with 256 additions and 37 deletions.
293 changes: 256 additions & 37 deletions crates/pindakaas/src/propositional_logic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,17 +2,26 @@ use std::{fmt::Display, iter::once, ops::Not};

use itertools::{Itertools, Position};

use crate::{ClauseDatabase, Cnf, Encoder, Lit, Result};
use crate::{ClauseDatabase, Cnf, Encoder, Lit, Result, Unsatisfiable};

/// A propositional logic formula
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Formula {
///A atomic formula (a literal)
Atom(Lit),
/// The negation of a sub-formula
Not(Box<Formula>),
/// A conjunction of two or more sub-formulas
And(Vec<Formula>),
/// A disjunction of two or more sub-formulas
Or(Vec<Formula>),
/// An implication of two sub-formulas
Implies(Box<Formula>, Box<Formula>),
/// The equivalence of two or more sub-formulas
Equiv(Vec<Formula>),
/// An exclusive or of two or more sub-formulas
Xor(Vec<Formula>),
/// A choice between two sub-formulas
IfThenElse {
cond: Box<Formula>,
then: Box<Formula>,
Expand All @@ -21,6 +30,7 @@ pub enum Formula {
}

impl Formula {
/// Convert propositional logic formula to CNF
pub fn clausify(&self) -> Result<Cnf> {
let mut cnf = Cnf::default();
cnf.encode(self, &TseitinEncoder)?;
Expand All @@ -33,49 +43,59 @@ impl Formula {
Ok(match self {
Formula::Atom(lit) => {
if let Some(name) = name {
db.add_clause(vec![!name, *lit])?;
db.add_clause(vec![name, !lit])?;
if *lit != name {
db.add_clause([!name, *lit])?;
db.add_clause([name, !lit])?;
}
name
} else {
*lit
}
}
Formula::Not(f) => !(f.bind(db, name)?),
Formula::And(sub) => {
assert_ne!(sub.len(), 0, "unable to bind empty and formula");
if sub.len() == 1 {
return sub[0].bind(db, name);
}
let name = name.unwrap_or_else(|| db.new_var().into());
let lits = sub
.iter()
.map(|f| f.bind(db, None))
.collect::<Result<Vec<_>>>()?;
// not name -> (not lits[0] or not lits[1] or ...)
db.add_clause(once(name).chain(lits.iter().map(|l| !l)))?;
for lit in lits {
// name -> lit
db.add_clause([!name, lit])?;
match sub.len() {
0 => {
let name = name.unwrap_or_else(|| db.new_var().into());
db.add_clause([name])?;
name
}
1 => return sub[0].bind(db, name),
_ => {
let name = name.unwrap_or_else(|| db.new_var().into());
let lits = sub
.iter()
.map(|f| f.bind(db, None))
.collect::<Result<Vec<_>>>()?;
// not name -> (not lits[0] or not lits[1] or ...)
db.add_clause(once(name).chain(lits.iter().map(|l| !l)))?;
for lit in lits {
// name -> lit
db.add_clause([!name, lit])?;
}
name
}
}
name
}
Formula::Or(sub) => {
assert_ne!(sub.len(), 0, "unable to bind empty or formula");
if sub.len() == 1 {
return sub[0].bind(db, name);
}
let name = name.unwrap_or_else(|| db.new_var().into());
let lits = sub
.iter()
.map(|f| f.bind(db, None))
.collect::<Result<Vec<_>>>()?;
for lit in &lits {
// not name -> not lit
db.add_clause([name, !lit])?;
match sub.len() {
0 => return Err(Unsatisfiable),
1 => return sub[0].bind(db, name),
_ => {
let name = name.unwrap_or_else(|| db.new_var().into());
let lits = sub
.iter()
.map(|f| f.bind(db, None))
.collect::<Result<Vec<_>>>()?;
for lit in &lits {
// not name -> not lit
db.add_clause([name, !lit])?;
}
// name -> (lit[0] or lit[1] or ...)
db.add_clause(once(!name).chain(lits.into_iter()))?;
name
}
}
// name -> (lit[0] or lit[1] or ...)
db.add_clause(once(!name).chain(lits.into_iter()))?;
name
}
Formula::Implies(left, right) => {
let name = name.unwrap_or_else(|| db.new_var().into());
Expand All @@ -91,7 +111,7 @@ impl Formula {
}
Formula::Equiv(sub) => {
assert!(
sub.len() < 2,
sub.len() >= 2,
"unable to bind the equivalence of less than 2 formulas"
);
let name = name.unwrap_or_else(|| db.new_var().into());
Expand Down Expand Up @@ -224,6 +244,19 @@ impl<DB: ClauseDatabase> Encoder<DB, Formula> for TseitinEncoder {
let neg_sub = sub.iter().map(|f| !(f.clone())).collect();
self.encode(db, &Formula::And(neg_sub))
}
Formula::Implies(x, y) => {
self.encode(db, x)?;
self.encode(db, &!(**y).clone())
}
Formula::IfThenElse { cond, then, els } => {
let name = cond.bind(db, None)?;
let mut cdb = db.with_conditions(vec![!name]);
let neg_then: Formula = !*then.clone();
self.encode(&mut cdb, &neg_then)?;
let mut cdb = db.with_conditions(vec![name]);
let neg_els: Formula = !*els.clone();
self.encode(&mut cdb, &neg_els)
}
_ => {
let l = f.bind(db, None)?;
db.add_clause([!l])
Expand All @@ -236,6 +269,9 @@ impl<DB: ClauseDatabase> Encoder<DB, Formula> for TseitinEncoder {
Ok(())
}
Formula::Or(sub) => {
if sub.is_empty() {
return Err(Unsatisfiable);
}
let lits = sub
.iter()
.map(|f| f.bind(db, None))
Expand Down Expand Up @@ -267,12 +303,12 @@ impl<DB: ClauseDatabase> Encoder<DB, Formula> for TseitinEncoder {
Ok(())
}
Formula::Xor(sub) => match sub.len() {
0 => Ok(()),
0 => Err(crate::Unsatisfiable),
1 => self.encode(db, &sub[0]),
_ => {
let mut sub = sub.clone();
let a = sub.pop().map(|f| f.bind(db, None)).unwrap()?;
let b = if sub.len() > 1 {
let b = sub.pop().map(|f| f.bind(db, None)).unwrap()?;
let a = if sub.len() > 1 {
Formula::Xor(sub).bind(db, None)
} else {
sub.pop().map(|f| f.bind(db, None)).unwrap()
Expand All @@ -291,3 +327,186 @@ impl<DB: ClauseDatabase> Encoder<DB, Formula> for TseitinEncoder {
}
}
}

#[cfg(test)]
mod tests {
use crate::{
helpers::tests::{assert_enc_sol, lits},
Encoder, Formula, Lit, TseitinEncoder,
};

#[test]
fn encode_prop_and() {
assert_enc_sol!(
TseitinEncoder,
3,
&Formula::And(vec![
Formula::Atom(1.into()),
Formula::Atom(2.into()),
Formula::Atom(3.into()),
])
=> vec![lits![1], lits![2], lits![3]],
vec![lits![1, 2, 3],]
);
assert_enc_sol!(
TseitinEncoder,
3,
&Formula::Equiv(vec![
Formula::Atom(3.into()),
Formula::And(vec![
Formula::Atom(1.into()),
Formula::Atom(2.into()),
])
])
=> vec![lits![-1, -2, 3], lits![1, -3], lits![2, -3]],
vec![lits![1, 2, 3], lits![-1, 2, -3], lits![-1, -2, -3], lits![1, -2, -3]]
);
}

#[test]
fn encode_prop_or() {
assert_enc_sol!(
TseitinEncoder,
3,
&Formula::Or(vec![
Formula::Atom(1.into()),
Formula::Atom(2.into()),
Formula::Atom(3.into()),
])
=> vec![lits![1, 2, 3]],
vec![lits![1,2,3], lits![-1,2,3], lits![1,-2,3], lits![1,2,-3], lits![-1,-2,3], lits![1,-2,-3],lits![-1,2,-3],]
);
assert_enc_sol!(
TseitinEncoder,
3,
&Formula::Equiv(vec![
Formula::Atom(3.into()),
Formula::Or(vec![
Formula::Atom(1.into()),
Formula::Atom(2.into()),
])
])
=> vec![lits![1, 2, -3], lits![-1, 3], lits![-2, 3]],
vec![lits![1, 2, 3], lits![-1, 2, 3], lits![-1, -2, -3], lits![1, -2, 3]]
);
}

#[test]
fn encode_prop_implies() {
assert_enc_sol!(
TseitinEncoder,
2,
&Formula::Implies(
Box::new(Formula::Atom(1.into())),
Box::new(Formula::Atom(2.into()))
)
=> vec![lits![-1, 2]],
vec![lits![-1, -2], lits![1, 2], lits![-1, 2]]
);
assert_enc_sol!(
TseitinEncoder,
3,
&Formula::Equiv(
vec![
Formula::Atom(3.into()),
Formula::Implies(
Box::new(Formula::Atom(1.into())),
Box::new(Formula::Atom(2.into())),
)]
)
=> vec![lits![-1, 2, -3], lits![1, 3], lits![-2, 3]],
vec![lits![1, 2, 3], lits![1, -2, -3], lits![-1, -2, 3], lits![-1, 2, 3]]
);
}

#[test]
fn encode_prop_equiv() {
assert_enc_sol!(
TseitinEncoder,
4,
&Formula::Equiv(vec![
Formula::Atom(1.into()),
Formula::Atom(2.into()),
Formula::Atom(3.into()),
Formula::Atom(4.into())
])
=> vec![lits![-1, 2], lits![1, -2], lits![1, -3], lits![-1, 3], lits![1, -4], lits![-1, 4]],
vec![lits![1, 2, 3, 4], lits![-1, -2, -3, -4]]
);
assert_enc_sol!(
TseitinEncoder,
3,
&Formula::Equiv(vec![
Formula::Atom(3.into()),
Formula::Equiv(vec![
Formula::Atom(1.into()),
Formula::Atom(2.into()),
])
])
=> vec![lits![-1, 2, -3], lits![1, -2, -3], lits![-1, -2, 3], lits![1, 2, 3]],
vec![lits![1, 2, 3], lits![-1, 2, -3], lits![-1, -2, 3], lits![1, -2, -3]]
);
}

#[test]
fn encode_prop_xor() {
assert_enc_sol!(
TseitinEncoder,
4,
&Formula::Xor(vec![
Formula::Atom(1.into()),
Formula::Atom(2.into()),
Formula::Atom(3.into()),
Formula::Atom(4.into()),
])
=> vec![
lits![-1, -3, -6], lits![1, 3, -6], lits![1, -3, 6], lits![-1, 3, 6],
lits![-2, -5, -6], lits![2, -5, 6], lits![2, 5, -6], lits![-2, 5, 6],
lits![4, 5], lits![-4, -5]],
vec![lits![-1, 2, 3, 4], lits![1, -2, 3, 4], lits![1, 2, -3, 4], lits![1, 2, 3, -4], lits![-1, -2, -3, 4], lits![-1, -2, 3, -4], lits![-1, 2, -3, -4], lits![1, -2, -3, -4]]
);
assert_enc_sol!(
TseitinEncoder,
4,
&Formula::Equiv(vec![
Formula::Atom(4.into()),
Formula::Xor(vec![
Formula::Atom(1.into()),
Formula::Atom(2.into()),
Formula::Atom(3.into()),
])
])
=> vec![lits![-1, -3, -5], lits![1, 3, -5], lits![-1, 3, 5], lits![1, -3, 5], lits![-2, -4, -5], lits![2, -4, 5], lits![2, 4, -5], lits![-2, 4, 5]],
vec![lits![-1, -2, -3, -4], lits![-1, -2, 3, 4], lits![-1, 2, -3, 4], lits![-1, 2, 3, -4], lits![1, -2, -3, 4], lits![1, -2, 3, -4], lits![1, 2, -3, -4], lits![1, 2, 3, 4]]
);
}

#[test]
fn encode_prop_ite() {
assert_enc_sol!(
TseitinEncoder,
3,
&Formula::IfThenElse{
cond: Box::new(Formula::Atom(1.into())),
then: Box::new(Formula::Atom(2.into())),
els: Box::new(Formula::Atom(3.into())),
}
=> vec![lits![-1, 2], lits![1, 3]],
vec![lits![-1, -2, 3], lits![-1, 2, 3], lits![1, 2, -3], lits![1, 2, 3]]
);
assert_enc_sol!(
TseitinEncoder,
4,
&Formula::Equiv(vec![
Formula::Atom(4.into()),
Formula::IfThenElse{
cond: Box::new(Formula::Atom(1.into())),
then: Box::new(Formula::Atom(2.into())),
els: Box::new(Formula::Atom(3.into())),
}
])
=> vec![lits![-1, 2, -4], lits![1, 3, -4], lits![-1, -2, 4], lits![1, -3, 4], lits![-2, -3, 4]],
vec![lits![-1, -2, -3, -4], lits![-1, -2, 3, 4], lits![1, -2, 3, -4], lits![1, 2, 3, 4], lits![1, 2, -3, 4], lits![1, -2, -3, -4], lits![-1, 2, 3, 4], lits![-1, 2, -3, -4]]
);
}
}

0 comments on commit 1e90f85

Please sign in to comment.