dpll for the SAT solver and some properties

testcases/Sat.scala

@@ -172,27 +172,6 @@ object Sat {
     case Not(Var(n)) => ClauseCons(VarCons(-n, VarNil()), ClauseNil())
     case Var(n) => ClauseCons(VarCons(n, VarNil()), ClauseNil())
   }
-  def property1(formula: Formula, trueVars: Set[Int]): Boolean = {
-    val dnfFormula = dnfNaive(formula)
-    eval(formula, trueVars) == evalDnf(dnfFormula, trueVars)
-  } holds
-
-  def property2(formula: Formula, trueVars: Set[Int]): Boolean = {
-    val cnfFormula = cnfNaive(formula)
-    eval(formula, trueVars) == evalCnf(cnfFormula, trueVars)
-  } holds
-
-  def propertyWrong1(formula: Formula, trueVars: Set[Int]): Boolean = {
-    val dnfFormula = dnfNaive(formula)
-    isSatDnf(dnfFormula)
-  } holds
-
-  def property3(formula: Formula, trueVars: Set[Int]): Boolean = {
-    val dnfFormula = dnfNaive(formula)
-    if(!isSatDnf(dnfFormula)) eval(formula, trueVars) else true
-  } holds
-
-
 
   def vars(formula: Formula): Set[Int] = formula match {
     case Var(n) => Set(n)
@@ -211,6 +190,23 @@ object Sat {
     case ClauseLit(b) => b
   }
 
+  def simplify(formula: ClauseList): ClauseList = formula match {
+    case ClauseNil() => ClauseNil()
+    case ClauseCons(cl, cls) => simplify(cl) match {
+      case VarNil() => ClauseLit(false)
+      case VarLit(b) => if(!b) ClauseLit(false) else ClauseCons(VarLit(b), simplify(cls))
+      case vs => ClauseCons(vs, simplify(cls))
+    }
+    case ClauseLit(b) => ClauseLit(b)
+  }
+
+  def simplify(vars: VarList): VarList = vars match {
+    case VarNil() => VarNil()
+    case VarLit(b) => VarLit(b)
+    case VarCons(VarLit(b), vs) => if(b) VarList(true) else simplify(vs)
+    case VarCons(v, vs) => VarCons(v, simplify(vs))
+  }
+
   //for substitute we assume we are dealing with a cnf formula
   def substitute(formula: ClauseList, variable: Int, value: Boolean): ClauseList = formula match {
     case ClauseNil() => ClauseNil()
@@ -223,8 +219,8 @@ object Sat {
     case VarLit(b) => VarLit(b)
     case VarCons(v, vs) => 
       if     (v == variable && value)   VarLit(true)
-      else if(v == variable && !value)  substitute(vs, variable, value)
-      else if(v == -variable && value)  substitute(vs, variable, value)
+      else if(v == variable && !value)  VarCons(VarLit(false), substitute(vs, variable, value))
+      else if(v == -variable && value)  VarCons(VarLit(false), substitute(vs, variable, value))
       else if(v == -variable && !value) VarLit(true)
       else                              VarCons(v, substitute(vs, variable, value))
   }
@@ -244,14 +240,41 @@ object Sat {
     case ClauseLit(b) => b
     case _ => {
       val chosenVar = choose(formula)
-      val lhs = dpll(substitute(formula, chosenVar, true))
-      val rhs = dpll(substitute(formula, chosenVar, false))
+      val lhs = dpll(simplify(substitute(formula, chosenVar, true)))
+      val rhs = dpll(simplify(substitute(formula, chosenVar, false)))
       lhs || rhs
     }
   }
 
 
 
+  def property1(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val dnfFormula = dnfNaive(formula)
+    eval(formula, trueVars) == evalDnf(dnfFormula, trueVars)
+  } holds
+
+  def property2(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val cnfFormula = cnfNaive(formula)
+    eval(formula, trueVars) == evalCnf(cnfFormula, trueVars)
+  } holds
+
+  def propertyWrong1(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val dnfFormula = dnfNaive(formula)
+    isSatDnf(dnfFormula)
+  } holds
+
+  def property3(formula: Formula, trueVars: Set[Int]): Boolean = {
+    val dnfFormula = dnfNaive(formula)
+    if(!isSatDnf(dnfFormula)) eval(formula, trueVars) else true
+  } holds
+
+  def property4(formula: Formula): Boolean = {
+    val cnfFormula = cnfNaive(formula)
+    val dnfFormula = dnfNaive(formula)
+    isSatDnf(dnfFormula) == dpll(cnfFormula)
+  }
+
+
 //  def main(args: Array[String]) {
 //    val f1 = And(Var(1), Or(Var(1), Not(Var(2)), Var(3)), Var(2), Not(Var(3)))
 //    val dnff1 = clauses2list(dnfNaive(f1))