SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in Solving Difference Logic

Abstract

Existing difference logic (DL) solvers can be broadly classified as eager or lazy, each with its own merits and de-merits. We propose a novel difference logic solver SDSAT that combines the strengths of both these approaches and provides a robust performance over a wide set of benchmarks. The solver SDSAT works in two phases: allocation and solve. In the allocation phase, it allocates non-uniform adequate ranges for variables appearing in difference predicates. This phase is similar to previous small domain encoding approaches, but uses a novel algorithm Nu-SMOD with 1-2 orders of magnitude improvement in performance and smaller ranges for variables. Furthermore, the difference logic formula is not transformed into an equi-satisfiable Boolean formula in a single step, but rather done lazily in the following phase. In the solve phase, SDSAT uses a lazy refinement approach to search for a satisfying model within the allocated ranges. Thus, any partially DL-theory consistent model can be discarded if it cannot be satisfied within the allocated ranges. Note the crucial difference: in eager approaches, such a partially consistent model is not allowed in the first place, while in lazy approaches such a model is never discarded. Moreover, we dynamically refine the allocated ranges and search for a feasible solution within the updated ranges. This combined approach benefits from both the smaller search space (as in eager approaches) and also from the theory-specific graph-based algorithms (characteristic of lazy approaches). Experimental results show that our method is robust and always better than or comparable to state-of-the art solvers using similar eager or lazy techniques.