Plans for basic clauseset constructions.
More...
Go to the source code of this file.
Detailed Description
Plans for basic clauseset constructions.
 Todo:
 Representations of the basic logical operations

The problem is, given clausesets 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 clausesets 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 complementpreserving 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 complementpreserving 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

"dual_cs" is the clauseset obtained by full distribution.

Compare with ComputerAlgebra/Hypergraphs/Lisp/Transversals/plans/general.hpp.

Compare with Algorithms/AllSolutions/plans/MinimalAssignments.hpp.

A semantic negation G of a clauseset F is characterised by comp_cs(G) being a DNFrepresentation of F.
 Todo:
 Gluing operations

Gluing: DONE

DONE ("full_gluing") Given clausesets F, G, use a new variable v, add v to all of F, add v to all of G, and take the union.

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 varsets 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 variabledisjointness, so we need some operation to make F, G variabledisjoint.
Definition in file Constructions.hpp.