Integration of DPLL-SAT and Linear Programming
Christian Herde · Vieweg+Teubner eBooks · 2011
In this chapter, we present a decision procedure which is tailored to fit the needs of BMC of infinite-state systems with piecewise linear variable updates, e.g. of linear hybrid automata, as introduced in chapter 2. Our tool, we name it H y SAT-1, tightly integrates a DPLL style SAT solver with a linear programming routine, combining the virtues of both methods: Linear programming adds the capability of solving large conjunctive systems of linear inequalities over the reals, whereas the SAT solver accounts for fast Boolean search and efficient handling of disjunctions. Building on the work presented in chapter 3, we use our pseudo-Boolean solver GOBLIN as SAT engine in H y SAT-1. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.