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.

Relations to other parts
  • 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.
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.
Considering special reductions
  • There is exactly one r_0-base of every F, namely the result of subsumption elimination in F.
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.
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.
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.