Thanks, modern rule engines and description logic formalisations are something for me to explore! Are there any other practical applications of such advanced SAT solvers?