Plans for Maximacomponents regarding generalised clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans for Maximacomponents regarding generalised clausesets.
 Todo:
 Notions for generalised literals

Compare "Better general naming conventions" in ComputerAlgebra/Satisfiability/Lisp/plans/general.hpp.

We have the "nonboolean" 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 nonboolean variables is, where to put the information about the domain of the variables:

See the discussions in ComputerAlgebra/Satisfiability/Lisp/plans/SatisfactionProblems.hpp.

Perhaps it's not part of clausesets etc., but only part of "problems" given for example to SATsolvers.

So a signed clauseset etc. would always need to be accompanied by either a uniform domain, or by a domain function.

But perhaps we should use pairs [FF, D], where D is a set, list or map. Perhaps the default for all types of clausesets is a uniform domain. Actually, likely better to use triples [FF[1],FF[2],D].

But since we can also use sensibly nonboolean clausesets 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.

There is also the idea that a "domain association" is basically a partial assignment; actually it should be a "total partial assignment".

One could allow then suffixes like "tpa_mp".
Definition in file NonBoolean.hpp.