Plans for translations from nonboolean clausesets to boolean clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans for translations from nonboolean clausesets to boolean clausesets.
 Todo:
 Connections to other modules
 Todo:
 Add standardised translations

Standardised translations from nonboolean to boolean clausesets/lists should be implemented.

For translations from nonboolean formal clauselists, 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.
 Todo:
 Generalised canonical translation

See Satisfiability/Lisp/FiniteFunctions/plans/TseitinTranslation.hpp for the boolean case.

Consider a generalised DNF clausesets 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".
 Todo:
 DONE Translating nonboolean clausesets into boolean clausesets

DONE Write nbfcsfd2fcs_alo(FF) and nbfcsfd2fcs_aloamo(FF), translating nonboolean clausesets into boolean clausesets by using new boolean variables nbv(v,e) for old variables v and values e, adding in the first case only atleastoneclauses for each v, and in the second case also adding the atmostoneclauses.
 Todo:
 DONE Add translations for nonboolean clauselists with uniform domain

See ComputerAlgebra/RamseyTheory/Lisp/RamseyProblems.mac and ramsey_nbfclud for possible use.
Definition in file NonBooleanTranslations.hpp.