NonBooleanTranslations.hpp File Reference

Plans for translations from non-boolean clause-sets to boolean clause-sets. More...

Go to the source code of this file.

Detailed Description

Plans for translations from non-boolean clause-sets to boolean clause-sets.

Connections to other modules
Add standardised translations
  • Standardised translations from non-boolean to boolean clause-sets/lists should be implemented.
  • For translations from non-boolean formal clause-lists, it seems natural to take the ordering given by the variable list, and the ordering given by the domain and then define the new ordering on the domain lexicographically based first on the variable ordering and then on the domain.
  • Such a (variable,domain) lexicographical ordering would allow additional variables to be added to the problem at the end of the variable ordering without requiring renumbering.
  • Perhaps two versions could be supplied, with one ordering first by variable then domain, and then vice versa (then allowing the domain to be easily extended)?
  • See ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/RamseyProblems.mac for an example of use.
Generalised canonical translation
  • See Satisfiability/Lisp/FiniteFunctions/plans/TseitinTranslation.hpp for the boolean case.
  • Consider a generalised DNF clause-sets F (i.e., with literals "variable = value").
  • The natural generalisation of the canonical translation has new variables for all clauses C of F, set to be equivalent to DNF({C}).
  • This naturally needs the direct encoding, using one boolean variable for the literal "variable = value".
DONE Translating non-boolean clause-sets into boolean clause-sets
  • DONE Write nbfcsfd2fcs_alo(FF) and nbfcsfd2fcs_aloamo(FF), translating non-boolean clause-sets into boolean clause-sets by using new boolean variables nbv(v,e) for old variables v and values e, adding in the first case only at-least-one-clauses for each v, and in the second case also adding the at-most-one-clauses.
DONE Add translations for non-boolean clause-lists with uniform domain
  • See ComputerAlgebra/RamseyTheory/Lisp/RamseyProblems.mac and ramsey_nbfclud for possible use.

Definition in file NonBooleanTranslations.hpp.