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.