Renaming map from source to target variables Entries are of the form:
Renaming map from source to target variables Entries are of the form:
If l is a free (ie. non-gate) literal of the source formula:
l -> x_{l}
Where: - l is a free of the source formula (either p or -p) - x_{l} is the renamed literal corresponding to l (either x_{p} or x_{-p})
Translates source and adds a cardinality constraint on the number of positive positive free variables.
Translates source and adds a cardinality constraint on the number of positive positive free variables.
A backtranslator instance for translating models of target to prime implicants of source.
Translates source and adds a minimization criterion over positive free variables.
Translates source and adds a minimization criterion over positive free variables.
A backtranslator instance for translating models of target to prime implicants of source.
Translates source clauses to target clauses using the renaming algorithm.
Translates source clauses to target clauses using the renaming algorithm.
A backtranslator instance for translating models of target to prime implicants of source.
An iterator on variables that correspond to variables that were free in source instance.
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.