Constraint methods for modal satisfiability

Modal and modal-like formalisms such as temporal or description logics go beyond propositional logic by introducing operators that allow for a guarded form of quantication over states or paths of transition systems. Thus, they are more expressive than propositional logic, yet computationally better behaved than rst-order logic. We propose constraint-based methods to model and solve modal satisability problems. We model the satisability of basic modal formulas via appropriate sets of nite constraint satisfaction problems, and then resolve these via constraint solvers. The domains of the constraint satisfaction problems contain other values than just the Boolean 0 or 1; for these values, we create specialised constraints that help us steer the decision procedure and so keep the modal search tree as small as possible. We show experimentally that this constraint modelling gives us a better control over the decision procedure than existing SAT-based models.