Finite CSP solvers for modal satisfiability

We present a novel encoding of modal satisfiability problems as Constraint Satisfaction Problems. We allow the domains of the resulting constraints to contain other values than just the Boolean $0$ or $1$, and add various constraints to reason about these values. This modelling is pivotal to speeding up the performance of our constraint-based procedure for modal satisfiability in Constraint Logic Programming (CLP). Our encoding results in a correct solver that attempts to minimize the size of the tree model that it is implicitly trying to generate. An important advantage of our modelling is that we do not need to change the underlying CSP algorithms, and can use them almost as `black boxes