Packages

class TransformToCnf extends CnfBuilder

Plaisted transformation: used for conversion of a propositional formula into conjunctive normal form (CNF) (input format for SAT solver). A simple conversion into CNF via Shannon expansion would also be possible but it's worst-case complexity is exponential (in the number of variables) and thus even simple problems could become untractable. The Plaisted transformation results in an _equisatisfiable_ CNF-formula (it generates auxiliary variables) but runs with linear complexity. The common known Tseitin transformation uses bi-implication, whereas the Plaisted transformation uses implication only, thus the resulting CNF formula has (on average) only half of the clauses of a Tseitin transformation. The Plaisted transformation uses the polarities of sub-expressions to figure out which part of the bi-implication can be omitted. However, if all sub-expressions have positive polarity (e.g., after transformation into negation normal form) then the conversion is rather simple and the pseudo-normalization via NNF increases chances only one side of the bi-implication is needed.

Source
Solving.scala
Linear Supertypes
Type Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TransformToCnf
  2. CnfBuilder
  3. AnyRef
  4. Any
Implicitly
  1. by any2stringadd
  2. by StringFormat
  3. by Ensuring
  4. by ArrowAssoc
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new TransformToCnf(symbolMapping: SymbolMapping)

Value Members

  1. def addClauseProcessed(clause: Clause): Unit
    Definition Classes
    CnfBuilder
  2. def apply(p: CNF.Prop): Solvable
  3. def buildCnf: Array[Clause]
    Definition Classes
    CnfBuilder
  4. def constFalse: Lit
    Definition Classes
    CnfBuilder
  5. lazy val constTrue: Lit
    Definition Classes
    CnfBuilder
  6. def convertSym(sym: CNF.Sym): Lit
  7. def isConst(l: Lit): Boolean
    Definition Classes
    CnfBuilder
  8. var literalCount: Int
    Definition Classes
    TransformToCnfCnfBuilder
  9. def newLiteral(): Lit

    returns

    new Tseitin variable

    Definition Classes
    CnfBuilder