Satisfiability, coverage and learning of Boolean formulas in normal form
ABSTRACT
Conjunctive/disjunctive forms[CNF/DNF] can express any function, but
excessive length and non-unique representation are drawbacks compared
to circuits, BDDs. However satisfaction/refutation look simpler since
ONE clause, or All clauses are involved.
Algorithms to refute f [plus providing a counterexample] are fundamental
in formal verification of designs. Difficulties grow when the formula
size is near the "sharp threshold" on length(f), where the satisfying
set R(f) becomes empty "almost surely".
Physicists study the topology of this R, using spin glass analogies.
We concentrate on the size |R| as a function of length(f).
For clause size k growing slowly with n [number of variables], our
results give a rather full picture-relying on a "pseudo-random" structure
condition: two clauses have only few variables in common. It is
instructive to see how it implies uniqueness of representation and
also learning algorithms reconstructing THE clauses of f from random
examples.
Cases of fixed clause size [k>=3] are notorious for their
threshold-related difficulty, and many studies produced partial/heuristic
results. It becomes even worse for the size of R: even the case k=2 is open,
not clear if Fridgut technique helps. We give some results explaining
why this is so.