Wissenschaftliche Artikel

Bloem, R., Braud-Santoni, N., Hadzic, V., Egly, U., Lonsing, F., & Seidl, M. (2021). Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations. Formal Methods in System Design, 57(2), 157–177. https://doi.org/10.1007/s10703-021-00371-7 ( reposiTUm)
Egly, U., Kronegger, M., Lonsing, F., & Pfandler, A. (2017). Conformant planning as a case study of incremental QBF solving. Annals of Mathematics and Artificial Intelligence, 80(1), 21–45. http://hdl.handle.net/20.500.12708/147186 ( reposiTUm)
Egly, U., Kronegger, M., Lonsing, F., & Pfandler, A. (2016). Conformant Planning as a Case Study of Incremental QBF Solving. Annals of Mathematics and Artificial Intelligence, 80(1), 21–45. https://doi.org/10.1007/s10472-016-9501-2 ( reposiTUm)
Creignou, N., Daudé, H., Egly, U., & Rossignol, R. (2015). Exact location of the phase transition for random (1,2)-QSAT. RAIRO - Theoretical Informatics and Applications, 49(1), 23–45. https://doi.org/10.1051/ita/2014025 ( reposiTUm)
Creignou, N., Egly, U., & Schmidt, J. (2014). Complexity Classifications for Logic-Based Argumentation. ACM Transactions on Computational Logic, 15(3), 1–20. https://doi.org/10.1145/2629421 ( reposiTUm)
Miljanovic, M., Egly, U., & Eiter, T. (2012). Detection of Windows in Facades Using Image Processing Algorithms. Indian Journal of Computer Science and Engineering, 3(4), 539–547. http://hdl.handle.net/20.500.12708/164414 ( reposiTUm)
Reiterer, A., Egly, U., Vicovac, T., Mai, E., Moafipoor, S., Grejner-Brzezinska, D. A., & Toth, C. K. (2010). Application of artificial intelligence in Geodesy - A review of theoretical foundations and practical examples. Journal of Applied Geodesy, 4(4). https://doi.org/10.1515/jag.2010.020 ( reposiTUm)
Egly, U., Gaggl, S., & Woltran, S. (2010). Answer-Set Programming Encodings for Argumentation Frameworks. Argument and Computation, 1(2), 147–177. http://hdl.handle.net/20.500.12708/167366 ( reposiTUm)
Egly, U., & Haller, L. (2010). A SAT Solver for Circuits Based on the Tableau Method. KI - Künstliche Intelligenz, 24(1), 15–23. https://doi.org/10.1007/s13218-010-0008-4 ( reposiTUm)
Reiterer, A., Lehmann, M., Miljanovic, M., Ali, H., Paar, G., Egly, U., Eiter, T., & Kahmen, H. (2009). A 3D optical deformation measurement system supported by knowledge-based and learning techniques. Journal of Applied Geodesy, 3(1), 1–13. http://hdl.handle.net/20.500.12708/165576 ( reposiTUm)
Egly, U., Seidl, M., & Woltran, S. (2009). A Solver for QBFs in Negation Normal Form. Constraints, 14(1), 38–79. http://hdl.handle.net/20.500.12708/165275 ( reposiTUm)
Reiterer, A., Egly, U., Eiter, T., & Kahmen, H. (2008). A knowledge-based videotheodolite measurement system for object representation /monitoring. Advances in Engineering Software, 39(10), 821–827. http://hdl.handle.net/20.500.12708/168962 ( reposiTUm)
Creignou, N., Daude, H., & Egly, U. (2007). Phase Transition for Random Quantified XOR-Formulas. Journal of Artificial Intelligence Research, 29, 1–18. http://hdl.handle.net/20.500.12708/169673 ( reposiTUm)
Egly, U., Pichler, R., & Woltran, S. (2005). On Deciding Subsumption Problems. Annals of Mathematics and Artificial Intelligence, 43(1–4), 255–294. http://hdl.handle.net/20.500.12708/173345 ( reposiTUm)

Beiträge in Tagungsbänden

Mandl, A., & Egly, U. (2022). Implementations for Shor’s algorithm for the DLP. In 52. Jahrestagung der Gesellschaft für Informatik (pp. 1133–1143). Gesellschaft für Informatik. https://doi.org/10.18420/inf2022_96 ( reposiTUm)
Lonsing, F., & Egly, U. (2019). QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. In Theory and Applications of Satisfiability Testing – SAT 2019 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019, Proceedings (pp. 203–210). LNCS. https://doi.org/10.1007/978-3-030-24258-9_14 ( reposiTUm)
Lonsing, F., & Egly, U. (2018). Evaluating QBF Solvers: Quantifier Alternations Matter. In Principles and Practice of Constraint Programming 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings (pp. 276–294). Springer. https://doi.org/10.1007/978-3-319-98334-9_19 ( reposiTUm)
Lonsing, F., & Egly, U. (2018). $${\textsf {QRAT}}^{+}$$: Generalizing QRAT by a More Powerful QBF Redundancy Property. In Automated Reasoning (pp. 161–177). LNCS. https://doi.org/10.1007/978-3-319-94205-6_12 ( reposiTUm)
Bloem, R., Braud-Santoni, N., Hadzic, V., Egly, U., Lonsing, F., & Seidl, M. (2018). Expansion-Based QBF Solving Without Recursion. In 2018 Formal Methods in Computer Aided Design (FMCAD). International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, United States of America (the). IEEE. https://doi.org/10.23919/fmcad.2018.8603004 ( reposiTUm)
Lonsing, F., & Egly, U. (2017). DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. In Automated Deduction – CADE 26 (pp. 371–384). Springer. https://doi.org/10.1007/978-3-319-63046-5_23 ( reposiTUm)
Lonsing, F., Egly, U., & Seidl, M. (2016). Q-Resolution with Generalized Axioms. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 435–452). Springer. https://doi.org/10.1007/978-3-319-40970-2_27 ( reposiTUm)
Egly, U. (2016). On Stronger Calculi for QBFs. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 419–434). Springer. https://doi.org/10.1007/978-3-319-40970-2_26 ( reposiTUm)
Lonsing, F., Bacchus, F., Biere, A., Egly, U., & Seidl, M. (2015). Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 418–433). Springer. https://doi.org/10.1007/978-3-662-48899-7_29 ( reposiTUm)
Egly, U., Lonsing, F., & Oetsch, J. (2015). Automated Benchmarking of Incremental SAT and QBF Solvers. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 178–186). Springer. https://doi.org/10.1007/978-3-662-48899-7_13 ( reposiTUm)
Lonsing, F., & Egly, U. (2015). Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. In Theory and Applications of Satisfiability Testing -- SAT 2015 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings (pp. 191–198). Springer. https://doi.org/10.1007/978-3-319-24318-4_14 ( reposiTUm)
Lonsing, F., & Egly, U. (2014). Incremental QBF Solving. In Principles and Practice of Constraint Programming 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014, Proceedings (pp. 514–530). Springer. https://doi.org/10.1007/978-3-319-10428-7_38 ( reposiTUm)
Lonsing, F., & Egly, U. (2014). Incremental QBF Solving by DepQBF. In Mathematical Software – ICMS 2014 (pp. 307–314). Springer. https://doi.org/10.1007/978-3-662-44199-2_48 ( reposiTUm)
Egly, U., Kronegger, M., Lonsing, F., & Pfandler, A. (2014). Conformant Planning as a Case Study of Incremental QBF Solving. In Artificial Intelligence and Symbolic Computation (pp. 120–131). Springer. https://doi.org/10.1007/978-3-319-13770-4_11 ( reposiTUm)
Balabanov, V., Widl, M., & Jiang, J.-H. R. (2014). QBF Resolution Systems and Their Proof Complexities. In C. Sinz & U. Egly (Eds.), Theory and Applications of Satisfiability Testing - SAT 2014 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings (pp. 154–169). LNCS / Springer. https://doi.org/10.1007/978-3-319-09284-3_12 ( reposiTUm)
Bloem, R., Egly, U., Klampfl, P., Könighofer, R., & Lonsing, F. (2014). SAT-Based Methods for Circuit Synthesis. In Formal Methods in Computer-Aided Design (pp. 31–34). IEEE. http://hdl.handle.net/20.500.12708/55291 ( reposiTUm)
Lonsing, F., Egly, U., & Van Gelder, A. (2013). Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. In Theory and Applications of Satisfiability Testing – SAT 2013 (pp. 100–115). https://doi.org/10.1007/978-3-642-39071-5_9 ( reposiTUm)
Widl, M., Biere, A., Kaufmann, P., Egly, U., Heule, M., Kappel, G., Seidl, M., & Tompits, H. (2013). Guided Merging of Sequence Diagrams. In Software Language Engineering (pp. 164–183). Lecture Notes in Computer Science Volume 7745. https://doi.org/10.1007/978-3-642-36089-3_10 ( reposiTUm)
Egly, U., & Widl, M. (2013). Solution extraction from long-distance resolution proofs. In M. Seidl & F. Lonsing (Eds.), International Workshop on Quantified Boolean Formulas 2013 Informal Workshop Report (p. 10). http://hdl.handle.net/20.500.12708/54894 ( reposiTUm)
Egly, U., Lonsing, F., & Widl, M. (2013). Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. In K. McMillan, A. Middeldorp, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 291–308). Springer. https://doi.org/10.1007/978-3-642-45221-5_21 ( reposiTUm)
Kaufmann, P., Egly, U., Gabmeyer, S., Kappel, G., Seidl, M., Tompits, H., Widl, M., & Wimmer, M. (2012). Towards Scenario-Based Testing of UML Diagrams. In Tests and Proofs (pp. 149–155). Springer. https://doi.org/10.1007/978-3-642-30473-6_12 ( reposiTUm)
Creignou, N., Egly, U., & Seidl, M. (2012). A Framework for the Specification of Random SAT and QSAT Formulas. In Proceedings of the 6th International Conference on Tests and Proofs (TAP 2012) (pp. 163–168). Springer. http://hdl.handle.net/20.500.12708/54164 ( reposiTUm)
Egly, U., Creignou, N., & Schmidt, J. (2012). Complexity of logic-based argumentation in Schaefer’s framework. In B. Verheij, S. Szeider, & S. Woltran (Eds.), Computational Models of Argument (pp. 237–248). IOS Press. http://hdl.handle.net/20.500.12708/54461 ( reposiTUm)
Egly, U. (2012). On Sequent Systems and Resolution for QBFs. In Theory and Applications of Satisfiability Testing – SAT 2012 (pp. 100–113). Lecture Notes in Computer Science, Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-31612-8_9 ( reposiTUm)
Kaufmann, P., Egly, U., Gabmeyer, S., Kappel, G., Seidl, M., Tompits, H., Widl, M., & Wimmer, M. (2012). Towards Semantics-Aware Merge Support in Optimistic Model Versioning. In Models in Software Engineering (pp. 246–256). Springer LNCS. https://doi.org/10.1007/978-3-642-29645-1_24 ( reposiTUm)
Widl, M., Biere, A., Kaufmann, P., Egly, U., Heule, M., Kappel, G., Seidl, M., & Tompits, H. (2012). Guided Merging of Sequence Diagrams. In K. Czarnecki & G. Hedin (Eds.), SLE 2012 - Pre-proceedings (pp. 163–182). http://hdl.handle.net/20.500.12708/54255 ( reposiTUm)
Kaufmann, P., Egly, U., Gabmeyer, S., Kappel, G., Seidl, M., Tompits, H., Widl, M., & Wimmer, M. (2011). Towards Semantics-Aware Merge Support in Optimistic Model Versioning. In Proceedings of the Models and Evolution Workshop @ MoDELS’11 (p. 10). http://hdl.handle.net/20.500.12708/53735 ( reposiTUm)
Vicovac, T., Reiterer, A., Egly, U., Eiter, T., & Rieke-Zapp, D. (2010). Knowledge-Based Geo-risk Assessment for an Intelligent Measurement System. In M. Bramer (Ed.), Artificial Intelligence in Theory and Practice III (pp. 215–224). Springer. https://doi.org/10.1007/978-3-642-15286-3_21 ( reposiTUm)
Vicovac, T., Reiterer, A., Egly, U., Eiter, T., & Rieke-Zapp, D. (2010). Intelligent Deformation Interpretation. In A. Reiterer, U. Egly, M. Heinert, & B. Riedel (Eds.), Application of Artificial Intelligence and Innovations in Engineering Geodesy (AIEG 2010) (pp. 10–20). http://hdl.handle.net/20.500.12708/42560 ( reposiTUm)
Vicovac, T., Reiterer, A., Egly, U., Eiter, T., & Rieke-Zapp, D. (2009). First Developement steps for an Automated Knowledge-Based Deformation Interpretation System. In A. Grün & H. Kahmen (Eds.), Optical 3-D Measurement Techniques IX (pp. 61–90). http://hdl.handle.net/20.500.12708/42385 ( reposiTUm)
Creignou, N., Daudé, H., Egly, U., & Rossignol, R. (2009). (1,2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms. In O. Kullmann (Ed.), Theory and Applications of Satisfiability Testing - SAT 2009 (pp. 363–376). Springer Lecture Notes in Computer Science (LNCS). https://doi.org/10.1007/978-3-642-02777-2_34 ( reposiTUm)
Reiterer, A., Lehmann, M., Miljanovic, M., Ali, H., Paar, G., Egly, U., Eiter, T., & Kahmen, H. (2008). Deformation Monitoring using a new kind of Optical 3D Measurement System: Components and Perspectives. In Measuring the Change (p. 10). http://hdl.handle.net/20.500.12708/42215 ( reposiTUm)
Reiterer, A., Lehmann, M., Miljanovic, M., Ali, H., Paar, G., Egly, U., Eiter, T., & Kahmen, H. (2008). Ein bildgestütztes 3D Deformationsmesssystem (An Image-Based 3D Deformation Measurement System). In Journal of Alpine Geology, Pangeo 2008 (p. 87). Mitt. Ges. Geol. Bergbaustud. Österr. http://hdl.handle.net/20.500.12708/42265 ( reposiTUm)
Lehmann, M., & Reiterer, A. (2008). Case-Based Deformation Assessment - A Concept. In A. Reiterer & U. Egly (Eds.), Application of Artificial Intelligence in Engineering Geodesy (pp. 91–98). http://hdl.handle.net/20.500.12708/42283 ( reposiTUm)
Creignou, N., Daude, H., Egly, U., & Rossignol, R. (2008). New Results on the Phase Transition for Random Quantified Boolean Formulas. In Theory and Application of Satisfiability Testing --- SAT 2008 (pp. 34–47). Lecture Notes in Computer Science. http://hdl.handle.net/20.500.12708/52643 ( reposiTUm)
Egly, U., Gaggl, S. A., & Woltran, S. (2008). ASPARTIX: Implementing Argumentation Frameworks Using Answer-Set Programming. In M. G. de la Banda & E. Pontelli (Eds.), Proceedings of the 24#^{th} Conference on Logic Programming (ICLP’08) (pp. 734–738). Springer. http://hdl.handle.net/20.500.12708/52465 ( reposiTUm)
Egly, U., Gaggl, S. A., & Woltran, S. (2008). Answer-Set Programming Encodings for Argumentation Frameworks. In W. Faber & J. Lee (Eds.), ICLP-Workshop Proceedings; Proceedings of the 1st International Workshop on Answer Set Programming and Other Computing Paradigms, ASPOCP 2008 (pp. 1–15). http://hdl.handle.net/20.500.12708/52469 ( reposiTUm)
Egly, U., & Woltran, S. (2006). Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas. In P. E. Dunne & T. J. M. Bench-Capon (Eds.), Proceedings of the 1st International Conference on Computational Models of Argument (COMMA 2006) (pp. 133–144). IOS Press. http://hdl.handle.net/20.500.12708/51590 ( reposiTUm)
Egly, U., Seidl, M., & Woltran, S. (2006). A Solver for QBFs in Nonprenex Form: Overview and Experimental Results. In Proceedings of the Guangzhou Symposioum on Satisfiability in Logic-Based Modeling (p. 11). http://hdl.handle.net/20.500.12708/51624 ( reposiTUm)
Creignou, N., Daude, H., & Egly, U. (2006). Phase Transition for Random Quantified XOR-formulas. In Proceedings of the Guangzhou Symposioum on Satisfiability in Logic-Based Modeling (p. 12). http://hdl.handle.net/20.500.12708/51625 ( reposiTUm)
Egly, U., Seidl, M., & Woltran, S. (2006). A Solver for QBFs in Nonprenex Form. In Proceedings of the ECAI 2006 (pp. 477–481). IOS Press. http://hdl.handle.net/20.500.12708/51448 ( reposiTUm)
Reiterer, A., Egly, U., Eiter, T., & Kahmen, H. (2005). A Knowledge-Based Decision System for an Image-Based Measurement. In B. H. V. Topping (Ed.), Proceedings of the Eighth International Conference on the Application of Artificial Intelligence to Civil, Structural and Environmental Engineering (pp. 35–36). http://hdl.handle.net/20.500.12708/41891 ( reposiTUm)
Reiterer, A., Kahmen, H., Eiter, T., Egly, U., & Paar, G. (2005). A Smart Videometric System. In A. Grün & H. Kahmen (Eds.), Proceedings Optical 3-D Measurement Techniques VII, Vol. II (pp. 370–375). http://hdl.handle.net/20.500.12708/41914 ( reposiTUm)
Egly, U., Novak, G., & Weber, D. (2005). Decision Making for MiroSOT Soccer Playing Robots. In Decision Making for MiroSOT Soccer Playing Robots (pp. 69–72). http://hdl.handle.net/20.500.12708/68833 ( reposiTUm)

Bücher

Reiterer, A., & Egly, U. (Eds.). (2008). Application of Artificial Intelligence in Engineering Geodesy. Eigenverlag. http://hdl.handle.net/20.500.12708/22790 ( reposiTUm)

Tagungsbände

Beyersdorff, O., Egly, U., Mahajan, M., & Nalon, C. (Eds.). (2020). SAT and Interactions (Dagstuhl Seminar 20061). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/DagRep.10.2.1 ( reposiTUm)
Theory and Applications of Satisfiability Testing – SAT 2014. (2014). In C. Sinz & U. Egly (Eds.), Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-319-09284-3 ( reposiTUm)

Präsentationen

Egly, U. (2016). Translations from QBFs to First-order Logic. Deduktionstreffen, Klagenfurt, Austria. http://hdl.handle.net/20.500.12708/86444 ( reposiTUm)
Egly, U. (2014). Quantifier handling in calculi for quantified Boolean formulas. International Workshop on Quantification (QUANTIFY), Wien, Austria. http://hdl.handle.net/20.500.12708/85997 ( reposiTUm)
Egly, U. (2014). Deduction Concepts for Quantified Boolean Formulas. Advanced Winter School on Reasoning Engines for Rigorous System Engineering, Johannes Kepler University, Linz, Austria. http://hdl.handle.net/20.500.12708/86000 ( reposiTUm)
Egly, U. (2014). On the Relation between Resolution Calculi for QBFs and First-order Formulas. International Workshop on Quantified Boolean Formulas, Helsinki, Finland. http://hdl.handle.net/20.500.12708/85998 ( reposiTUm)
Egly, U. (2014). Quantifier Handling in Different Calculi for Quantified Boolean Formulas. Algebra, Logic and Algorithms seminar, Leeds, United Kingdom of Great Britain and Northern Ireland (the). http://hdl.handle.net/20.500.12708/85999 ( reposiTUm)
Egly, U., Kronegger, M., Lonsing, F., & Pfandler, A. (2014). Conformant Planning as a Case Study of Incremental QBF Solving. International Workshop on Quantified Boolean Formulas, Helsinki, Finland. http://hdl.handle.net/20.500.12708/85946 ( reposiTUm)
Egly, U. (2013). Questions around quantified boolean formulas. ANR Boole Réunion Finale, Paris, Frankreich, EU. http://hdl.handle.net/20.500.12708/85685 ( reposiTUm)
Egly, U. (2013). Solving quantified Boolean formula. Journées ANR BOOLE, Marseille, Frankreich, EU. http://hdl.handle.net/20.500.12708/85684 ( reposiTUm)
Egly, U. (2012). On sequent systems and resolution for quantified boolean formulas. Dagstuhl Seminar 12471 - SAT Interactions, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85469 ( reposiTUm)
Egly, U. (2012). A new learning scheme for QDPLL solvers. Dagstuhl Seminar 12461: Games and Decisions for Rigorous Systems Engineering, Dagstuhl, Deutschland, EU. http://hdl.handle.net/20.500.12708/85468 ( reposiTUm)
Egly, U. (2011). DPLL Procedures for Non-clausal SAT and QSAT Problems. Workshop on Computational Logics and Applications, Wien, Austria. http://hdl.handle.net/20.500.12708/85220 ( reposiTUm)
Reiterer, A., Bauer, A., & Egly, U. (2008). Deformation Monitoring by Image Assisted Total Stations - State of the Art and Future Developments. Technologieforum Leica Geosystems, Heerbrugg, Schweiz, Non-EU. http://hdl.handle.net/20.500.12708/82156 ( reposiTUm)
Egly, U. (2004). Argumentation Frameworks and QBFs. International Workshop on QSAT and SAT, Guangzhou, P.R. China, Austria. http://hdl.handle.net/20.500.12708/84320 ( reposiTUm)
Egly, U. (2003). Beyond DP: Alternative Calculi for QBF Solving. QBF-symposium, Paris, France, Austria. http://hdl.handle.net/20.500.12708/84235 ( reposiTUm)

Berichte

Lonsing, F., & Egly, U. (2017). Evaluating QBF Solvers: Quantifier Alternations Matter. http://hdl.handle.net/20.500.12708/39349 ( reposiTUm)
Egly, U., Gaggl, S. A., & Woltran, S. (2008). Answer-Set Programming Encodings for Argumentation Frameworks (DBAI-TR-2008-62). http://hdl.handle.net/20.500.12708/35164 ( reposiTUm)
Egly, U., Seidl, M., & Woltran, S. (2008). A Solver for QBFs in Negation Normal Form (INFSYS RR-1843-08-03). http://hdl.handle.net/20.500.12708/35354 ( reposiTUm)
Egly, U., Pichler, R., & Woltran, S. (2003). On Deciding Subsumption Problems. http://hdl.handle.net/20.500.12708/32928 ( reposiTUm)

Preprints

Egly, U., Creignou, N., & Schmidt, J. (2013). Complexity Classifications for logic-based Argumentation. arXiv. https://doi.org/10.48550/arXiv.1304.5388 ( reposiTUm)