Dr Oliver Kullmann

Associate Professor

Computer Science

+44 (0) 1792 513369

o.kullmann@swansea.ac.uk

Office - 408
Fourth Floor
Computational Foundry
Bay Campus

Available For Postgraduate Supervision

Research Links

https://orcid.org/0000-0003-3021-0095

ResearcherID

About

Dr Oliver Kullmann is an Associate Professor in the Department of Computer Science, Swansea University.

Publications

Research Highlights

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
https://doi.org/10.1007/978-3-031-30820-8_23, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa62220
http://dx.doi.org/10.1007/978-3-031-30820-8_23
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.
https://doi.org/10.1109/candar57322.2022.00029, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61915
http://dx.doi.org/10.1109/candar57322.2022.00029
Kullmann, O. & Zaikin, O. (2021). Projection Heuristics for Binary Branchings Between Sum and Product. In Theory and Applications of Satisfiability Testing – SAT 2021 (pp. 299-314). Springer International Publishing.
https://doi.org/10.1007/978-3-030-80223-3_21, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa58797
Kullmann, O. & Shukla, A. (2019). Autarkies for DQCNF. In 2019 Formal Methods in Computer Aided Design (FMCAD) (pp. 179-183). IEEE.
https://doi.org/10.23919/fmcad.2019.8894263, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa52742
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
https://doi.org/10.1007/978-3-030-24258-9_15, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa50334
http://dx.doi.org/10.1007/978-3-030-24258-9_15

All Research

Journal Articles

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, 0
https://doi.org/10.1002/cpe.8004, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa65385
http://dx.doi.org/10.1002/cpe.8004
Heule, M. & Kullmann, O. (2017). The science of brute force. Communications of the ACM, 60(8), 70-79.
https://doi.org/10.1145/3107239, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa31506
Ahmed, T., Kullmann, O., & Snevily, H. (2014). On the van der Waerden numbers. Discrete Applied Mathematics, 174, 27-51.
https://doi.org/10.1016/j.dam.2014.05.007, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa18005
http://www.cs.swan.ac.uk/~csoliver/papers.html#VDW232011
Gwynne, M. & Kullmann, O. (2014). Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution. Journal of Automated Reasoning, 52(1), 31-65.
https://doi.org/10.1007/s10817-013-9275-8, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa13746
http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2013
Kullmann, O. & Zhao, X. (2013). On Davis–Putnam reductions for minimally unsatisfiable clause-sets. Theoretical Computer Science, 492, 70-87.
https://doi.org/10.1016/j.tcs.2013.04.020, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa13745
Kullmann, O. (2011). Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.. Fundamenta Informaticae, 109(1), 83-119.
https://doi.org/10.3233/FI-2011-429, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa5284
Kullmann, O. (2011). Constraint satisfaction problems in clausal form I: Autarkies and deficiency.. Fundamenta Informaticae, 109(1), 27-81.
https://doi.org/10.3233/FI-2011-428, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa5283
http://www.cs.swan.ac.uk/~csoliver/papers.html#ClausalFormI
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
http://jsat.ewi.tudelft.nl/content/volume2/JSAT2_4_Kullmann.pdf
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
https://doi.org/10.1023/B:AMAI.0000012871.08577.0b, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa1717
Kullmann, O. (2003). Lean clause-sets: generalizations of minimally unsatisfiable clause-sets. Discrete Applied Mathematics, 130(2), 209
https://doi.org/10.1016/S0166-218X(02)00406-7, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa1714
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
https://doi.org/10.1016/S0304-3975(01)00337-1, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa1716
Kullmann, O. & Kullmann, O. (1999). New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science, 223(1-2), 1-72.
https://doi.org/10.1016/S0304-3975(98)00017-6, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa21436
http://www.sciencedirect.com/science/article/pii/S0304397598000176

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
https://doi.org/10.1007/978-3-031-30820-8_23, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa62220
http://dx.doi.org/10.1007/978-3-031-30820-8_23
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
https://doi.org/10.1007/978-3-030-24258-9_15, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa50334
http://dx.doi.org/10.1007/978-3-030-24258-9_15
Heule, M., Kullmann, O., & Biere, A. (2018). Cube-and-Conquer for Satisfiability. Handbook of Parallel Constraint Reasoning (pp. 31-59). Springer
https://doi.org/10.1007/978-3-319-63516-3_2, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa36186
https://link.springer.com/chapter/10.1007/978-3-319-63516-3_2
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).
https://doi.org/10.1007/978-3-319-24318-4_11, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa26207
Buening, H. & Kullmann, O. (2009). Chapter 11: Minimal satisfiability and autarkies. (pp. 339-401). IOS Press
https://doi.org/10.3233/978-1-58603-929-5-339, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa6
http://cs.swan.ac.uk/~csoliver/Artikel/p01c11_mus.pdf
Kullmann, O. (2009). Chapter 7: Fundaments of branching heuristics. Handbook of Satisfiability (pp. 205-244). IOS Press
https://doi.org/10.3233/978-1-58603-929-5-205, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa7
http://ebooks.iospress.nl/publication/4991
Kullmann, O. (2008). Present and Future of Practical SAT Solving. Complexity of Constraints (pp. 283Springer
https://doi.org/10.1007/978-3-540-92800-3_11, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa5
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 Society
SU 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.
https://doi.org/10.1109/candar57322.2022.00029, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa61915
http://dx.doi.org/10.1109/candar57322.2022.00029
Kullmann, O. & Zaikin, O. (2021). Projection Heuristics for Binary Branchings Between Sum and Product. In Theory and Applications of Satisfiability Testing – SAT 2021 (pp. 299-314). Springer International Publishing.
https://doi.org/10.1007/978-3-030-80223-3_21, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa58797
Kullmann, O. & Shukla, A. (2019). Autarkies for DQCNF. In 2019 Formal Methods in Computer Aided Design (FMCAD) (pp. 179-183). IEEE.
https://doi.org/10.23919/fmcad.2019.8894263, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa52742
Abbasizanjani, H. & Kullmann, O. (2018). Minimal unsatisfiability and minimal strongly connected digraphs. In Theory and Applications of Satisfiability Testing - SAT 2018Springer Cham.
https://doi.org/10.1007/978-3-319-94144-8, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa39955
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
https://www.ijcai.org/proceedings/2017/0683.pdf
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.
https://doi.org/10.1007/978-3-319-40970-2_15, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa28694
http://cs.swan.ac.uk/~csoliver/papers.html#PYTHAGOREAN2016C
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.
https://doi.org/10.1007/978-3-319-09284-3_13, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa18004
http://www.cs.swan.ac.uk/~csoliver/papers.html#HARD2014
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.
https://doi.org/10.1007/978-3-319-04921-2_33, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa18003
http://www.cs.swan.ac.uk/~csoliver/papers.html#XOR2013LATA
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.
https://doi.org/10.1007/978-3-642-35843-2_20, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa13748
http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2012SOFSEM
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).
https://doi.org/10.1007/978-3-642-31612-8_21, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa13747
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.
https://doi.org/10.1007/978-3-642-34188-5_8, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa8073
http://www.cs.swan.ac.uk/~csoliver/papers.html#CuCo2011
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).
https://doi.org/10.1007/978-3-642-21581-0_5, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa7515
Kullmann, O. (2010). Green-Tao Numbers and SAT. In Theory and Applications of Satisfiability Testing – SAT 2010 LCNS (pp. 352-362).
https://doi.org/10.1007/978-3-642-14186-7_32, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa7516
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).
https://doi.org/10.1007/978-3-642-14186-7_20, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa7514

Edited Books

Kullmann, O. (Ed.). (2009). Theory and Applications of Satisfiability Testing -- SAT 2009. Springer.
SU Repository: https://cronfa.swan.ac.uk/Record/cronfa190

Supervision

Singular DP-reduction and minimal unsatisfiability in boolean and non-boolean clause-sets (current)

PhD

Other supervisor: Dr Edwin Beggs
General Solving Engines«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /» Lifting Search Techniques to be used in General«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /»«br /» Purpose Programming Languages (current)

PhD

Other supervisor: Dr Monika Seisenberger
Exploring the IC3 Algorithm to Improve the Siemens-Swansea Ladder Logic Verification Tool (awarded 2023)

MRes

Other supervisor: Prof Markus Roggenbach

Taught Modules

CS-270 Algorithms

This module introduces students to the formal concepts of algorithms and data structures and will enable them to understand how the selection of different algorithms and data types affects the performance and efficiency of a program. Particular attention will be paid to the fundamental problems of searching, sorting, and graph traversal.
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.

Dr Oliver Kullmann

Telephone number

Email address