Horn Formula Utilities

[jix]

Horn Formulas are a useful special case of CNF formulas, with various potential use cases in imctk.

Horn clauses can model:

• Implication / justification graphs
• Monotone circuits
  • Including fixpoints of monotone cyclic circuits

Whereas solving CNF requires unit propagation, making decisions (guesses) and backtracking in case of incorrect decisions (potentially with learning new clauses), for Horn formulas unit propagation alone is sufficient.

In a model checking context given a set of properties it can be useful to consider a variant where there's a pair of variables x, x' for each property x representing the property holding up to the past or current frame respectively. Here each Horn clause represents a (conditional) proof or (relative) induction step. (Not sure if there is an established name, I'm calling this temporal Horn clauses for now.) Given a set of assumption, using a variant of unit propagation, it's possible to compute lower bounds indicating the number of frames for which a property must hold given the known facts represented as Horn clauses. For properties that are mutually inductive this will produce an infinite bound.

This has some useful applications for PDR/IC3 in an incremental / multi-property setting, both for detecting proofs of individual properties before PDR converges as a whole as well as to allow re-use of already derived information even across PDR invocations with different combinational assumptions that are not folded into the target property.

Overall this would consist of:

• similar basic utilities as for CNF (Utilities for dealing with CNF formulas #9)
• unit propagation with a stack of assumption that can be pushed and popped
  • implemented like decisions and backtracking in CDCL sat solvers, but without learning
• minimization of unsatisfiable (or equivalently justifying) assumptions
  • some of preliminary experiments seem to indicate that some minimization problems (some examples in Utilities for dealing with CNF formulas #9) can be sped up quite a bit by expressing them as this problem on Horn formulas, potentially including some refinement steps that incrementally add Horn clauses in case the full problem can't be efficiently expressed as a Horn formula
    • this seems to be the case for computing minimal justifications
    • my guess is that might be true even more so for computing or approximating minimum justifications
• unit propagation of temporal bounds with fixpoint detection to compute a maximal mutually inductive subset of properties
  • most likely completely separate from the non-temporal unit propagation implementation, it's very similar on a high level, but the low level details differ enough that an attempt to unify them would only make things harder to implement and understand