Utilities for dealing with CNF formulas

[jix]

Some methods to be implemented in and/or used from imctk inherently work with CNF representations. This might be of the full design or something auxiliary like an invariant, over/under-approximation of an invariant, tracking already covered or outstanding cases or something else entirely. Sometimes this might also be DNF, but since by de Morgan they're equivalent under negation, that makes little difference for generic utility code.

Important use cases for CNF include PDR and the invariants it produces as well as general interfacing with non-circuit SAT solvers.

Basic utilities should include:

• Efficiently storing CNF formulas without individual per-clause allocations
  • Efficiently detecting and avoiding duplicated clauses
• Optionally maintaining occurrence lists (allows looking up all clauses containing a variable/literal)
• Detecting and removing subsumed clauses, either online using maintained occurrence lists and/or as batch operation
• Parsing and writing of DIMACS CNF files (using my flussab-cnf crate)
• Converting bit-level IR into CNF

More involved are tools for extracting and recovering the dependency and/or circuit structure from a CNF formula. This is useful for moving back from CNF to the IR, but also a useful primitive to have while staying in the CNF representation.

This consists of:

• Recovering gates from the CNF by finding local functional dependencies (a variable fully defined by variables that are co-occuring in clauses)
• Recovering non-local functional dependencies using Padoa's Method (two copies of the CNF with assumptions on variables being equival or not equal)
• Reconstructing circuits from non-local functional dependencies
  • All functional dependencies would come with a subset of clauses. For local functional dependencies this can be just a sum-of-products or products-of-sum representation directly derived from the clauses involving either the positive or negative literal of the defined variable. Non-local functional dependencies, on the other hand, may be only known as a CNF using auxiliary variables that themselves are not fully defined by the fanin variables of the dependency, but taking two copies with the inputs tied together and outputs force to opposite values will result in an interpolant that gives a circuit corresponding to the functional dependency.
• Using known functional dependencies for finding a small set of "inputs" which together define all other variables, also known as a "independent support". This can also be with a subset of inputs already given and restricted to a subset of to-be-defined variables
  • See also https://github.com/meelgroup/arjun for an implementation and paper on this
  • The known functional dependencies can be represented as a set of Horn clauses
    • The variables in the Horn formula represent whether the value of a CNF variable has a fixed definition given other defined variables, but doesn't consider the value it takes
    • An independent support then is a subset of variables that imply all other variables
    • This is a reoccurring problem and there are various possible effort vs small/minimal/minimum trade-offs
      • This could be minimized with multiple SAT queries without explicitly representing the Horn formula, but in my tests working with Horn clauses as much as possible was quite a bit faster
      • Horn Formula Utilities #11 will provide ways to perform this minimization
• Extracting constraints from the CNF formula, minimizing included redundant constraints
  • After having selected inputs and a unique defining functional dependency for each variable (avoiding cycles), a) the CNF formula will usually have clauses left that are not part of the selected definitions and may restrict valid input values b) the defining clauses with positive and negative occurrences of the defined variable may over-constrain the defined variable, also restricting valid input values.
  • We can use a SAT solver to detect redundancies between these constraining clauses (relative to the selected defining clauses) with each such redundancy being a Horn clause
  • Finding a small set of constraining clauses that removes as many redundant clauses as possible is thus the same problem as we had in the previous point
    • Again, doable without the explicit Horn clause representation, but my guess is that it would help here too and we can use Horn Formula Utilities #11

[jix]

I have at least prototyped large parts of this, but some of it in a very quick and dirty way, so this will need quite a bit of cleanup before turning into a PR