On investigations into boolean function representations with different inference properties.
More...
Go to the source code of this file.
Detailed Description
On investigations into boolean function representations with different inference properties.
 Todo:
 Connections
 Todo:
 rbased clausesets

Let r be a reduction and F be an active clauseset.

F is called "rbased" if for a partial assignment phi such that phi * F is unsatisfiable we have that rreduction applied to F yields a contradiction.

Furthermore we speak of "properly rbased" if removal of a clause or removal of some literaloccurrence either creates a clauseset not equivalent to F or which is no longer rbased.

F is "rbased w.r.t. V" for some set V of variables, if F is rbased with respect to all partial assignments in V, and F is "totally rbased" if we can use V = var(F).

If nothing is said, then "totally" is always implied.

F is "strongly rbased" if F is rbased and for all partial assignments phi we have that the r(phi*F) has no forced assignments, that is, there is no variable v in var(F) and e in {0,1} such that <v > e> * phi*F is unsatisfiable.

Natural examples for r are r = r_k (k a natural number >= 0).

The weaker r the stronger is the representation (w.r.t. inference power).

The property of being (totally) (properly) rbased implicitly compares F with the underlying boolean function; we can also speak of an rbased representation of a boolean function.

If F is a CNFclauseset, then being r_0based is equivalent to F containing all prime implicates of C, while being properly r_0based is equivalent to being maximally prime (consisting exactly of the set of all primeCNFclauses).

See "The notion of a base of a clauseset relative to some reduction" in ComputerAlgebra/Satisfiability/Lisp/Reductions/plans/RBases.hpp for the case where no additional variables are considered:

We make the natural assumption that if F' is a strengthening of F, i.e., adding clauses and/or shortening clauses, then {} in r(F) implies {} in r(F').

That F (totally) properly rbased is now equivalent to F being an rbase of the set of primeCNFclauses of F.

The function rand_rbase_cs(F,r) in ComputerAlgebra/Satisfiability/Lisp/Reductions/RBases.mac randomly computes an rbase of F.
 Todo:
 Positive representations

Defining a positive representation

Consider a boolean condition C on variables V (that is, C(f) is a boolean value for total assignments f, and C depends only on V).

A "positive representation" R of C is an active clauseset on variables V' >= V such that if R(f) is true then also C(f) is true, and for f such that C(f) is true there is a unique f' which differs from f only on V'  V such that C'(f) is true.

Perhaps this should better be called a "unique positive
representation", while in general we demand only the existence of some f'. This is equivalently to saying that the projection of the satisfying assignments for R to V yield exactly the satisfying assignments for C.

rbased positive representations

See "rbased representations" above.

In general, if we say a positive representation R of a condition C is rbased, then R is rbased w.r.t. V (where V is the underlying set of original variables, while the representation uses V' >= V).

If R is rbased with respect to V', then we make this explicit by calling R "totally rbased".

Note that, in general, we do not consider the effect of assignments to variables in V'  V. It seems sensible to me (OK) to consider this as the basis, but for further refinements considerations of V'  V might be needed.

Another sensible condition here is for satisfying f for C(f) how difficult it is to compute the extension f'. For example one could demand that the additional assignments follow by unitclause propagation.
Definition in file ReductionBasedRepresentations.hpp.