pysat icon indicating copy to clipboard operation
pysat copied to clipboard

Published 20 hours ago • verified publisher icon pysathq

formula simplication

Open yxliang01 opened this issue 4 years ago • 4 comments

Would be great if pysat supports CNF formula simplification :)

Thanks

yxliang01 avatar Nov 12 '19 09:11 yxliang01

Hi @yxliang01, I agree that it would be great. This feature would help a lot in many use cases. Therefore, PRs are welcome! :) Otherwise, I will take a look into this only when I have time. :)

alexeyignatiev avatar Nov 13 '19 16:11 alexeyignatiev

@alexeyignatiev Yup! It definitely be very useful. However, I also can't allocate time for this recently... You have an estimate for this? It would be super helpful for my research projects if this is implemented! :) (PySat already facilitated my project, thanks for that)

yxliang01 avatar Nov 13 '19 16:11 yxliang01

Unfortunately, I cannot estimate when this could be done. BTW, what kind of simplification do you mean? Two-level minimization or formula preprocessing?

alexeyignatiev avatar Nov 13 '19 17:11 alexeyignatiev

I meant simply formula preprocessing. E.g. removing clauses that always hold, etc...

yxliang01 avatar Nov 13 '19 17:11 yxliang01