search

ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
63 stars 15 forks source link

suggestion: add some AIG magic #12

Closed jwaldmann closed 8 years ago

jwaldmann commented 9 years ago

What is the reasoning behind the rewrite rules in instance Boolean Bit (in Ersatz.Bit)? Besides semantical correctness, I mean.

Can we perhaps do better by using AIG?

Basically, reduce the set of constructors of data Bit, and simplify (cf. http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf) before Tseitin transform (in runBit)?

Looks like a nice student project.

ekmett commented 9 years ago

Basically we distinguish between Literals and Bits. Literals are actual honest to god bits we send to the SAT solver, but we try to avoid exploding that set as much as possible, by doing some basic constant folding.

I had the nodes in there way back in the dawn of time because I was interested in one of the non-prenex QBF solving strategies and for that I wanted to keep them.

But, we could definitely do a smarter cleanup by using pretty much anything from the literature.

jwaldmann commented 8 years ago

I noticed that my commit that was referenced above, is gone. Here's a copy: https://github.com/jwaldmann/ersatz/commit/f60ed52a92a2daf1a9f1af291f522d318a000ae3

ekmett commented 8 years ago

Merged and removed Or entirely as a signal of intent. I haven't checked the build though.