OKlibrary  0.2.1.6
NonBoolean.hpp File Reference

Plans for Maxima-components regarding generalised clause-sets. More...

Go to the source code of this file.

## Detailed Description

Plans for Maxima-components regarding generalised clause-sets.

Todo:
Notions for generalised literals
• Compare "Better general naming conventions" in ComputerAlgebra/Satisfiability/Lisp/plans/general.hpp.
• We have the "non-boolean" versions of literals, where literals are pairs [v,e], with e a value.
• And there are "power" versions, where then e is a set of values.
• The "monosigned literals" resp. "signed literals" are corresponding triples, with the third component in {-1,+1}.
• One could instead use terms "nb(v,e), nb(v,e,s), pl(v,e), pl(v,e,s)".
• A problem with non-boolean variables is, where to put the information about the domain of the variables:
1. See the discussions in ComputerAlgebra/Satisfiability/Lisp/plans/SatisfactionProblems.hpp.
2. Perhaps it's not part of clause-sets etc., but only part of "problems" given for example to SAT-solvers.
3. So a signed clause-set etc. would always need to be accompanied by either a uniform domain, or by a domain function.
4. But perhaps we should use pairs [FF, D], where D is a set, list or map. Perhaps the default for all types of clause-sets is a uniform domain. Actually, likely better to use triples [FF[1],FF[2],D].
5. But since we can also use sensibly non-boolean clause-sets without the domain information (for example it is not needed in order to apply a partial assignment), we should use the (additional) suffix "ud" for uniform domain and "fd" for function domain.
6. There is also the idea that a "domain association" is basically a partial assignment; actually it should be a "total partial assignment".
7. One could allow then suffixes like "tpa_mp".

Definition in file NonBoolean.hpp.