
Dr. rer. nat. Markus Iser
- Post-Doctoral Researcher
- Automated Reasoning and Optimization, Meta Algorithmics, Explainable Artificial Intelligence, Algorithm Visualization and Sonification
- Raum: 208
- Tel.: +49 721 608-44232
- Fax: +49 721 608-43088
- markus iser ∂does-not-exist.kit edu
- GitHub
Projects and Teaching
Courses
Title | Type | Semester |
---|---|---|
Fortgeschrittene Themen im SAT Solving | Seminar | WS 2022/23 |
SAT Solving in der Praxis | Lecture and Exercises | SS 2023 |
Fortgeschrittene Themen im SAT Solving (renamed from "Scalability and Diversification in Modern SAT Solving") | Seminar | WS 2022/23 |
Practical SAT Solving | Lecture and Exercises | SS 2022 |
Animating Propositional Proofs | Praxis der Softwareentwicklung | WS 2021/22 |
Automating SAT Solver Research | Praxis der Forschung | WS 2021/22 |
Scalability and Diversification in Modern SAT Solving | Seminar | WS 2021/22 |
Practical SAT Solving | Lecture and Exercises | SS 2021 |
Scalability and Diversification in Modern SAT Solving | Seminar | WS 2020/21 |
Practical SAT Solving | Lecture and Exercises | SS 2020 |
SAT Community Karlsruhe (SACK) | Seminar | WS 2019/20 |
Algorithms 1 | Exercises and Lecture Organization | SS 2019 |
Algorithms 1 | Exercises and Lecture Organization | SS 2018 |
Programming | Exercises and Lecture Organization | WS 2013/14 |
Programming | Exercises and Lecture Organization | WS 2012/13 |
Open and Running Thesises
Title | Type |
---|---|
Explaining Random Forest Classifiers through SAT-based Abduction | Master Thesis |
Fuzzy Clause Importance Measures through Trail Sampling | Master Thesis |
Runtime Prediction for SAT Instances | Master Thesis (external) |
Constructing Binary Decision Diagrams | Master Thesis (external) |
Data-Driven Automatic and Optimal Evaluation of SAT Solvers | Bachelor / Master Thesis |
A Novel SAT Solver Architecture | Master Thesis (external) |
SAT-based Product Configuration | Master Thesis (external) |
Publications
Title | Authors | Publication | Year |
---|---|---|---|
Oracle-Based Local Search for Pseudo-Boolean Optimization | Markus Iser, Jeremias Berg, Matti Järvisalo | Proceedings of the 26th European Conference on Artificial Intelligence (ECAI 2023) | 2023 |
Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions | Editors: Tomáš Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda | University of Helsinki, Department of Computer Science | 2023 |
Active Learning for SAT Solver Benchmarking | Tobias Fuchs, Jakob Bach, Markus Iser | International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023) | 2023 |
A Comprehensive Study of k-Portfolios of Recent SAT Solvers | Jakob Bach, Markus Iser, Klemens Böhm | International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) | 2022 |
Dinosat: A SAT Solver with Native DNF Support | Thomas Bartel, Tomáš Balyo, Markus Iser | Pragmatics of SAT (POS 2022) | 2022 |
SATViz: Real-Time Visualization of Clausal Proofs | Tim Holzenkamp, Kevin Kuryshev, Thomas Oltmann, Lucas Wäldele, Johann Zuber, Tobias Heuer, and Markus Iser |
Pragmatics of SAT (POS 2022) | 2022 |
Unit Propagation with Stable Watches (+Video) | Markus Iser, Tomáš Balyo | 27th International Conference on Principles and Practice of Constraint Programming (CP 2021) | 2021 |
Fast Approximate Calculation of Valid Domains in a Satisfiability-based Product Configurator | Johannes Werner, Tomáš Balyo, Markus Iser, Michael Klein | 23rd Configuration Workshop (ConfWS 2021) | 2021 |
SAT Competition 2020 | Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda | Artificial Intelligence Journal (AIJ) | 2021 |
Collaborative Management of Benchmark Instances and their Attributes | Markus Iser, Luca Springer, Carsten Sinz | arXiv preprint | 2020 |
Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions | Editors: Tomáš Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda | University of Helsinki, Department of Computer Science | 2020 |
Recognition and Exploitation of Gate Structure in SAT Solving (Dissertation) | Markus Iser | Karlsruhe Institute of Technology, Germany | 2020 |
Memory Efficient Parallel SAT Solving with Inprocessing | Markus Iser, Tomáš Balyo, Carsten Sinz | IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI 2019) | 2019 |
Candy for SAT Race 2019 | Markus Iser, Felix Kutzner | SAT RACE 2019 | 2019 |
Systematic Analysis of Experiments in Solving Boolean Satisfiability Problems | Markus Iser | Deduktionstreffen | 2019 |
Integrating Static Code Analysis Toolchains | Matthias Kern, Ferhat Erata, Markus Iser, Carsten Sinz, Frederic Loiret, Stefan Otten, Eric Sax | IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC) | 2019 |
A Problem Meta-Data Library for Research in SAT | Markus Iser, Carsten Sinz | Proceedings of Pragmatics of SAT | 2019 |
Using Gate Recognition and Random Simulation for Under-Approximation and Optimized Branching in SAT Solvers | Markus Iser, Felix Kutzner, Carsten Sinz | IEEE 29th International Conference on Tools with Artificial Intelligence (ICTAI 2017) | 2017 |
System Description of Candy Kingdom - A Sweet Family of SAT Solvers | Markus Iser, Felix Kutzner | SAT COMPETITION 2017 | 2017 |
SAT Race 2015 | Tomáš Balyo, Armin Biere, Markus Iser, Carsten Sinz | Journal of Artificial Intelligence | 2016 |
Beans and Eggs - Proteins for Glucose 3.0 | Markus Iser | SAT COMPETITION 2016 | 2016 |
Recognition of Nested Gates in CNF Formulas | Markus Iser, Norbert Manthey, Carsten Sinz | International Conference on Theory and Applications of Satisfiability Testing (SAT 2015) | 2015 |
Minimizing Models for Tseitin-Encoded SAT Instances | Markus Iser, Carsten Sinz, Mana Taghdiri | International Conference on Theory and Applications of Satisfiability Testing (SAT 2013) | 2013 |
Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod | Markus Iser, Mana Taghdiri, Carsten Sinz | International Conference on Theory and Applications of Satisfiability Testing (SAT 2012) | 2012 |
MiniSAT 09z for SAT-Competition 2009 | Markus Iser | SAT 2009 competitive events booklet | 2009 |
Problem-Sensitive Restart Heuristics for the DPLL Procedure | Carsten Sinz, Markus Iser | International Conference on Theory and Applications of Satisfiability Testing (SAT 2009) | 2009 |
Supervised Thesises
Title | Student | Date | Type |
---|---|---|---|
Automated Tuning and Portfolio Selection for SAT Solvers | Tobias Fuchs | Mai 2023 | Master Thesis |
Product Configuration as a MaxSMT Problem | Björn Ehrlinspiel | Apr. 2023 | Master Thesis (external) |
Fuzzy Clause Weights Through Trail Sampling | Achim Kriso | Mar. 2023 | Master Thesis |
Construction of Binary Decision Diagrams | Maxim Popov | Nov. 2022 | Master Thesis (external) |
Predicting Hardness and Runtime of SAT Instances | Sajjad Ahmad | Nov. 2022 | Master Thesis (external) |
Feature Importance in SAT Instance Classification | Elizaveta Danilova | Aug. 2022 | Bachelor Thesis |
Decision Heuristics in a Constraint-based Product Configurator | Matthias Gorenflo | Jun. 2022 | Master Thesis (external) |
A Novel SAT Solver Architecture | Thomas Barthel | Jun. 2022 | Master Thesis (external) |
Cluster Analysis for SAT Instances | Paul Ferdinand Heinen | Feb. 2022 | Bachelor Thesis |
Asynchronous Clause Exchange for Malleable SAT Solving | Malte Sönnichsen | Feb. 2022 | Master Thesis |
Selecting SAT Instances to Evaluate Solvers | Youheng Lü | Jul. 2021 | Bachelor Thesis |
Massively Parallel Software Verification with Mallob and LLBMC | Christian Solomon | Feb. 2021 | Bachelor Thesis |
Integer Arithmetic in SAT-based Product Configuration | Nik Böttger | Jun. 2020 | Master Thesis (external) |
Explainable k-Portfolios of SAT-Solvers | Luc Mercatoris | Apr. 2021 | Bachelor Thesis |
Efficient Approximation of Implicated Literals Applied in SAT-based Product Configuration | Johannes Werner | Dec. 2020 | Master Thesis (external) |
Recognition of Constraints in CNF Formulas | Robin Link | Oct. 2020 | Bachelor Thesis |
Controlling Heuristics in CDCL SAT Solving with Adaptive Centrality Computations | Norbert Blümle | Jan. 2020 | Master Thesis |
Automated Analysis of Runtime Experiments in SAT Solving | Benjamin-Philipp Roth | Nov. 2019 | Bachelor Thesis |
Exploiting Gate Structure to Direct CDCL Search via Variable Selection and Approximation | Felix Kutzner | Jun. 2016 | Diploma Thesis |
Kodierungen zur Lösung von Ressourcen-abhängigen Terminplanungsproblemen mittels Integer Linear Programming | Norbert Blümle | Nov. 2015 | Bachelor Thesis |
SAT-based Solutions to the Resource-constrained Project Scheduling Problem | Christian Ammann | Nov. 2015 | Bachelor Thesis |
SAT-basierte Lösungsverfahren für das Discrete Tomography Problem: Eine vergleichende Untersuchung | Rosina Kazokova | Jan. 2015 | Bachelor Thesis |