OKlibrary  0.2.1.6
RBases.hpp File Reference

Plans for removing redundancies from the set of prime implicates. More...

Go to the source code of this file.

## Detailed Description

Plans for removing redundancies from the set of prime implicates.

Todo:
Relations to other parts
Todo:
Organisation
• DONE The concept of r-bases can be applied to arbitrary clause-sets, not just to the set of all prime-clauses of some boolean function.
• DONE So likely this module should be moved from Lisp/Primality to module Lisp/Reductions.
• What remains there is the application to compute "interesting" subsets of the set of all prime-clauses.
Todo:
The notion of a base of a clause-set relative to some reduction
• Consider some reduction r (i.e., r: CLS -> CLS with r(F) satisfiability-equivalent to F).
• A sub-clause-set F' of a clause-set F is an "r-base of F" if for every clause D in F and for the corresponding partial assignment phi_D^0 the empty clause is element of r(phi_D^0 * F'), while this is not true for any strict subset of F'.
• That means that all missing clauses D can be derived from F' by means of r.
• Using additional assumptions for r one can derive more efficient algorithms.
• An "r-generating" clause-set drops the requirement that no clause can be removed.
• Both notions of generating clause-sets and base-clause-sets actually make sense regarding the relation between arbitrary clause-sets F and F' (F is r-generating resp. an r-base for F').
• As with Satisfiability/Reductions/Bases/RUcpGen.cpp, we need also the form of rbase_cl(F,red_) using some given stock F0 of clauses to be used.
Todo:
Considering special reductions
• There is exactly one r_0-base of every F, namely the result of subsumption elimination in F.
Todo:
Application to the representation of boolean functions
• If F is the set of prime implicates of some boolean function, which is too big to be included in some CNF-representation, then the hope is that r_1-bases or r_2-bases might be much smaller, while still having enough inference power.
• The reasoning is that if r is too strong (for example if r detects every unsatisfiability, then the bases of (any) F are exactly the irredundant cores) then we get smaller F', however we possibly gave up too much inference power, and SAT-solving might be much harder.
• The r_k-bases of such F are exactly the minimal (w.r.t subset-inclusion) r_k-based representation via CNFs not using additional variables (see "Investigating conditions and their representations" in Investigations/Cryptography/AdvancedEncryptionStandard/plans/general.hpp) of the underlying boolean function.
Todo:
Sampling of r-bases
• DONE (we have rand_rbase_cs in ComputerAlgebra/Satisfiability/Lisp/Reductions/RBases.mac) First we just need the natural randomised algorithm for producing some r-base.
1. We start with F' = F, while G = {} is the set of clauses which are necessary.
2. Choose C at random from F' - G, and let F'' := F' - {C}.
3. If for all D in F - F'' we have {} in r(phi_D * F''), then let F' := F'', and repeat with choosing another C.
4. Otherwise G := G + {C}, and another C is tried.
5. The algorithm stops once F' = G, and then F' is an r-basis of F.
• The remaining problem here is to precisely specify the random permutation.
1. See "Random r_1-bases" in Satisfiability/Reductions/Bases/plans/UcpBase.hpp.
Todo:
Computing minimum r-bases
• Searching for minimum bases (that is, of minimum size) might be very expensive, but, of course, should be implemented.

Definition in file RBases.hpp.