feat: detect and special case XORs when lowering AIG to CNF#13946
Open
georgerennie wants to merge 4 commits into
Open
feat: detect and special case XORs when lowering AIG to CNF#13946georgerennie wants to merge 4 commits into
georgerennie wants to merge 4 commits into
Conversation
This PR adds detection and optimized lowering of XOR/XNOR gates to `bv_decide`'s AIG to CNF lowering. This adds a function `Std.Sat.AIG.detectXOR` that detects XOR gates of the form `¬(a ∧ b) ∧ ¬(¬a ∧ ¬b)` up to permutation of inputs and negation of inputs/output. When the CNF lowering lowers a gate, it first uses `detectXor` to see if it can be lowered as an XOR, and if so uses a 4 clause description instead of the 12 used by lowering as AND gates.
georgerennie
commented
Jun 3, 2026
| @[expose] public section | ||
|
|
||
| /-! | ||
| This module contains functions to detect compound logic gates represented by sub-graphs of the `AIG`. |
Contributor
Author
There was a problem hiding this comment.
Wasn't sure whether this should really be its own file but it felt like something that might be useful for other optimizations. Subsequently we can add the same for ITE detection here.
Contributor
Author
|
changelog-tactics |
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds detection and optimized lowering of XOR/XNOR gates to
bv_decide's AIG to CNF lowering. It adds a functionStd.Sat.AIG.detectXORthat detects XOR gates of the form¬(a ∧ b) ∧ ¬(¬a ∧ ¬b)up to permutation of inputs and negation of inputs/output. When the CNF lowering lowers a gate, it first usesdetectXorto see if it can be lowered as an XOR, and if so uses a 4 clause encoding instead of the 12 used by lowering as AND gates.