Abstract
Model Checking (MC) and Constraint Programming (CP) are complementary techniques with the potential for mutual improvement. In this paper, we focus on leveraging on-the-fly MC techniques to improve the performance of a CP solver for dynamic problems. To evaluate the effectiveness of our approach, we conduct a case study based on a reachability problem. Using a constructive approach inspired by MC, we propose to incorporate an on-the-fly strategy into an existing CP solver. Through comparative analysis, we evaluate this technique’s impact on the solver’s performance in terms of time and space efficiency. Our results show that the on-the-fly MC-based CP solver performs better than a pure CP solver, overcoming the limitations of the destructive approach typically used in CP. More precisely, the introduction of the on-the-fly strategy allows one to gain a factor of at least 20 in time/space. This work contributes to bridging the gap between MC and CP, highlights the potential for cross-domain improvement, and opens avenues for future research combining these powerful formal techniques.