OKlibrary  0.2.1.6
general.hpp File Reference

General plans for categories of clause-sets. More...

Go to the source code of this file.


Detailed Description

General plans for categories of clause-sets.

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.
    1. Abbreviations like "morcls" (morphism for clause-sets).
    2. It seems that the morphism itself just maps literals to literals (or variables to variables in case of variable-based categories; see below), while the action on the clauses is just induced.
    3. 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 variable-based and literal-based categories, which are concrete categories of the categories of var-sets resp. lit-sets.
    1. A var-set is just a set, while a lit-set is a ZZ_2-set.
    2. A ZZ_2-set 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.
    3. 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).
    4. 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
  • Variable-based: 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.
  • Literal-based: Objects are pairs [[L,opr], F], where [L,opr] is a literal-system (see above), while F: TASS(L) -> {0,1}, where TASS(L) is the set of maps f: L -> {0,1} which preserve the ZZ_2-operation (that is, we have ZZ_2-morphisms).
  • Morphisms are maps alpha: V -> V' resp. morphisms alpha: L -> L':
    1. Every total assignment f in the codomain is assigned a total assignment alpha(f) in the domain with alpha(f)(x) = f(alpha(x)).
    2. We have two categories here, the "DNF-form" and the "CNF-form", where the CNF-condition is that always F(alpha(f)) >= F'(f) holds, while the DNF-condition is F(alpha(f)) <= F'(f).
  • Let's call the categories BDNF and BCNF.
  • Interpretation of clause-sets as CNF's and DNF's:
    1. From categories of clause-sets we have the functors CNF resp. DNF to BCNF resp. BDNF, which assigns to every clause-set F its boolean function as CNF resp. DNF.
    2. So for a clause-set 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).
    3. On the morphisms the functors just act identical.
  • Canonical representations of boolean functions:
    1. 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 CNF-clause).
    2. 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 DNF-clause) 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 clause-sets and dual prime clause-sets:
    1. Let Pr(F) for a clause-set 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.
    2. Let Tr(F) for a clause-set 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 non-trivial contravariant functor? So Tr doesn't seem to be a functor.
    3. 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 P-functor:
    1. We need to give them now different names: P_CNF and P_DNF.
    2. 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.
    3. But this likely only in the form of CLS with subsumption.

Definition in file general.hpp.