Dr Oliver Kullman

Honorary Associate Professor (School of Mathematics and Computer Science)

Mathematics and Computer Science School

+44 (0) 1792 513369

o.kullmann@swansea.ac.uk

Available For Postgraduate Supervision

Research Links

ResearcherID

About

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

Publications

Research Highlights

Kullmann, O. (n.d.) The classification of minimally unsatisfiable 2-CNFs -- a fundamental study
https://doi.org/10.48550/arXiv.2003.03639, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa71878
Kullmann, O. & Clewer, E. (2026). Simple minimally unsatisfiable subsets of 2-CNFs. arXiv, 1-18.
https://doi.org/10.48550/arXiv.2603.10944, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa71622
Kullmann, O. (2021). Chapter 8. Fundaments of Branching Heuristics. Frontiers in Artificial Intelligence and Applications, 336
https://doi.org/10.3233/faia200991, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa70993
Büning, H. & Kullmann, O. (2021). Chapter 14. Minimal Unsatisfiability and Autarkies. Frontiers in Artificial Intelligence and Applications, 336
https://doi.org/10.3233/faia200997, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa70991
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
https://doi.org/10.1002/cpe.8004, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa65385

All Research

Journal Articles

Kullmann, O. & Clewer, E. (2026). Simple minimally unsatisfiable subsets of 2-CNFs. arXiv, 1-18.
https://doi.org/10.48550/arXiv.2603.10944, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa71622
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
https://doi.org/10.1002/cpe.8004, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa65385
Kullmann, O. (2021). Chapter 8. Fundaments of Branching Heuristics. Frontiers in Artificial Intelligence and Applications, 336
https://doi.org/10.3233/faia200991, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa70993
Büning, H. & Kullmann, O. (2021). Chapter 14. Minimal Unsatisfiability and Autarkies. Frontiers in Artificial Intelligence and Applications, 336
https://doi.org/10.3233/faia200997, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa70991
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 Lecture Notes in Computer Science (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

Other Research Outputs

Kullmann, O. (n.d.) The classification of minimally unsatisfiable 2-CNFs -- a fundamental study
https://doi.org/10.48550/arXiv.2003.03639, SU Repository: https://cronfa.swan.ac.uk/Record/cronfa71878

Supervision

General Solving Engines Lifting Search Techniques to be used in General Purpose Programming Language (awarded 2025)

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