I recently took a few days apart to implement my own SAT solver. The idea is to describe the solution space of each clause by a dnf. Then intersect the solutio

I recently took a few days apart to implement my own SAT solver. The idea is to describe the solution space of each clause by a dnf. Then intersect the solution spaces (dnf1 and dnf2).to_dnf() in a way such that the intermediate solution space representations are small. In the end it is solving ALLSAT, by converting cnf to dnf. I'm happy that it works well for many small sized problems.