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.