Class

util.sat

Sat4JSolver

Related Doc: package sat

Permalink

abstract class Sat4JSolver extends SolverLike with ProblemLike

A builder for dimacs models.

Linear Supertypes
ProblemLike, SolverLike, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Sat4JSolver
  2. ProblemLike
  3. SolverLike
  4. AnyRef
  5. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Sat4JSolver(solver: ISolver with IProblem)

    Permalink

Abstract Value Members

  1. abstract def addBlockingClause(c: List[Int])(implicit switchable: Boolean = false): Unit

    Permalink

    Adds a blocking clause to the solver.

    Adds a blocking clause to the solver.

    Definition Classes
    SolverLike
  2. abstract def clearLearntClauses(): Unit

    Permalink

    Removes all learnt clauses fromt the solver.

    Removes all learnt clauses fromt the solver.

    Definition Classes
    SolverLike
  3. abstract def discardModel(): Unit

    Permalink

    Discards the current model (meant to be used when iterating on models of a formula).

    Discards the current model (meant to be used when iterating on models of a formula).

    Definition Classes
    SolverLike
  4. abstract def expireTimeout(): Unit

    Permalink

    Force timeout to expire.

    Force timeout to expire.

    Definition Classes
    SolverLike
  5. abstract def findModel(assumptions: List[Int]): Try[List[Int]]

    Permalink

    Checks the problem for satisfiability

    Checks the problem for satisfiability

    assumptions

    a set of literals to assert during the check.

    returns

    Succes(m)
    Definition Classes
    ProblemLike
  6. abstract def findModel: Try[List[Int]]

    Permalink

    Checks the problem for satisfiability

    Checks the problem for satisfiability

    returns

    Success(model)
    Definition Classes
    ProblemLike
  7. abstract def getModel: Try[List[Int]]

    Permalink

    returns

    Success(model)
    Definition Classes
    SolverLike
  8. abstract def getTimeout: Int

    Permalink

    returns

    the currently set timeout value in seconds.

    Definition Classes
    SolverLike
  9. abstract def getTimeoutMs: Long

    Permalink

    returns

    the currently set timeout value in milliseconds.

    Definition Classes
    SolverLike
  10. abstract def isDBSimplficationAllowed: Boolean

    Permalink

    True iff DB simplification is allowed.

    True iff DB simplification is allowed.

    Definition Classes
    SolverLike
  11. abstract def isSatisfiable(assumptions: List[Int]): Boolean

    Permalink

    Checks the problem for satisfiability.

    Checks the problem for satisfiability.

    assumptions

    set of literals to assert during the check.

    returns

    true iff the problem is satisfiable under the given assumptions.

    Definition Classes
    ProblemLike
  12. abstract def isSatisfiable(globalTimeout: Boolean): Boolean

    Permalink

    Checks the problem for satisfiability.

    Checks the problem for satisfiability.

    globalTimeout

    if true, the timeout counter will not reset between each call.

    returns

    true iff the problem is satisfiable.

    Definition Classes
    ProblemLike
  13. abstract def isSatisfiable(assumptions: List[Int], globalTimeout: Boolean): Boolean

    Permalink

    Checks the problem for satisfiability.

    Checks the problem for satisfiability.

    assumptions

    a set of literals to assert during the check.

    globalTimeout

    if true, timeout counter will not be reset between call.

    returns

    true iff the problem is satisfiable under the given assumptions.

    Definition Classes
    ProblemLike
  14. abstract def isSatisfiable: Boolean

    Permalink

    Checks the problem for satisfiability.

    Checks the problem for satisfiability.

    returns

    true iff the problem is satisfiable.

    Definition Classes
    ProblemLike
  15. abstract def isSolverKeptHot: Boolean

    Permalink

    True iff the solver is kept hot between check-sats.

    True iff the solver is kept hot between check-sats.

    Definition Classes
    SolverLike
  16. abstract def liftCurrentModelToClause(projectOnLits: Option[Set[Int]] = None): Try[List[Int]]

    Permalink

    Lifts the negation of the current model to a clause (to be used as a blocking clause when enumerating models), optionally projecting the model over the given set of literals.

    Lifts the negation of the current model to a clause (to be used as a blocking clause when enumerating models), optionally projecting the model over the given set of literals.

    projectOnLits

    A list of literals on which to restrict the clause

    returns

    Success(clause)
    Definition Classes
    SolverLike
  17. abstract def liftCurrentModelToCube(projectOnLits: Option[Set[Int]] = None): Try[List[Int]]

    Permalink

    Lifts the current model to a cube, optionally projecting the model over the given set of literals.

    Lifts the current model to a cube, optionally projecting the model over the given set of literals.

    projectOnLits

    A list of literals on which to restrict the cube

    returns

    Success(cube)
    Definition Classes
    SolverLike
  18. abstract def model: Try[List[Int]]

    Permalink

    returns

    Success(m)
    Definition Classes
    ProblemLike
  19. abstract def primeImplicant(lit: Int): Try[Boolean]

    Permalink

    Checks if the given literal is part of the prime implicant computed using the previous call to primeImplicant.

    Checks if the given literal is part of the prime implicant computed using the previous call to primeImplicant.

    returns

    Success(b)
    Definition Classes
    ProblemLike
  20. abstract def primeImplicant: Try[List[Int]]

    Permalink

    Generates a prime implicant of the problem if some exists.

    Generates a prime implicant of the problem if some exists.

    returns

    Success(pi)
    Definition Classes
    ProblemLike
  21. abstract def reset(): Unit

    Permalink

    Resets the solver to a clean state.

    Resets the solver to a clean state.

    Definition Classes
    SolverLike
  22. abstract def setDBSimplificationAllowed(value: Boolean): Unit

    Permalink

    Enable/disable clause DB simplification.

    Enable/disable clause DB simplification.

    Definition Classes
    SolverLike
  23. abstract def setKeepSolverHot(value: Boolean): Unit

    Permalink

    Enable/disable the "keep solver hot" feature.

    Enable/disable the "keep solver hot" feature.

    Definition Classes
    SolverLike
  24. abstract def setTimeout(duration: Int): Unit

    Permalink

    Sets a timeout expressed in seconds.

    Sets a timeout expressed in seconds.

    duration

    timeout duration in seconds.

    Definition Classes
    SolverLike
  25. abstract def setTimeoutMs(duration: Long): Unit

    Permalink

    Sets a timeout expressed in milliseconds.

    Sets a timeout expressed in milliseconds.

    duration

    timeout duration in milliseconds.

    Definition Classes
    SolverLike
  26. abstract def setTimeoutOnConflicts(nofConflicts: Int): Unit

    Permalink

    Sets a timeout expressed as a number of conflicts.

    Sets a timeout expressed as a number of conflicts.

    nofConflicts

    timeout duration in number of conflicts reached.

    Definition Classes
    SolverLike
  27. abstract def unsatExplanation: Try[List[Int]]

    Permalink

    Returns a clause explaning the unsat state of the constraints (must follow a call to ProblemLike.isSatisfiable that returned false.

    Returns a clause explaning the unsat state of the constraints (must follow a call to ProblemLike.isSatisfiable that returned false.

    returns

    Success(clause)
    Definition Classes
    SolverLike

Concrete 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. final def asInstanceOf[T0]: T0

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

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  6. final def eq(arg0: AnyRef): Boolean

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

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

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

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

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

    Permalink
    Definition Classes
    Any
  12. final def ne(arg0: AnyRef): Boolean

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

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

    Permalink
    Definition Classes
    AnyRef
  15. final def synchronized[T0](arg0: ⇒ T0): T0

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

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

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

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

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

Inherited from ProblemLike

Inherited from SolverLike

Inherited from AnyRef

Inherited from Any

Ungrouped