Optimizing DNF/CNF forms

[seanbaxter]

I wrote a C++ compiler and am implementing partial ordering of constraints, which is part of C++20 concepts. Unlike anything else in the compiler frontend, this involves formal logic, which I have no experience with.

http://eel.is/c++draft/temp.constr

Constraints are recursively broken apart into atoms. Conjunction and disjunction are the only operators supported, not negation, thankfully. I have a binary tree where terminals are atoms and interior nodes are || and && operations. Spooling this into CNF or DNF can generate pretty big normal forms. I was pointed to z3 and am wondering if there's a way to either lower a tree like I described to simplified CNF/DNF, or to take CNF/DNF and simplify that.

I'd need to use the C or C++ interfaces. My atoms are identified with integers. If there's a better subsumes test than the one I pasted, I could also use that, although the test if one atom subsumes another is very involved and I'd need a callback into the C++ frontend.

Is z3 suited for this?

[aytey]

I think this subsumption is direct implication, right? A set of clauses A subsumbes a set of clauses B iff B is always logically entailed by A (however, because things in Z3 are implicitly existentially quantified, you probably want something like B -> ¬A is UNSAT).

If so, sure, Z3 would work for this. Z3 has a way to get it give you the CNF after reduction (as long as you don't need the theory solver, which would require "iteration"; i.e., your formula can be solved eagerly). However, if you're directly targetting Z3 as a way to solve formulae, do you care about getting the CNF? Would it be enough for you if Z3 could tell you "yes, A is subsumed by B"?

[seanbaxter]

I think I would need to cache the simplified CNF and DNF. The first time partial ordering is executed on a template, I do the constraint substitutions and generate the normal forms. This is costly. Then I do the subsumption test against the normal form of other candidate templates. This may be done hundreds of times, so amortizing the normal form construction is important.

I think using z3_simplify may help a good deal. I'd be more comfortable incorporating that into my program because I could at least examine what it returns and be confident that I understand its behavior.

Is there an example of using z3_simplify to optimize either ASTs or normal forms and getting normal forms back?

[aytey]

Yeah, I'm never sure when and where calling the simplifier directly "makes sense" (in our industrial use of Z3, we never call simplify directly, but leave that up to solve to do).

As an example:

import z3

a = z3.Bool("a")
b = z3.Bool("b")
c = z3.Bool("c")

expr = z3.And(z3.Or(a, b), z3.Or(a, c), a)

print(z3.simplify(expr))

# EOF

This does not simplify expr at all, although the obvious simplification is to rewrite the whole thing to be a.

Anyway, could incremental solving and substitution work for you? For example:

import z3

# Need a solver, obviously ...
s = z3.Solver()

# What are the "propositions" in our constraints
a = z3.Bool("a")
b = z3.Bool("b")
c = z3.Bool("c")

# Build up the propositional skeleton
expr = z3.And(z3.Or(a, b), z3.Or(a, c), a)

# Add our propositional skeleton
s.add(expr)

# If this isn't satisfiable, we have a problem
assert s.check() == z3.sat

# Concrete substitutions
x = z3.BitVec("x", 32)
y = z3.BitVec("y", 32)

# So we now want to instantiate our (satisfiable) propositional skeleton with
# some "real" stuff
new_a = x > y
new_b = x + 1 > y
new_c = y > 10

# Build-up our new expression
new_expr = z3.substitute(expr, [(a, new_a), (b, new_b), (c, new_c)])

# Use incremental solving
s.push()

# Add our new expression
s.add(new_expr)

# This may or may not be satisfiable, and that's what we're trying to find out
print(s.check())

# Pop the solver so we're ready to check the next instance
s.pop()

# EOF

This would allow you parse and build-up the "propositional skeleton" of your constraint once (and check that some concrete instance would allow it to hold; to avoid having "impossible" constraints). Next, when you come to a specific instance (e.g., in a template instantiation), you can "substitute" your propositional terms for the concrete ones that come from that specific instance. If you use incremental solving here, you don't have to check the propositional skeleton multiple times, you can just do a pop after checking the newly-found concrete instance.

This avoids you parsing/building-up the expression twice, and it also means that you "don't have to care" about how something like Z3 reasons about the formula (you don't need to call simplify or get the CNF yourself), you just need to care about "is this satisfiable or not?".

[seanbaxter]

Thanks for super detailed reply. I'll keep coming back to this as I move forward.