Plans for Maximacomponents regarding computation of prime implicates/implicants of boolean functions and clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans for Maximacomponents regarding computation of prime implicates/implicants of boolean functions and clausesets.
 Todo:
 Tests

Add tests for all functions, including

all_minequiv_bvs_rsubhg

all_minequiv_bvsr_cs

all_minequiv_bvsr_sub_cs
 Todo:
 Organisation

DONE (to be moved to ComputerAlgebra/Satisfiability/Lisp/Primality/plans/general.hpp) The resolutionmodule doesn't seem to be the right place.

DONE Perhaps we create a whole new module.

The basic tasks for a given *clauseset* to compute "prime clauses" and "dual prime clauses".

For a boolean function this means that the prime implicates and prime implicants are to be computed.

DONE We have this basic terminology problem:

Coming from boolean functions, an absolute point of view is taken, where implicates belong to the "false" side, and "implicants" to the "true" side.

The other point of view (as taken above with "prime clauses" etc.) is relative: Within the given representation (CNF or DNF based) either stay with the representation and minimise the clauses (given a CNF, this would mean the prime implicates), or "go to the other side" (for a CNF this means prime implicants).

So we use "prime clauses" and "dual prime clauses" for the relative point of view, and "prime implicates" resp. "prime implicants" for the absolute point of view.

See "Dualisation" below.

See "Connections" below.

We need generic testfunctions "okltest_prime_clauses_cs", "okltest_dual_prime_clauses_cs" and the special cases "okltest_prime_clauses_full_cs", "okltest_dual_prime_clauses_full_cs" (since there are many algorithms for computing these fundamental functions).
 Todo:
 Best method for prime_clauses_cs

hardness_cs uses min_resolution_closure_cs(F)[1], which for okltest_hardness_cs is actually better than the current prime_clauses_cs(F) = min_extdp_prod_cs(F). Is this coincidence, or is there a deeper reason?

See "Improving min_extdp_cs" below.

See "Fast computation of prime implicates/implicants" in Experimentation/Investigations/BooleanFunctions/plans/general.hpp for the investigation.
 Todo:
 Improving min_extdp_cs

A first reasonable heuristics seems min_extdp_prod_cs  is it really reasonable?

Can we improve the subsumptionelimination in an elegant way?
 Todo:
 min_2resolution_closure_cs

Currently the name likely is not corrected, since if the input is not a full clauseset, then likely we do not compute the minclosure under 2subsumption resolution (example?).

What is the complexity of min_2resolution_closure_cs(F) ?

If we take the input size as 2^n, then the procedure is trivially polynomial (altogether there are at most 3^n clauses). But the question is whether the running time is polynomial in the real input, that is, in F ?!

We need to count the total number of clauses created.

This is exactly the number of clauses which follow from F (over the same variables; no need to distinguish between the old clauses in F and the new created ones, but just altogether is counted).

If F has 2^n clauses, then altogether 3^n clauses are created, where (2^n)^(log_2(3)) = 3^n.

So one could conjecture that the total number of clauses which follow from a full clauseset F (over the same variables, of course) is at most c(F)^(log_2(3)).

In "Computations of all prime clauses for full clausesets" in Satisfiability/Lisp/Primality/plans/general.hpp it is shown that that number is at most 1/2 c(F)^2 + 1/2 c(F).

Hashing:

Efficient implementations of min_2resolution_closure_cs rely on efficient hashing schemes for clauses.

In Satisfiability/FiniteFunctions/QuineMcCluskey.hpp a "total" hashing scheme is used, that is, simply a boolean array of length 3^n is used, with the bijection from clauses with n variables to {0,...,3^n1} as indexing (hashing) scheme.

This should be efficient for dense clausesets, but it is very inefficient for sparse clausesets (and somewhat larger n).

Alternative hashing schemes need to be developed.
 Todo:
 Dualisation

Implement the algorithm given by "dual_cs" in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac

That is, just subsumption elimination needs to be added.

How to do this in a better way? For example doing subsumption elimination inbetween?

DONE Or should this go somewhere else??

DONE Should we perhaps have modules "PrimeClauses" and "DualPrimeClauses" ? Or one module "Primality" (which contains those two)?
 Todo:
 Connections
 Todo:
 Hitting clausesets

The input of Quine/McCluskey is a (special) hitting clauseset (namely a full clauseset)  can we somehow generalise the algorithm to work with arbitrary hitting clausesets?

Given a hitting clauseset F, we can easily compute for each clause C in F a prime implicate C' <= C of F, by greedily removing literals from C and checking whether still F implies C' holds.

Achieved by "replace_by_prime_implicates_hitting".

Can all prime implicates of F be obtained in this way (for fixed F)? Likely not (examples?).

Likely there can be exponentially many prime implicates C' <= C ?

And likely it is hard to find some C' of minimal length?

Once we know phi_C' * F is unsatisfiable, it should be possible to read off directly from this computation which literals from C' can be further dropped.

In this way we obtain F' <= F consisting of some prime implicates of F such that F' is equivalent to F. By removing redundant clauses from F' we can further go into the direction of a shortest CNF representation of the underlying boolean function.

Since SAT solvers can be used to obtain F, in this way we can harness the power of SAT solvers (w.r.t. computing small splitting trees) for computing small CNF/DNF representations.

It should be possible to compute with polynomial delay all prime implicates which are subsuming some clause from F. See "contained_prime_implicate" below.
 Todo:
 contained_prime_implicate

Write the more general function "all_contained_prime_implicates", which returns the set of all prime implicates contained in S (so now we also allow that C doesn't follow from F, which holds iff the returned clauseset is empty).

For a recursive solution the problem is to avoid overlaps.
Definition in file PrimeImplicatesImplicants.hpp.