Written by Hossein Hojjat

object DPLL
{
  case class Literal(val name: String, val pos: Boolean)
  def negate(l : Literal) = Literal(l.name, !l.pos)
  type Clause = Set[Literal]
  def DPLL(f : Set[Clause]) : (Boolean,Map[String,Boolean]) = {
    if(f.isEmpty) return (true,Map.empty[String,Boolean])
    if(f.exists(clause => clause.isEmpty)) return (false,Map.empty[String,Boolean])
    if(f.exists(clause => clause.size == 1)) {
      val unit_clause: Literal = f.find(clause => clause.size == 1) match { case Some(c) => c.toList.head}
      val nf = f.filter( clause => (!clause.contains(unit_clause)))
        .map( clause => if (clause.contains(negate(unit_clause))) (clause - negate(unit_clause)) else clause)
      val (ds,dm) = DPLL(nf)
      return (ds,dm + (if (unit_clause.pos) (unit_clause.name -> true) else (unit_clause.name -> false)))
    }
    val literals = f.reduceLeft((a,b) => a ++ b)
    var pures: Set[Literal] = Set.empty[Literal]
    literals.foreach(l => (if(pures.contains(negate(l))) pures --= Set(l,negate(l)) else pures += l))
    if(pures.size != 0) {
      val pure = pures.toList.head
      val (ds,dm) = DPLL(f.filter( clause => (!clause.contains(pure))))
      return (ds,dm + (if (pure.pos) (pure.name -> true) else (pure.name -> false)))
    }
    val literal_to_split = f.toList.head.toList.head
    val (ds,dm) = DPLL(f + Set(literal_to_split))
    if(ds) (true, dm) else DPLL(f + Set(negate(literal_to_split))) 
  }    
  def main(args : Array[String]) : Unit = {
    var form = Set.empty[Clause]
    var clause = Set.empty[Literal]
    var tok:String = ""
    scala.io.Source.fromFile(new java.io.File(args(0))).getLines.foreach {
      line => if( !line.startsWith("c") && !line.startsWith("p")) {
        val scanner = new java.util.Scanner(line)
        while(scanner.hasNext) {
          tok = scanner.next
          if (tok != "0") 
            {if( tok.startsWith("-")) clause += Literal(tok.drop(1), false) else clause += Literal(tok, true)} 
          else {
            form += clause
            clause = Set.empty[Literal]
    }}}}
    if( clause.size != 0) form += clause
    val (rs,rm) = DPLL(form)
    if(rs) println("s SATISFIABLE\nv " + rm.map(m => (if( m._2) m._1 else "-" + m._1)).mkString(" "))
    else println("s UNSATISFIABLE")   
  }
}