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.
A back translator from models of the target formula to prime implicants of the source formula.
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.
An interface for building circuit-like formulas on top of CNF formulas.
An interface for building formulas in conjunctive normal form.
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.
Created by rdelmas on 21/06/16.
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.
Translates NNF expressions to witness circuit for keyAtom.
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].
the nnf expression to translate
the target circuit in which to encode the formula
if set to true, all gates created in the circuit will be switchable
An interface for building optimization problems on top of CNF formulas.
This class takes a boolean formula as input, and outputs several files which which can be used for prime implicant enumeration.
Translation function from Prop to NNF.
Translation function from Prop to NNF. Each instance of the class possesses its own translation cache.
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 = ?)
An interface for building pseudo-boolean problems on top of CNF formulas.
A builder for dimacs models.
A builder for dimacs models, returning a result of type R.
Encodes switches definitions in the dual rail formula to enforce proper ternary valued models.
Witness circuit translation function.
Propositional logic in conjunctive normal form.
Propositional logic solely with negation, conjunction, disjunction and if-then-else.
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.
A object for printing FormulaLike objects to dimacs, OPB, circuit and graphviz files.
Propositional logic in negation-normal-form.
Propositional logic.
Created by rdelmas on 28/06/16.
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.
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.
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.
A generic hashing function for lists of objects.
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).