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 rbases can be applied to arbitrary clausesets, not just to the set of all primeclauses 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 primeclauses.
 Todo:
 The notion of a base of a clauseset relative to some reduction

Consider some reduction r (i.e., r: CLS > CLS with r(F) satisfiabilityequivalent to F).

A subclauseset F' of a clauseset F is an "rbase 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 "rgenerating" clauseset drops the requirement that no clause can be removed.

Both notions of generating clausesets and baseclausesets actually make sense regarding the relation between arbitrary clausesets F and F' (F is rgenerating resp. an rbase 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_0base 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 CNFrepresentation, then the hope is that r_1bases or r_2bases 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 SATsolving might be much harder.

The r_kbases of such F are exactly the minimal (w.r.t subsetinclusion) r_kbased 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 rbases

DONE (we have rand_rbase_cs in ComputerAlgebra/Satisfiability/Lisp/Reductions/RBases.mac) First we just need the natural randomised algorithm for producing some rbase.

We start with F' = F, while G = {} is the set of clauses which are necessary.

Choose C at random from F'  G, and let F'' := F'  {C}.

If for all D in F  F'' we have {} in r(phi_D * F''), then let F' := F'', and repeat with choosing another C.

Otherwise G := G + {C}, and another C is tried.

The algorithm stops once F' = G, and then F' is an rbasis of F.

The remaining problem here is to precisely specify the random permutation.

See "Random r_1bases" in Satisfiability/Reductions/Bases/plans/UcpBase.hpp.
 Todo:
 Computing minimum rbases

Searching for minimum bases (that is, of minimum size) might be very expensive, but, of course, should be implemented.
Definition in file RBases.hpp.