OKlibrary  0.2.1.6
ReductionBasedRepresentations.hpp File Reference

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:
r-based clause-sets
• Let r be a reduction and F be an active clause-set.
• F is called "r-based" if for a partial assignment phi such that phi * F is unsatisfiable we have that r-reduction applied to F yields a contradiction.
• Furthermore we speak of "properly r-based" if removal of a clause or removal of some literal-occurrence either creates a clause-set not equivalent to F or which is no longer r-based.
• F is "r-based w.r.t. V" for some set V of variables, if F is r-based with respect to all partial assignments in V, and F is "totally r-based" if we can use V = var(F).
• If nothing is said, then "totally" is always implied.
• F is "strongly r-based" if F is r-based 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) r-based implicitly compares F with the underlying boolean function; we can also speak of an r-based representation of a boolean function.
• If F is a CNF-clause-set, then being r_0-based is equivalent to F containing all prime implicates of C, while being properly r_0-based is equivalent to being maximally prime (consisting exactly of the set of all prime-CNF-clauses).
• See "The notion of a base of a clause-set relative to some reduction" in ComputerAlgebra/Satisfiability/Lisp/Reductions/plans/RBases.hpp for the case where no additional variables are considered:
1. 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').
2. That F (totally) properly r-based is now equivalent to F being an r-base of the set of prime-CNF-clauses of F.
• The function rand_rbase_cs(F,r) in ComputerAlgebra/Satisfiability/Lisp/Reductions/RBases.mac randomly computes an r-base of F.
Todo:
Positive representations
• Defining a positive representation
1. 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).
2. A "positive representation" R of C is an active clause-set 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.
3. 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.
• r-based positive representations
1. See "r-based representations" above.
2. In general, if we say a positive representation R of a condition C is r-based, then R is r-based w.r.t. V (where V is the underlying set of original variables, while the representation uses V' >= V).
3. If R is r-based with respect to V', then we make this explicit by calling R "totally r-based".
4. 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.
5. 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 unit-clause propagation.

Definition in file ReductionBasedRepresentations.hpp.