BCP solver #7747
brouhaha
started this conversation in
Show and tell
BCP solver
#7747
Replies: 1 comment 1 reply
-
|
There are a number of references to this with different techniques applied, but yes, it is basically maxsat so it depends if the maxsat algorithms in z3 are suitable. |
Beta Was this translation helpful? Give feedback.
1 reply
-
|
It works fine for the test cases I've tried, but those are all fairly small. Unfortunately I don't have any large test cases with known results for comparison. |
Beta Was this translation helpful? Give feedback.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
-
Recently I spent some time trying to write my own Binate Cover Problem solver. BCP is a superset of the Unate Cover Problem, and is commonly used in logic synthesis. Anyhow, I haven't yet got my from-scratch BCP solver working, but today I realized that Z3 should be able to solve BCP problems, and it's likely to do it far faster than anything I might throw together. (BCP is an NP-Hard problem.)
I may have reinvented the wheel, or it may be that few people need this, but I published my simple implementations in Python and C++.
Beta Was this translation helpful? Give feedback.
All reactions