Benjamin Kiesl

Postdoctoral Researcher at the CISPA Helmholtz Center

I'm a postdoc at the CISPA Helmholtz Center for Information Security in Saarbr├╝cken, Germany, working in the group of Cas Cremers. Before, I did a PhD in computer science under the supervision of Martina Seidl and Hans Tompits at TU Wien. I have a background in automated reasoning, in particular in SAT solving, but I have also done some work on other formalisms such as first-order logic and quantified Boolean formulas. Together with Marijn Heule and Armin Biere I have developed strong proof systems for propositional logic that lend themselves neatly to automation. We've also come up with a SAT solving paradigm, called Satisfaction-Driven Clause Learning (SDCL), that harnesses the strengths of our proof systems to solve propositional formulas that are (due to inherent theoretical restrictions) too hard for ordinary SAT solvers.

Besides, I know a thing or two about software engineering: I have some professional experience as a software developer, working with C++ (the programming language I'm most familiar with) and Java. I enjoy writing readable software as much as I enjoy writing readable papers and I believe that these two activities have many things in common.

Contact

Address
Benjamin Kiesl
CISPA – Helmholtz Center for Information Security
Stuhlsatzenhaus 5
66123 Saarbr├╝cken
GERMANY
Email
benjamin.kiesl[at]cispa.saarland

Software

drat2er – A command-line tool that transforms DRAT proofs (as produced by modern SAT solvers) into extended-resolution proofs.

Publications

Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere (2019):
Encoding Redundancy for Satisfaction-Driven Clause Learning. [pdf | bibtex]
In: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019). Best Paper Nomination.
Benjamin Kiesl (2019):
Structural Reasoning Methods for Satisfiability Solving and Beyond. [pdf | bibtex]
PhD Thesis.
Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere (2019):
Strong Extension-Free Proof Systems. [pdf | bibtex]
In: Journal of Automated Reasoning.
Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere (2018):
Local Redundancy in SAT: Generalizations of Blocked Clauses . [pdf | bibtex]
In: Logical Methods in Computer Science (LMCS), vol. 14(4:3).
Benjamin Kiesl, Adrian Rebola-Pardo, and Marijn J.H. Heule (2018):
Extended Resolution Simulates DRAT . [pdf | bibtex]
In: Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018). Best Paper Award.
Marijn J.H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere (2017):
PRuning Through Satisfaction . [pdf | bibtex]
In: Proceedings of the 13th Haifa Verification Conference (HVC 2017). Best Paper Award.
Benjamin Kiesl, Marijn J.H. Heule, and Martina Seidl (2017):
A Little Blocked Literal Goes a Long Way . [pdf | bibtex]
In: Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017).
Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere (2017):
Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? [pdf | bibtex]
In: Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017).
Benjamin Kiesl and Martin Suda (2017):
A Unifying Principle for Clause Elimination in First-Order Logic . [pdf | bibtex]
In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). Best Paper Award.
Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere (2017):
Short Proofs Without New Variables . [pdf | bibtex]
In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). Best Paper Award.
Marijn J.H. Heule and Benjamin Kiesl (2017):
The Potential of Interference-Based Proof Systems [pdf | bibtex]
In: Proceedings of the 1st ARCADE Workshop (ARCADE 2017).
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, and Armin Biere (2017):
Blocked Clauses in First-Order Logic [pdf | bibtex]
In: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21).
Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere (2016):
Super-Blocked Clauses [pdf | bibtex]
In: Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR 2016).