Constructions.hpp File Reference

Plans for basic clause-set constructions. More...

Go to the source code of this file.

Detailed Description

Plans for basic clause-set constructions.

Representations of the basic logical operations
  • The problem is, given clause-sets F_1, F_2, find representations of F_1 and F_1, F_1 or F_2, not F_1, F_1 <-> F_2, F_1 -> F_2 and so on.
  • Here we consider F_1, F_2 as CNF --- in general we consider clause-sets as combinatorial objects, which can represent CNF *and* DNF, but here it seems helpful, since otherwise perhaps no good names are available?
  • F_1 and F_2 is the union of F_1, F_2; see "and_cs".
  • F_1 or F_2 is or_cs(F_1, F_2).
  • (CLS, and_cs, or_cs, {}, {{}}) is a commutative semiring with idempotent addition.
  • Perhaps these rules should better be represented by the operations.
  • In CLS as category, with morphisms complement-preserving homomorphisms for hypergraphs, it should and_cs be the coproduct, but or_cs doesn't look like a product. One could repair that by using as homomorphisms complement-preserving maps f: F -> G from literals to literals such that for C in F there exists D in G with D <= f(C) ?!
  • So perhaps we should use the names "coproduct_cs" and "product_cs" ?!
  • Negation
    1. "dual_cs" is the clause-set obtained by full distribution.
    2. Compare with ComputerAlgebra/Hypergraphs/Lisp/Transversals/plans/general.hpp.
    3. Compare with Algorithms/AllSolutions/plans/MinimalAssignments.hpp.
    4. A semantic negation G of a clause-set F is characterised by comp_cs(G) being a DNF-representation of F.
Gluing operations
  • Gluing: DONE
    1. DONE ("full_gluing") Given clause-sets F, G, use a new variable v, add v to all of F, add -v to all of G, and take the union.
    2. DONE ("partial_gluing") This is "full gluing", while for "partial gluing" v resp. -v is only added to some clauses of F resp. G (but in both cases to at least one clause).
    Since this is some "combinatorial operation", we could first compute n := max(n(F),n(G)), standardise the var-sets of F, G to {1,...,n}, and then use the new variable n+1.
  • Semantically this represents ( exists(v) : F or G).
  • DONE (we have vardisjoint_full_gluing) Often this operation needs variable-disjointness, so we need some operation to make F, G variable-disjoint.

Definition in file Constructions.hpp.