Fast and Flexible Difference Constraint Propagation for DPLL(T)

1. Cherkassky, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. In: Díaz, J. (ed.) ESA 1996. LNCS, vol. 1136, pp. 349–363. Springer, Heidelberg (1996)

   Google Scholar 

2. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms. MIT Press, Cambridge (1990)

   MATH  Google Scholar 

3. Cotton, S.: Satisfiability checking with difference constraints. Master’s thesis, Max Planck Institute (2005)

   Google Scholar 

4. Cotton, S., Maler, O.: Satisfiability modulo theory chains with DPLL(T). In Verimag Technical Report (2006), http://www-verimag.imag.fr/TR/TR-2006-4.pdf

5. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5(7), 394–397 (1962)

   Article  MATH  MathSciNet  Google Scholar 

6. Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(1), 201–215 (1960)

   Article  MATH  MathSciNet  Google Scholar 

7. Dijkstra, E.W.: A note on two problems in connexion with graphs. Numer. Math. 1, 269–271 (1959)

   Article  MATH  MathSciNet  Google Scholar 

8. Eèn, N., Sorensson, N.: Minisat – a sat solver with conflict-clause minimization. In: SAT 2005 (2005)

   Google Scholar 

9. Frigioni, D., Marchetti-Spaccamela, A., Nanni, U.: Fully dynamic shortest paths and negative cycles detection on digraphs with arbitrary arc weights. In: European Symposium on Algorithms, pp. 320–331 (1998)

   Google Scholar 

10. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

11. Goldberg, A.V.: Shortests path algorithms: Engineering aspects. In: Proceedings of the Internation Symposium of Algorithms and Computation (2001)

    Google Scholar 

12. Goldberg, E., Novikov, Y.: Berkmin: A fast and robust SAT solver (2002)

    Google Scholar 

13. Johnson, D.B.: Efficient algorithms for shortest paths in sparse networks. J. Assoc. Comput. Mach. 24(1) (1977)

    Google Scholar 

14. Marquez-Silva, J.P., Sakallah, K.A.: Grasp – a new search algorithm for satisfiability. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 220–227. Springer, Heidelberg (1996)

    Google Scholar 

15. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001 (2001)

    Google Scholar 

16. Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of Timed Automata via Satisfiability Checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 225–243. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

17. Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

18. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 36–50. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

19. Ranise, S., Tinelli, C.: The SMT-LIB format: An initial proposal. In: PDPAR (July 2003)

    Google Scholar 

20. Tarjan, R.E.: Shortest paths. AT&T Technical Reports. AT&T Bell Laboratories (1981)

    Google Scholar 

Download references