Abstract
In logistics and other application areas, one faces many intractable and NP-hard problems like scheduling, routing, packing, planning, and various kinds of optimization. Many of them can nicely and correctly be modeled by means of graph transformation. But a graph transformation engine fails to run the solutions properly because it does not have any mechanisms to overcome or circumvent the intractability. In this paper, we propose to combine the graph transformation engine GrGen.NET with the SAT solver MiniSat to improve the situation. SAT solvers have proved to run efficiently in many cases in the area of chip design and verification. We want to take these positive experiences up and to use the SAT solver as a tentative experiment for assisting the graph transformation engine in finding solutions to NP-hard problems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Irwin, M.J. (ed.) Proc. of the 36th Annual ACM/IEEE Design Automation Conference, pp. 317–320. ACM (1999)
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)
Blazewicz, J., Ecker, K.H., Pesch, E., Schmidt, G., Weglarz, J. (eds.): Handbook on Scheduling: From Theory to Applications. Springer (2007)
Brucker, P.: Scheduling Algorithms. Springer (2007)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer (2006)
Funsat: http://hackage.haskell.org/package/funsat-0.6.0 (accessed August 26, 2011)
Ganai, M., Gupta, A.: SAT-Based Scalable Formal Verification Solutions. Series on Integrated Circuits and Systems. Springer (2007)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman (1979)
Geiß, R., Kroll, M.: GrGen.NET: A Fast, Expressive, and General Purpose Graph Rewrite Tool. In: Schürr, A., Nagl, M., Zündorf, A. (eds.) AGTIVE 2007. LNCS, vol. 5088, pp. 568–569. Springer, Heidelberg (2008)
Kreowski, H.J., Kuske, S.: Graph transformation units with interleaving semantics. Formal Aspects of Computing 11(6), 690–723 (1999)
Kreowski, H.-J., Kuske, S., Rozenberg, G.: Graph Transformation Units – An Overview. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 57–75. Springer, Heidelberg (2008)
Kreowski, H.-J., Kuske, S., Wille, R.: Graph Transformation Units Guided by a SAT Solver. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 27–42. Springer, Heidelberg (2010)
Limboole (2011), http://fmv.jku.at/limboole/ (accessed August 26, 2011)
Logic2CNF (2011), http://projects.cs.kent.ac.uk/projects/logic2cnf/trac/ (accessed August 26, 2011)
Niedermeier, R.: Invitation to Fixed-Parameter Algorithms. Oxford Lecture Series in Mathematics and its Applications, vol. 31. Oxford University Press, USA (2006)
Pinedo, M.: Scheduling: Theory, Algorithms, and Systems. Springer (2008)
Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1: Foundations. World Scientific (1997)
Sugar (2011), http://bach.istc.kobe-u.ac.jp/sugar/ (accessed August 26, 2011)
Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 466–483 (1968); (reprinted in: Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning, vol. 2, pp. 466–483. Springer (1983))
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ermler, M., Kreowski, HJ., Kuske, S., von Totth, C. (2012). From Graph Transformation Units via MiniSat to GrGen.NET. In: Schürr, A., Varró, D., Varró, G. (eds) Applications of Graph Transformations with Industrial Relevance. AGTIVE 2011. Lecture Notes in Computer Science, vol 7233. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34176-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-34176-2_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34175-5
Online ISBN: 978-3-642-34176-2
eBook Packages: Computer ScienceComputer Science (R0)