Dr. Ashlin Iser

Efficient Symbolic Reasoning and Trustworthy AI – Karlsruhe Institute of Technology (KIT)

Academic expertise in algorithm engineering and automated reasoning, grounded in over 20 years of hands-on software engineering – from bare-metal performance optimization to full-stack system design. I design algorithms and heuristics that make intractable combinatorial optimization problems tractable, and I work at the intersection of AI for reasoning and reasoning for AI.

🔬 Research Interests

I specialize in Efficient Symbolic Reasoning (SAT/SMT, combinatorial optimization, constraint solving, planning, and scheduling) and its two-way relationship with machine learning: AI for reasoning – data-driven algorithm selection, configuration, and tuning to push solvers to peak performance – and reasoning for AI – Trustworthy, Explainable AI that makes learned models verifiable and interpretable, with an emerging interest in Neuro-Symbolic architectures that ground them in sound solvers via autoformalization and solver-in-the-loop pipelines. My work spans high-performance solver engineering for large-scale combinatorial problems and their real-world applications, such as planning, scheduling, software verification, and formal explainability.

📈 Engagement

Professional Activities: Organizer of the International SAT Competitions (2015; annually since 2020); active program committee member (e.g., SAT, ECAI) and reviewer for leading journals (e.g., AIJ, NCOMMS).

Teaching & Mentorship: Focused on graduate-level courses (including Practical SAT Solving with an LQI of 100, and the Recent Advances in SAT Solving seminar) along with mentoring research and software engineering projects. Experienced in organizing large-scale undergraduate lab courses (Algorithms, Programming) with up to 700 participants.

Supervision: Over 30 completed theses (Bachelor, Master, Diploma), split between academic, research-focused topics at the institute and industry-partnered collaborations (CAS Software AG, PLANTA Projekt-Management Systeme GmbH).

Publications: 24 peer-reviewed papers (journals, conferences & workshops), listed on my Google Scholar profile.

Open Source: All projects on my GitHub profile are open source, most notably the Global Benchmark Database (GBD).

🛠 Technical Expertise

Algorithm & Performance Engineering: Bare-metal and low-level optimization, high-performance solver engineering for large-scale combinatorial problems, and parallel algorithm design.

Full-Stack & Architecture: End-to-end system design spanning algorithmic backends, web frontends, and relational data modeling.

Technologies: High Performance Computing (HPC), Constraint & Logic Solving, Database Systems and Modeling, Machine Learning, Software Testing, Static Code Analysis.

Languages & Tools: C++, Python, SQL, C, Java, diverse Scripting Languages and Web Technologies, and extensive experience with Linux environments.

📚 Selected Publications

Sustainable Benchmarking Tool (2026, SAT)
Ashlin Iser, Marie Anastacio, Théo Matricon, Laurent Simon, Holger H. Hoos

Active Learning for SAT Solver Benchmarking (2025, JAR)
Tobias Fuchs, Jakob Bach, Ashlin Iser

Global Benchmark Database (SAT 2024)
Ashlin Iser, Christoph Jabs

Oracle-Based Local Search for Pseudo-Boolean Optimization (ECAI 2023)
Ashlin Iser, Jeremias Berg, Matti Järvisalo

A Comprehensive Study of k-Portfolios of Recent SAT Solvers (SAT 2022)
Jakob Bach, Ashlin Iser, Klemens Böhm

Unit Propagation with Stable Watches (CP 2021)
Ashlin Iser, Tomáš Balyo

SAT Competition 2020 (AIJ 2021)
Nils Froleyks, Marijn Heule, Ashlin Iser, Matti Järvisalo, Martin Suda