Submission #3336727

---

Source Code Expand

import collection.mutable
import scala.collection.mutable.ListBuffer

object Main {
  def main(args: Array[String]): Unit = {
    import scala.io.StdIn.readLine
    val Array(n, m) = readLine().split(" ").map(_.toInt)
    val cnf = CNF(readLine())
    val assignment = Assignment(readLine().map(_ == 'T'))

    val varToClauseIndexes = {
      val builder = mutable.Map[Var, mutable.ListBuffer[Int]]()
      builder ++= (0 until n).map(i => i -> ListBuffer[Int]())
      for {
        (c, i) <- cnf.zipWithIndex
        v <- c.vars
      } {
        builder(v) += i
      }
      builder.toMap.mapValues(seq => mutable.BitSet() ++= seq)
    }

    val falseCaluseIndexes = mutable.BitSet() ++= cnf.zipWithIndex.flatMap{
      case (c, i) if !c.test(assignment) => Some(i)
      case _ => None
    }

    def count(vars: Set[Var], falseSet: mutable.BitSet): Int = {
      if (vars.size > 10) return Int.MaxValue
      if (falseSet.isEmpty) return vars.size

      cnf(falseSet.head).vars.filterNot(vars.contains).map(v => {
        count(vars + v, falseSet ^ varToClauseIndexes(v))
      }) match {
        case list if list.isEmpty => Int.MaxValue
        case list => list.min
      }
    }

    val result = count(Set(), falseCaluseIndexes)
    if (result == Int.MaxValue) println("TOO LARGE") else println(result)
  }

  type CNF = IndexedSeq[Clause]
  type Var = Int

  case class Clause(left: Literal, right: Literal) {
    def test(assignment: Assignment): Boolean = {
      left.test(assignment) || right.test(assignment)
    }

    def vars = Seq(left.i, right.i)
  }

  case class Literal(i: Var, tilde: Boolean) {
    def test(assignment: Assignment): Boolean = {
      if (tilde) !assignment.list(i) else assignment.list(i)
    }
  }

  object CNF {
    def apply(str: String): CNF = {
      str.split("\\^").map(s => Clause(s))
    }
  }

  object Clause {
    def apply(str: String): Clause = {
      val Array(left, right) = str.slice(1, str.length - 1).split("v")
      Clause(Literal(left), Literal(right))
    }
  }

  object Literal {
    def apply(str: String): Literal = {
      str.split("~") match {
        case Array(x) => new Literal(x.toInt - 1, false)
        case Array("", x) => new Literal(x.toInt - 1, true)
      }
    }
  }

  case class Assignment(list: IndexedSeq[Boolean]) {
    def *(set: Set[Int]): Assignment = {
      val arr = list.toArray
      set.foreach(i => arr(i) = !arr(i))
      Assignment(arr.toIndexedSeq)
    }
  }

}

Submission Info

Judge Result