Modelling and solving temporal reasoning as propositional satisfiability