Object

util.sat

UnitProp

Related Doc: package sat

Permalink

object UnitProp

Very naive implementation of a unit propagation routine only meant to test propagation properties of clausal encodings for small problems/operators. Performance is not an issue, correctness is however required.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. UnitProp
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. sealed trait CStatus extends AnyRef

    Permalink

    Clause satisfiability status.

  2. case class CUnit(lit: Lit) extends CStatus with Product with Serializable

    Permalink
  3. type Clause = List[Lit]

    Permalink
  4. sealed trait FStatus extends AnyRef

    Permalink

    Formula satisfiability status.

  5. type Formula = List[Clause]

    Permalink
  6. type Lit = Int

    Permalink
  7. type Model = Map[Lit, Boolean]

    Permalink

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. object CConflicting extends CStatus with Product with Serializable

    Permalink
  5. object CSat extends CStatus with Product with Serializable

    Permalink
  6. object CUnknown extends CStatus with Product with Serializable

    Permalink
  7. object FSat extends FStatus with Product with Serializable

    Permalink
  8. object FUnknown extends FStatus with Product with Serializable

    Permalink
  9. object FUnsat extends FStatus with Product with Serializable

    Permalink
  10. def applySign(lit: Lit, value: Boolean): Boolean

    Permalink

    Applies the negation to value depending on the sign of lit.

  11. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  12. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  13. def convert(f: FormulaLike): Formula

    Permalink
  14. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  15. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  16. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  17. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  18. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  19. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  20. def litValue(lit: Lit, model: Model): Option[Boolean]

    Permalink

    Returns the value of the literal as found in model.

  21. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  22. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  23. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  24. def propagate(formula: Formula): (FStatus, Model)

    Permalink

    Formula level propagation until fixed point.

    Formula level propagation until fixed point.

    formula

    the formula to run propagation on

    returns

    A pair (result, model), the model can be inconsistent with formula if status is FUnsat

  25. def propagate(clause: Clause, model: Model): CStatus

    Permalink

    Clause level propagation.

  26. def propagateSP(formula: Formula, model: Model, fstatus: FStatus = FSat, units: List[CUnit] = Nil): (FStatus, List[CUnit])

    Permalink

    Formula level single pass of propagation to detect status and units.

  27. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  28. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  29. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  31. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped