Package

util

sat

Permalink

package sat

Visibility
  1. Public
  2. All

Type Members

  1. case class BijectionEncoder(nnf: Expr, circuit: FormulaLike, primaryEncoder: NNFToCircuitEncoder, witnessEncoder: WitnessEncoder, drFormula: FormulaLike, drEncoder: DualRailEncoder) extends Product with Serializable

    Permalink

    Adds constraints to the dual rail formula that enforce a bijection between models of the dual rail formula and prime implicants of the original formula: - the input atom of each witness circuit is equal to the inverse of the corresponding input when is switch is on, and to the input otherwise.

    Adds constraints to the dual rail formula that enforce a bijection between models of the dual rail formula and prime implicants of the original formula: - the input atom of each witness circuit is equal to the inverse of the corresponding input when is switch is on, and to the input otherwise. - the positive dual-rail literal of the witness circuit must be false (by adding a unit clause).

  2. class CNFPrimeImplicantBackTranslator extends AnyRef

    Permalink

    A back translator from models of the target formula to prime implicants of the source formula.

  3. class CNFPrimeImplicants extends AnyRef

    Permalink

    A class implementing the translation algorithm described in the paper "Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form" by Said Jabbour, Joao Marques-Silva, Lakhdar Sais and Yakoub Salhi.

  4. trait CircuitLike extends AnyRef

    Permalink

    An interface for building circuit-like formulas on top of CNF formulas.

  5. trait CnfLike extends AnyRef

    Permalink

    An interface for building formulas in conjunctive normal form.

  6. case class DualRailEncoder(source: FormulaLike, target: FormulaLike) extends Product with Serializable

    Permalink

    Implements the dual-rail transformation at clause level.

    Implements the dual-rail transformation at clause level. Does not split variables that are frozen in the source formula, and freezes them in the target formula.

  7. trait FormulaLike extends CnfLike with CircuitLike with PseudoBooleanLike with OptimizeLike

    Permalink

    Created by rdelmas on 21/06/16.

  8. case class IndepFromAllParentsOtherKids(nnf: Expr, circuit: FormulaLike, primaryEncoder: NNFToCircuitEncoder, witnessEncoder: WitnessEncoder, drFormula: FormulaLike, drEncoder: DualRailEncoder) extends Product with Serializable

    Permalink

    Adds new constraints to the dual-rail encoding for an optimization that is applied when a given gate g is such that: - the COI of g does not intersect the COI all of its parent's other kids

    Adds new constraints to the dual-rail encoding for an optimization that is applied when a given gate g is such that: - the COI of g does not intersect the COI all of its parent's other kids

    Under such conditions, the gate is part of a prime implicant iff when different from "?" some clause 'c' in the set of all clauses defining its parents gates is such that c - {g}, is false.

    Applied only on gates of the primary circuit.

  9. case class MonotonyOptimEncoder(nnf: Expr, circuit: FormulaLike, primaryEncoder: NNFToCircuitEncoder, witnessEncoder: WitnessEncoder, drFormula: FormulaLike, drEncoder: DualRailEncoder) extends Product with Serializable

    Permalink
  10. case class NNFAtomWitnessEncoder(nnf: Expr, keyAtom: Atom, primaryEncoder: NNFToCircuitEncoder, circuit: FormulaLike) extends (Expr) ⇒ Int with Product with Serializable

    Permalink

    Translates NNF expressions to witness circuit for keyAtom.

  11. case class NNFToCircuitEncoder(nnf: Expr, circuit: FormulaLike, switchableGates: Boolean) extends Product with Serializable

    Permalink

    Translator for a primary circuit.

    Translator for a primary circuit. If the switchableGates parameter is false, then atoms of the nnf formula are guaranteed to use the index range [1, nnf.atoms.size].

    nnf

    the nnf expression to translate

    circuit

    the target circuit in which to encode the formula

    switchableGates

    if set to true, all gates created in the circuit will be switchable

  12. trait OptimizeLike extends AnyRef

    Permalink

    An interface for building optimization problems on top of CNF formulas.

  13. case class PrimeImplicantGenerator(formula: Expr, filePrefix: String, maxOrder: Option[Int] = None, encodeForPrimer: Boolean = false, properTreeOpt: Boolean = false, monotonyOpt: Boolean = false) extends Product with Serializable

    Permalink

    This class takes a boolean formula as input, and outputs several files which which can be used for prime implicant enumeration.

  14. trait ProblemLike extends AnyRef

    Permalink
  15. class PropToNNF extends (Expr) ⇒ Expr

    Permalink

    Translation function from Prop to NNF.

    Translation function from Prop to NNF. Each instance of the class possesses its own translation cache.

  16. case class ProperTreeOptimEncoder(nnf: Expr, circuit: FormulaLike, primaryEncoder: NNFToCircuitEncoder, witnessEncoder: WitnessEncoder, drFormula: FormulaLike, drEncoder: DualRailEncoder) extends Product with Serializable

    Permalink

    Implements the optimisation applicable to gates for which all kids are independent and have a unique parent, ie applicable only to parts of the nnf formula that are genuine trees from the root and down to input literals.

    Implements the optimisation applicable to gates for which all kids are independent and have a unique parent, ie applicable only to parts of the nnf formula that are genuine trees from the root and down to input literals.

    This optim consists in forcing the maximum number of undefined kids for each possible output value of the gates

    For And(kids): - assert (o = 0) => nofKid(?) >= g.nofKids-1 - assert (o = ?) => nofKids(?) >= g.nofKids

    For Or(kids): - assert (o = 1) => nofKid(?) >= g.nofKids-1 - assert (o = ?) => nofKids(?) >= g.nofKids

    For Ite: - assert (o = 0) => optFalse,

    with: - define optFalse := And(optFalseFalse, optFalseTrue, optFalseUndef)

    with: - define optFalseFalse := (s = 0) => (t = ? and f = 0) - define optFalseTrue := (s = 1) => (t = 0 and f = ?) - define optFalseUndef := (s = ?) => (t = ? and f = ?)

    And - assert (o = 1) => optTrue

    with: - define optTrue := And( optTrueFalse, optTrueTrue, optTrueUndef )

    with: - define optTrueFalse := (s = 0) => (t = ? and f = 1) - define optTrueTrue := (s = 1) => (t = 1 and f = ?) - define optTrueUndef := (s = ?) => (t = 1 and f = 1)

    And - assert (o = ?) => optUndef

    with: - define optUndef := (t = ? and f = ?)

  17. trait PseudoBooleanLike extends AnyRef

    Permalink

    An interface for building pseudo-boolean problems on top of CNF formulas.

  18. abstract class Sat4JSolver extends SolverLike with ProblemLike

    Permalink

    A builder for dimacs models.

  19. trait SolverLike extends AnyRef

    Permalink

    A builder for dimacs models, returning a result of type R.

  20. case class SwitchEncoder(nnf: Expr, circuit: FormulaLike, drFormula: FormulaLike, drEncoder: DualRailEncoder) extends Product with Serializable

    Permalink

    Encodes switches definitions in the dual rail formula to enforce proper ternary valued models.

  21. case class WitnessEncoder(nnf: Expr, primaryEncoder: NNFToCircuitEncoder, circuit: FormulaLike) extends Product with Serializable

    Permalink

    Witness circuit translation function.

Value Members

  1. object CNF

    Permalink

    Propositional logic in conjunctive normal form.

  2. object Core

    Permalink

    Propositional logic solely with negation, conjunction, disjunction and if-then-else.

  3. object DualRailEncodingTests extends App

    Permalink

    Created by rdelmas on 26/06/16.

    Created by rdelmas on 26/06/16.

    Unit-tests of the dual rail enoding wrt the Ternary semantics of operators.

  4. object FormulaFileWriter

    Permalink

    A object for printing FormulaLike objects to dimacs, OPB, circuit and graphviz files.

  5. object NNF

    Permalink

    Propositional logic in negation-normal-form.

  6. object Prop

    Permalink

    Propositional logic.

  7. object PropToDualRailEncoder extends (Expr) ⇒ (FormulaLike, PartialFunction[Atom, (Int, Int)], PartialFunction[Expr, (Int, Int)])

    Permalink

    Created by rdelmas on 28/06/16.

  8. object PropToTernaryEncoder extends (Expr) ⇒ (FormulaLike, PartialFunction[Atom, (Int, Int)], PartialFunction[Expr, (Int, Int)])

    Permalink

    Created by rdelmas on 27/06/16.

    Created by rdelmas on 27/06/16.

    Encodes a Prop formula to a FormulaLike (CNF + Circuit) with the special dual-rail ternary logic encoding.

  9. object TernaryLogic

    Permalink

    Created by rdelmas on 26/06/16.

    Created by rdelmas on 26/06/16.

    Defines ternary semantics (true, false, X) for propositional operators and links with standard boolean semantics.

  10. object UnitProp

    Permalink

    Very naive implementation of a unit propagation routine only meant to test propagation properties of clausal encodings for small problems/operators.

    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.

  11. object foldHash

    Permalink

    A generic hashing function for lists of objects.

Ungrouped