  Invariant inference algorithms such as interpolation-based inference and
IC3/PDR show that it is feasible, in practice, to find inductive invariants for
many interesting systems, but non-trivial upper bounds on the computational
complexity of such algorithms are scarce, and limited to simple syntactic forms
of invariants. In this paper we achieve invariant inference algorithms, in the
domain of propositional transition systems, with provable upper bounds on the
number of SAT calls. We do this by building on the monotone theory, developed
by Bshouty for exact learning Boolean formulas. We prove results for two
invariant inference frameworks: (i) model-based interpolation, where we show an
algorithm that, under certain conditions about reachability, efficiently infers
invariants when they have both short CNF and DNF representations (transcending
previous results about monotone invariants); and (ii) abstract interpretation
in a domain based on the monotone theory that was previously studied in
relation to property-directed reachability, where we propose an efficient
implementation of the best abstract transformer, leading to overall complexity
bounds on the number of SAT calls. These results build on a novel procedure for
computing least monotone overapproximations.
