General plans for categories of clausesets.
More...
Go to the source code of this file.
Detailed Description
General plans for categories of clausesets.
 Todo:
 Relations to other modules
 Todo:
 Fundamental notions

Likely homomorphisms are special cases of substitutions; see "Applying substitutions" in ComputerAlgebra/Satisfiability/Lisp/Symmetries/plans/general.hpp.

A morphism f: F > G would then be a substitution which maps the literals from F to the literals from G, and which translates the clauses of F into the clauses of G.

Abbreviations like "morcls" (morphism for clausesets).

It seems that the morphism itself just maps literals to literals (or variables to variables in case of variablebased categories; see below), while the action on the clauses is just induced.

The two main conditions for clauses C are that f(C) equals a clause in the codomain, or, more generally, there exists a clause D in the codomain with D <= f(C).

We have variablebased and literalbased categories, which are concrete categories of the categories of varsets resp. litsets.

A varset is just a set, while a litset is a ZZ_2set.

A ZZ_2set is a pair [L,opr], according to ComputerAlgebra/Algebra/Lisp/Groupoids/Operations/plans/general.hpp, where opr(e,l) for e in {0,1} and l in L yields an element of L.

This uses ZZ_2 = cyclic_ugrp(2) (see ComputerAlgebra/Algebra/Lisp/Groupoids/Groups/CyclicGroups.mac), and so actually one can also use opr(e,l), where e is not just 0 or 1, but an arbitrary integer (interpreted as 0 or 1 iff its even or odd).

Could we also just use as set L of integers as a literal set, which is interpreted via 1*l = l ? Likely we should better employ a conversion function here.
 Todo:
 Categories of boolean functions

Variablebased: Objects are pairs [V,F], where V is a (finite) set of variables, while F: TASS(V) > {0,1}, where TASS(V) = {0,1}^V.

Literalbased: Objects are pairs [[L,opr], F], where [L,opr] is a literalsystem (see above), while F: TASS(L) > {0,1}, where TASS(L) is the set of maps f: L > {0,1} which preserve the ZZ_2operation (that is, we have ZZ_2morphisms).

Morphisms are maps alpha: V > V' resp. morphisms alpha: L > L':

Every total assignment f in the codomain is assigned a total assignment alpha(f) in the domain with alpha(f)(x) = f(alpha(x)).

We have two categories here, the "DNFform" and the "CNFform", where the CNFcondition is that always F(alpha(f)) >= F'(f) holds, while the DNFcondition is F(alpha(f)) <= F'(f).

Let's call the categories BDNF and BCNF.

Interpretation of clausesets as CNF's and DNF's:

From categories of clausesets we have the functors CNF resp. DNF to BCNF resp. BDNF, which assigns to every clauseset F its boolean function as CNF resp. DNF.

So for a clauseset F the two boolean functions DNF(F) and CNF(F) are dual to each other, that is, where the dual of a boolean function F is given by f > 1 + F(1+f) (where "+" here is xor).

On the morphisms the functors just act identical.

Canonical representations of boolean functions:

From BCNF to categories CLS (in their various forms) we have the functors A and P, which assign to the boolean function F the set of maximal resp. minimal implicates (w.r.t. subset inclusion; so the minimal implicates are the prime implicates); an "implicate" is a clause C such that F(f) = 1 implies f(C) = 1 (C as CNFclause).

And from BDNF to categories CLS (in their various forms) we have the functors A and P, which assign to the boolean function F the set of maximal resp. minimal implicants (w.r.t. subset inclusion; so the minimal implicants are the prime implicants); an "implicant" is a clause C such that f(C) = 1 (C as DNFclause) implies F(f) = 1.

We have an isomorphism D from BDNF to BCNF as well as from BCNF to BDNF given by forming the dual of boolean functions, where D: BDNF > BCNF can be obtained as the composition of first A and then CNF (or first P and then CNF).

Prime clausesets and dual prime clausesets:

Let Pr(F) for a clauseset F be the set of prime clauses. Now Pr is a functor from CLS to CLS (in its various forms), namely Pr is the composition of first the functor CNF and then the functor P, or, yielding the same result, first the functor DNF and then P.

Let Tr(F) for a clauseset F be the set of dual prime clauses. Tr needed to be a contravariant functor from CLS to CLS, as can be seen with {} > {{}}; however having only maps as morphisms, it seems impossible to have any nontrivial contravariant functor? So Tr doesn't seem to be a functor.

The point here is that Tr(F) needed to use the mapping from BNCF to CLS given by forming the prime DNF, which doesn't seem to be interpretable as functor(?). (Note that using D doesn't help, since D just equalises the two versions of P on BCNF and on BDNF.)

The intersection of BCNF and BDNF allows both forms of the Pfunctor:

We need to give them now different names: P_CNF and P_DNF.

Now also the map Tr: CLS > CLS (dual prime clauses, or "transversals") becomes a functor, but one needs to retrict the morphisms to, say, isomorphisms, so that the functor CNF (or DNF) becomes a functor to BCNF intersect BDNF.

But this likely only in the form of CLS with subsumption.
Definition in file general.hpp.