About
Dr Oliver Kullmann is an Associate Professor in the Department of Computer Science, Swansea University.
Dr Oliver Kullman
Honorary Associate Professor (School of Mathematics and Computer Science)
Mathematics and Computer Science School
Available For Postgraduate Supervision
Research Links
Publications
Research Highlights
-
Kullmann, O. (n.d.) The classification of minimally unsatisfiable 2-CNFs -- a fundamental study
-
Kullmann, O. & Clewer, E. (2026). Simple minimally unsatisfiable subsets of 2-CNFs. arXiv, 1-18.
-
Kullmann, O. (2021). Chapter 8. Fundaments of Branching Heuristics. Frontiers in Artificial Intelligence and Applications, 336
-
Büning, H. & Kullmann, O. (2021). Chapter 14. Minimal Unsatisfiability and Autarkies. Frontiers in Artificial Intelligence and Applications, 336
-
Pantekis, F., James, P., Kullmann, O., O'Reilly, L., & James, P. (2024). Optimized massively parallel solving of N‐Queens on GPGPUs. Concurrency and Computation: Practice and Experience, 36(10), e8004
All Research
Journal Articles
-
Kullmann, O. & Clewer, E. (2026). Simple minimally unsatisfiable subsets of 2-CNFs. arXiv, 1-18.
-
Pantekis, F., James, P., Kullmann, O., O'Reilly, L., & James, P. (2024). Optimized massively parallel solving of N‐Queens on GPGPUs. Concurrency and Computation: Practice and Experience, 36(10), e8004
-
Kullmann, O. (2021). Chapter 8. Fundaments of Branching Heuristics. Frontiers in Artificial Intelligence and Applications, 336
-
Büning, H. & Kullmann, O. (2021). Chapter 14. Minimal Unsatisfiability and Autarkies. Frontiers in Artificial Intelligence and Applications, 336
-
Heule, M. & Kullmann, O. (2017). The science of brute force. Communications of the ACM, 60(8), 70-79.
-
Ahmed, T., Kullmann, O., & Snevily, H. (2014). On the van der Waerden numbers. Discrete Applied Mathematics, 174, 27-51.
-
Gwynne, M. & Kullmann, O. (2014). Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution. Journal of Automated Reasoning, 52(1), 31-65.
-
Kullmann, O. & Zhao, X. (2013). On Davis–Putnam reductions for minimally unsatisfiable clause-sets. Theoretical Computer Science, 492, 70-87.
-
Kullmann, O. (2011). Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.. Fundamenta Informaticae, 109(1), 83-119.
-
Kullmann, O. (2011). Constraint satisfaction problems in clausal form I: Autarkies and deficiency.. Fundamenta Informaticae, 109(1), 27-81.
-
Kullmann, O. (2009). The OKlibrary: Introducing a "holistic" research platform for (generalised) SAT solving. Studies in Logic, 2(1), 20-53.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa172
-
Kullmann, O. (2006). The SAT 2005 solver competition on random instances. Journal on Satisfiability, Boolean Modeling and Computation, 2, 61-102.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa13744
-
Kullmann, O. (2004). Upper and Lower Bounds on the Complexity of Generalised Resolution and Generalised Constraint Satisfaction Problems. Annals of Mathematics and Artificial Intelligence, 40(3/4), 303
-
Kullmann, O. (2003). Lean clause-sets: generalizations of minimally unsatisfiable clause-sets. Discrete Applied Mathematics, 130(2), 209
-
Fleischner, H., Kullmann, O., & Szeider, S. (2002). Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theoretical Computer Science, 289(1), 503
-
Kullmann, O. & Kullmann, O. (1999). New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science, 223(1-2), 1-72.
Book Chapters
-
Kullmann, O. & Shukla, A. (2023). Transforming Quantified Boolean Formulas Using Biclique Covers. Tools and Algorithms for the Construction and Analysis of Systems (pp. 372-390). Springer Nature Switzerland
-
Mencía, C., Kullmann, O., Ignatiev, A., & Marques-Silva, J. (2019). On Computing the Union of MUSes. Lecture Notes in Computer Science (pp. 211-221). Springer International Publishing
-
Heule, M., Kullmann, O., & Biere, A. (2018). Cube-and-Conquer for Satisfiability. Handbook of Parallel Constraint Reasoning (pp. 31-59). Springer
-
Kullmann, O. & Marques-Silva, J. (2015). Computing Maximal Autarkies with Few and Simple Oracle Queries. Theory and Applications of Satisfiability Testing -- SAT 2015 (pp. 138-155).
-
Buening, H. & Kullmann, O. (2009). Chapter 11: Minimal satisfiability and autarkies. (pp. 339-401). IOS Press
-
Kullmann, O. (2009). Chapter 7: Fundaments of branching heuristics. Handbook of Satisfiability (pp. 205-244). IOS Press
-
Kullmann, O. (2008). Present and Future of Practical SAT Solving. Complexity of Constraints (pp. 283Springer
-
Kullmann, O. (1997). Worst-case Analysis, 3-SAT Decision and Lower Bounds: Approaches for Improved SAT Algorithms. Satisfiability Problem: Theory and Applications (DIMACS Workshop March 11-13, 1996) (pp. 261-313). American Mathematical SocietySU Repository: https://cronfa.swan.ac.uk/Record/cronfa19385
Conference Contributions
-
Pantekis, F., James, P., & Kullmann, O. (2022). Scalable N-Queens Solving on GPGPUs via Interwarp Collaborations. In 2022 Tenth International Symposium on Computing and Networking (CANDAR)IEEE.
-
Kullmann, O. & Zaikin, O. (2021). Projection Heuristics for Binary Branchings Between Sum and Product. In Lecture Notes in Computer Science (pp. 299-314). Springer International Publishing.
-
Kullmann, O. & Shukla, A. (2019). Autarkies for DQCNF. In 2019 Formal Methods in Computer Aided Design (FMCAD) (pp. 179-183). IEEE.
-
Abbasizanjani, H. & Kullmann, O. (2018). Minimal unsatisfiability and minimal strongly connected digraphs. In Theory and Applications of Satisfiability Testing - SAT 2018Springer Cham.
-
Heule, M. & Kullmann, O. (2017). Solving very hard problems: Cube-and-Conquer, a hybrid SAT solving method. In 26th International Joint Conference on Artificial Intelligence (IJCAI 2017) (pp. 4864-4868). International Joint Conference on Artificial Intelligence (IJCAI).SU Repository: https://cronfa.swan.ac.uk/Record/cronfa34731
-
Heule, M., Kullmann, O., & Marek, V. (2016). Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. In Theory and Applications of Satisfiability Testing – SAT 2016 (pp. 228-245). 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings.
-
Beyersdorff, O. & Kullmann, O. (2014). Unified Characterisations of Resolution Hardness Measures. In Theory and Applications of Satisfiability Testing – SAT 2014-187). International Conference on Theory and Applications of Satisfiability Testing: Springer.
-
Gwynne, M. & Kullmann, O. (2014). On SAT Representations of XOR Constraints. In Language and Automata Theory and Applications-420). International Conference on Language and Automata Theory and Applications.
-
Gwynne, M. & Kullmann, O. (2013). Generalising and Unifying SLUR and Unit-Refutation Completeness. In SOFSEM 2013: Theory and Practice of Computer Science. LCNS (pp. 220-232). Springer.
-
Kullmann, O. & Zhao, X. (2012). On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets. In Theory and Applications of Satisfiability Testing – SAT 2012. LCNS (pp. 270-283).
-
Heule, M., Kullmann, O., Wieringa, S., & Biere, A. (2011). Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In Hardware and Software: Verification and Testing (pp. 50-65). Springer.
-
Kullmann, O. & Zhao, X. (2011). On Variables with Few Occurrences in Conjunctive Normal Forms. In Theory and Applications of Satisfiability Testing - SAT 2011 (pp. 33-46).
-
Kullmann, O. (2010). Green-Tao Numbers and SAT. In Theory and Applications of Satisfiability Testing – SAT 2010 LCNS (pp. 352-362).
-
Peschiera, C., Pulina, L., Tacchella, A., Bubeck, U., Kullmann, O., & Lynce, I. (2010). The Seventh QBF Solvers Evaluation (QBFEVAL’10). In Theory and Applications of Satisfiability Testing – SAT 2010 LCNS (pp. 237-250).
Edited Books
-
Kullmann, O. (Ed.). (2009). Theory and Applications of Satisfiability Testing -- SAT 2009. Springer.SU Repository: https://cronfa.swan.ac.uk/Record/cronfa190
Other Research Outputs
-
Kullmann, O. (n.d.) The classification of minimally unsatisfiable 2-CNFs -- a fundamental study
Supervision
-
General Solving Engines Lifting Search Techniques to be used in General Purpose Programming Language (awarded 2025)
PhDOther supervisor: Dr Monika Seisenberger -
Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool (awarded 2023)
MResOther supervisor: Prof Markus Roggenbach
Taught Modules
-
CS-700 Logic and Computation Project
The research project will provide students with the opportunity of exploring a particular topic in computer science in some considerable depth. The project may involve the development of a software system in which case the student will experience the major phases of the life-cycle of a practical IT-project: Specification, design, implementation, testing, verification and validation. The project will enhance the students' competence in algorithm or system analysis, as well as informal and formal mathematical reasoning. It will give students an intellectual challenge to their abilities to learn new subjects without instruction and to further develop their abilities in literature researching, report writing, verbal presentation, project planning and time management.