We have gone through a similar journey on a project at work - starting by using Z3 then moving to a simpler in-house built boolean constraint solver. Will see if it is something that could be open sourced.