Wissenschaftliche Artikel

Lonsing, F., Seidl, M., & Van Gelder, A. (2016). The QBF Gallery: Behind the Scenes. Artificial Intelligence, 237, 92–114. https://doi.org/10.1016/j.artint.2016.04.002 ( 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)
Janota, M., Jordan, C., Klieber, W., Lonsing, F., Seidl, M., & Van Gelder, A. (2016). The QBF Gallery 2014: The QBF Competition at the FLoC Olympic Games. Journal on Satisfiability, Boolean Modeling and Computation, 9, 187–206. http://hdl.handle.net/20.500.12708/149734 ( 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)
Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., & Biere, A. (2015). Clause Elimination for SAT and QSAT. Journal of Artificial Intelligence Research, 53, 127–168. https://doi.org/10.1613/jair.4694 ( reposiTUm)
Widl, M., & Musliu, N. (2014). The break scheduling problem: complexity results and practical algorithms. Memetic Computing, 6(2), 97–112. https://doi.org/10.1007/s12293-014-0131-0 ( 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)

Beiträge in Tagungsbänden

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)
Balyo, T., & Lonsing, F. (2016). HordeQBF: A Modular and Massively Parallel QBF Solver. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 531–538). Springer. https://doi.org/10.1007/978-3-319-40970-2_33 ( 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)
Jordan, C., Kaiser, L., Lonsing, F., & Seidl, M. (2014). MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing. In 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. 430–437). LNCS / Springer. https://doi.org/10.1007/978-3-319-09284-3_32 ( 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., Jiang, J.-H. R., Janota, M., & Widl, M. (2014). Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs. In 2nd International Workshop on Quantified Boolean Formulas (p. 13). http://hdl.handle.net/20.500.12708/55980 ( 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)
Kaufmann, P., Kronegger, M., Pfandler, A., Seidl, M., & Widl, M. (2014). A SAT-Based Debugging Tool for State Machines and Sequence Diagrams. In Proceedings of the 7th International Conference on Software Language Engineering (SLE) (pp. 21–40). http://hdl.handle.net/20.500.12708/55748 ( reposiTUm)
Kaufmann, P., Kronegger, M., Pfandler, A., Seidl, M., & Widl, M. (2013). Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines. In Proceedings of the 10th International Workshop on Model Driven Engineering, Verification and Validation co-located with 16th International Conference on Model Driven Engineering Languages and Systems (MODELS 2013) (pp. 31–40). CEUR Workshop Proceedings. http://hdl.handle.net/20.500.12708/54717 ( reposiTUm)
Kaufmann, P., Seidl, M., & Widl, M. (2013). Semantics-Aware Versioning Challenge: Merging Sequence Diagrams along with State Machine Diagrams. In Softwaretechnik-Trends (pp. 1–3). Gesellschaft für Informatik. http://hdl.handle.net/20.500.12708/54587 ( 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)
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)
Widl, M. (2012). Test Case Generation by Grammar-based Fuzzing for Model-driven Engineering. In A. Biere, A. Nahir, & T. Vos (Eds.), Proceedings of the Eighth Haifa Verification Conference (p. 2). http://hdl.handle.net/20.500.12708/54407 ( 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)
Widl, M. (2011). Towards a Uniform Framework to Support the Evolution of Software Models. In Proceedings of the Doctoral Symposium at MODELS 2011 (p. 8). http://hdl.handle.net/20.500.12708/53833 ( reposiTUm)

Tagungsbände

Lonsing, F., & Seidl, M. (Eds.). (2016). Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016). CEUR-WS.org. http://hdl.handle.net/20.500.12708/24255 ( 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

Lonsing, F. (2017). Evaluating QBF Solvers: Quantifier Alternations Matter. Alpine Verification Meeting, IST Austria, Austria. http://hdl.handle.net/20.500.12708/86673 ( reposiTUm)
Lonsing, F. (2017). Parallel QBF Solving: State of the Art Techniques and Future Perspectives. First Workshop on Parallel Constraint Reasoning, Göteborg, Sweden. http://hdl.handle.net/20.500.12708/86674 ( reposiTUm)
Lonsing, F. (2017). An Introduction to QBF Solving. The Second Indian SAT+SMT School, Mysuru, India. http://hdl.handle.net/20.500.12708/86672 ( reposiTUm)
Egly, U. (2016). Translations from QBFs to First-order Logic. Deduktionstreffen, Klagenfurt, Austria. http://hdl.handle.net/20.500.12708/86444 ( reposiTUm)
Lonsing, F. (2016). Submissions to QBFEVAL’16. 4th International Workshop on Quantified Boolean Formulas (QBF 2016), Bordeaux, France. http://hdl.handle.net/20.500.12708/86434 ( reposiTUm)
Lonsing, F. (2016). An Overview of QBF Reasoning Techniques. Dagstuhl Seminar 16381: SAT and Interactions, Wadern, Germany. http://hdl.handle.net/20.500.12708/86432 ( reposiTUm)
Lonsing, F. (2016). Tutorial at IJCAI 2016: Solving (Problems with) Quantified Boolean Formulas: Recent Trends and Challenges. Twenty-Fifth International Joint Conference on Artificial Intelligence - IJCAI 2016, New York, NY, United States of America (the). http://hdl.handle.net/20.500.12708/86433 ( reposiTUm)
Lonsing, F. (2015). Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. PUMA/RiSE Workshop, Mondsee, Austria. http://hdl.handle.net/20.500.12708/86173 ( reposiTUm)
Lonsing, F. (2014). Incremental QBF Solving. Alpine Verification Meeting, IST Austria, Austria. http://hdl.handle.net/20.500.12708/85891 ( 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)
Lonsing, F. (2014). Search-Based QBF Solving. Advanced Winter School on Reasoning Engines for Rigorous System Engineering, Johannes Kepler University, Linz, Austria. http://hdl.handle.net/20.500.12708/86001 ( 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. (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)

Berichte

Lonsing, F., & Egly, U. (2017). Evaluating QBF Solvers: Quantifier Alternations Matter. http://hdl.handle.net/20.500.12708/39349 ( reposiTUm)