msakai / toysolver

My sandbox for experimenting with solver algorithms.
Other
154 stars 11 forks source link

Add BC-CNF pseudo boolean constraint encoder #85

Closed msakai closed 2 years ago

msakai commented 2 years ago

The implementation is based on the paper:

This is an incomplete implementation because our sequential encoder does not account for polarities.

There is room for improvement regarding the relationship between PB encoder, cardinality constraint encoder, and the Tseitin encoder.