Matti Jarvisalo
Matti Järvisalo
|
|
|
|
|
[News and Highlights] [Research] [Publications] [Activities] [Teaching]
I lead the
Constraint Reasoning
and Optimization Group
at the University of Helsinki.
News
See also recent work for new publications.
Earlier Highlights
|

M. Järvisalo, A. Van Gelder (eds.), LNCS 7962, Springer, 2013.
|
Research
Research Interests
Boolean satisfiability and generalizations,
decision procedures, constraint satisfaction, combinatorial/discrete optimization,
automated reasoning, artificial intelligence, operations research,
knowledge representation, complexity of reasoning, computational aspects of argumentation,
probabilistic graphical models, structure discovery, ...
Awards and Honors
- 2019 IJCAI-JAIR Best Paper Prize
- University of Helsinki 2019 Doctoral Dissertation Award to my PhD student Jeremias Berg
- PGM 2018 Best Student Paper Award to my PhD student Kari Rantanen
- CP 2017 Distinguished Paper Award
- Invited paper at AAAI 2017 in the What's Hot track.
- IJCAI 2016 Early Career Spotlight
as one of 22 (6 within Europe) most active early career researchers in all representative areas of AI.
- ECAI 2016 Runner-Up Best Student Paper Award to my PhD student Andreas Niskanen
-
Best solver at MaxSAT Evaluation 2015 on industrial and crafted weighted partial MaxSAT instances
for our solver LMHS.
-
ICCMA 2015 Honorary Mention at
for our Cegartix solver
-
KR 2012 Distinguished Student Paper Prize
-
2011 Best Researcher Award at Department of Computer Science,
University of Helsinki.
-
CP 2007 runner-up for the CP'07 Best Paper Award
-
ICLP 2007 Best Student Paper Award
Projects
-
Declarative Boolean Optimization: Pushing the Envelope (9/2019-8/2023; PI)
funded by Academy of Finland (Academy project funding for early-career researchers)
- Symbolic Reasoning for Formally Verified and Explainable AI (2020-2022; PI)
funded by Academy of Finland (ICT 2023 Autonomous Everything)
-
Decision Procedures for the Polynomial Hierarchy,
Boolean Optimization, and Model Counting (9/2014-8/2019; PI),
funded by Academy of Finland (Academy Research Fellow funding scheme)
-
Harnessing Constraint Reasoning for Structure Discovery (2015-2018; PI),
Research Funds of the University of Helsinki (Three-year Research Projects
funding scheme)
-
Extending the Reach of Boolean Constraint Reasoning
(1/2010-4/2013; PI),
Academy of Finland
(Postdoctoral Project funding scheme)
Publications
A complete list of my publications with downloadable papers and bibtex entries
is available both
by year and
by type.
External sources:
DBLP entry,
Google Scholar profile,
Semantic Scholar,
Orcid ID 0000-0003-2572-063X (incomplete data),
Scopus Author ID 23397451200 (incomplete data).
Some recent work
- SAT-based Judgment Aggregation, AAMAS 2023
[pdf]
- Incremental Maximum Satisfiability, SAT 2022
[pdf]
- MaxSAT-Based Bi-Objective Boolean Optimization, SAT 2022
[pdf]
- Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization, SAT 2022
[pdf]
- Clause Redundancy and Preprocessing in Maximum Satisfiability, IJCAR 2022
[pdf]
- Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework, KR 2022
[pdf]
- Algorithms for Reasoning in a Default Logic Instantiation of Assumption-Based Argumentation, COMMA 2022
[pdf]
- Computing Smallest MUSes of Quantified Boolean Formulas, LPNMR 2022
[pdf]
- Maximum Satisfiability, SAT Handbook (2021)
[pdf]
- Preprocessing in SAT Solving, SAT Handbook (2021)
[pdf]
- SAT Competition 2020, Artificial Intelligence (2021)
[pdf]
- Acceptance in Incomplete Argumentation Frameworks, Artificial Intelligence (2021)
[pdf]
- Declarative Algorithms and Complexity Results for Assumption-Based Argumentation, J. Artificial Intelligence Research (2021)
[pdf]
- Maximal Ancestral Graph Structure Learning via Exact Search, UAI 2021
[pdf]
- Harnessing Incremental Answer Set Solving for Reasoning in Assumption-Based Argumentation, ICLP 2021
[pdf]
- Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters, CP 2021
[pdf]
- Pseudo-Boolean Optimization by Implicit Hitting Sets, CP 2021
[pdf]
- Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT under Changing Weights, CP 2021
[pdf]
- Refined Core Relaxation for Core-Guided MaxSAT Solving, CP 2021
[pdf]
- Discovering Causal Graphs with Cycles and Latent Confounders: An Exact Branch-and-Bound Approach,
Int. J. Approximate Reasoning (2020)
[pdf]
- Controllability of Control Argumentation Frameworks, IJCAI-PRICAI 2020
[pdf]
- Finding Periodic Apartments via Boolean Satisfiability and Orderly Generation, LPAR 2020
[pdf]
- Finding Most Compatible Phylogenetic Trees over Multi-State Characters, AAAI 2020
[pdf]
- Deciding Acceptance in Incomplete Argumentation Frameworks, AAAI 2020
[pdf]
- Preprocessing in Incomplete MaxSAT Solving, ECAI 2020
[pdf]
- Learning Chordal Markov Networks via Stochastic Local Search, ECAI 2020
[pdf]
- Algorithms for Dynamic Argumentation Frameworks: An Incremental SAT-Based Approach, ECAI 2020
[pdf]
- Strong Refinements for Hard Problems in Argumentation Dynamics, ECAI 2020
[pdf]
- An Answer Set Programming Approach to Argumentative Reasoning in the ASPIC+ Framework, KR 2020
[pdf]
- Smallest Explanations and Diagnoses of Rejection in Abstract Argumentation, KR 2020
[pdf]
- μ-toksia: An Efficient Abstract Argumentation Reasoner, KR 2020
[pdf]
- Learning Optimal Cyclic Causal Graphs from Interventional Data, PGM 2020
[pdf]
Research-Related Software
See here.
Professional Activities
Editorial Board Memberships
Steering Committee Memberships
Organization
Competitions:
- Co-organizer, SAT Competition
2022,
2021,
2020,
2018,
2017,
2016,
2014,
2013,
2011
- Co-organizer, MaxSAT Evaluation
2022,
2021,
2020,
2019,
2018,
2017
- Co-organizer, SAT Race 2019
- Co-organizer, SAT Challenge 2012
Conferences:
- Local Chair, FoIKS 2022: 12th International Symposium on Foundations of Information and Knowledge Systems
, June 20-23, 2022, Helsinki, Finland
- Local Chair, SAT 2013:
16th International
Conference on Theory and
Applications of Satisfiability Testing, July 8-12, 2013, Helsinki, Finland
- Co-organizer, SAT-SMT Summer School 2013
- Local organizer, SWAT 2012:
13th Scandinavian Symposium and Workshops on Algorithm Theory, July 4-6, 2012, Helsinki, Finland
- Local Chair, JELIA 2010:
12th European Conference on
Logics in Artificial Intelligence,
September 13-15, 2010, Helsinki, Finland
Program Committee Chairing, Guest Editorials, Senior PC Memberships
- Applications and Systems Track Chair, KR 2023: 20th International Conference on Principles of Knowledge Representation and Reasoning
(together with Francesco Ricca)
- PC Chair, PoS 2022: 13th International Workshop on Pragmatics of SAT (together with Daniel Le Berre)
- Senior PC Member, IJCAI 2021: 30th International Joint
Conference on Artificial Intelligence
- PC Chair, PoS 2021: 12th International Workshop on Pragmatics of SAT,
online (together with Daniel Le Berre)
- Demo Track Chair, IJCAI-PRICAI 2020: 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence, Yokohama, Japan
-
PC Chair, PoS 2020: 11th International Workshop on Pragmatics of SAT,
Alghero, Italy (together with Daniel Le Berre)
- Senior PC Member, IJCAI-PRICAI 2020: 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence
-
PC Chair, PoS 2019: 10th International Workshop on Pragmatics of SAT,
Lisbon, Portugal (together with Daniel Le Berre)
- Senior PC Member, IJCAI 2019: 28th International Joint
Conference on Artificial Intelligence
- Senior PC Member, AAAI 2019: 33rd
AAAI Conference on Artificial Intelligence
-
PC Chair, PoS 2018: 9th International Workshop on Pragmatics of SAT, Oxford, UK
(together with Daniel Le Berre)
- Senior PC Member, IJCAI 2016: 25th International Joint
Conference on Artificial Intelligence
- Guest Editor, Journal of Satisfiability,
Boolean Modeling and Computation,
Special Issue on the SAT 2014 Competitions and Evaluations, 2015
-
PC Chair, SAT 2013: 16th International Conference on Theory and
Applications of Satisfiability Testing, Helsinki, Finland (together with Allen Van Gelder)
Program Committee Memberships
Reviewing
Reviewed scientific manuscripts for
journals
Journal of Artificial Intelligence Research,
Journal of Universal Computer Science,
Artificial Intelligence,
Annals of Mathematics and Artificial Intelligence,
International Journal of Approximate Reasoning,
Theory and Practice of Logic Programming,
IEEE Intelligent Systems,
Information Sciences,
Journal of Automated Reasoning,
Journal of Experimental and Theoretical Artificial Intelligence,
Journal on Satisfiability, Boolean Modeling and Computation,
AI Communications,
Journal of Logic and Computation (and various conferences).
Teaching
To prospective students: If you're interested in conducting research
aiming at a thesis under my guidance, feel free to contact me
via email. To get a feel for possible topic areas, see my research
interests above. You can also have a look at my publications.
Teaching
Lectured (teacher-in-charge of) the following courses at the University of Helsinki:
- Bachelor's Thesis Project, spring 2023 (supervisor)
- Seminar on Automated Reasoning and Optimization (5 ECTS), spring 2023
- Combinatorial Optimization (5 ECTS), autumn 2022
- Automated Logical Reasoning (5 ECTS), spring 2022
- Seminar on Logic-Enabled Verified and Explainable AI (5 ECTS), autumn 2021
- Bachelor's Thesis Project, autumn 2021 (supervisor)
- Automated Logical Reasoning (5 ECTS), spring 2021
- Combinatorial Optimization (5 ECTS), autumn 2020
- Bachelor's Thesis Project, spring 2020 (supervisor)
- Seminar on Model Checking (5 ECTS), autumn 2019
- Automated Logical Reasoning (5 ECTS), spring 2019
- Seminar on Discrete Algorithms (5 ECTS),
spring 2019 (with Juha Kärkkäinen and Veli Mäkinen)
- Combinatorial Optimization (5 ECTS), autumn 2018
- Seminar on Automated Planning (5 ECTS), autumn 2018
- Seminar on Applied Discrete Algorithms A (5 ECTS),
spring 2018 (with Juha Kärkkäinen and Veli Mäkinen)
- Bachelor's Thesis Project, spring 2018 (supervisor)
- Seminar on Computational Social Choice (3 ECTS),
autumn 2016.
MSc-level seminar course based on the recent Handbook of Computational Social Choice. Topics included voting theory,
fair allocation, coalition formation (matchings and hedonic games), and automated theorem discovery.
- Satisfiability, Boolean Modeling and Computation (5 ECTS),
spring 2016.
Central computational aspects of SAT, focusing on techniques that are important for modern real-world applications of SAT. Topics included: basics of propositional logic and computation; modern SAT solver algorithms and search techniques; preprocessing; modelling real-world problems as SAT; building complex SAT-based procedures for Boolean optimization and other search problems beyond NP.
-
Seminar on Tractability (3 ECTS),
autumn 2015.
MSc-level seminar course based on the recent book Tractability: Practical Approaches to Hard Problems.
Fundamental concepts and state-of-the-art techniques to tame intractability. Topics included: tractability in terms of graphical structures underlying problems, language restrictions, approximation algorithms, and kernelization methods, as well as utilizing heuristics in modern SAT-solvers.
-
Satisfiability, Boolean Modeling and Computation (3 ECTS),
intensive course in May 2015
Central computational aspects of Boolean satisfiability (SAT), focusing on techniques that are important for modern real-world applications of SAT.
-
Seminar:
Constraint Solving Meets Machine Learning and Data Mining (3 ECTS),
spring 2013.
A snapshot into the current state of forefront research in the intersection of constraint solving, machine learning and data mining.
-
Discrete Optimization Project (2 ECTS),
spring 2012.
Independent hands-on project work in the areas of constraint satisfaction and discrete optimization, involving problem modelling, algorithm implementation, and/or practical performance evaluation of search and optimization algorithms within a chosen topic.
-
Discrete Optimization (3 ECTS),
autumn 2011.
Combinatorial search spaces and optimization problems. Exhaustive and heuristic methods. Linear and integer programming.
-
Seminar on Boolean Constraint Reasoning (3 ECTS),
autumn 2010.
Theoretical and applied aspects of Boolean satisfiability, SAT
solvers and their extensions.
Previously, I've been involved as TA on:
-
Advanced Course in Computational Logic,
Helsinki University of Technology, spring 2009,
2008,
2007
2006
Modal logics, applications of temporal logics (LTL, CTL) in concurrent and
distributed systems
-
Computational Complexity Theory,
Helsinki University of Technology, autumn 2008,
2007,
2006,
2005,
2004,
2003
NP-completeness, randomized algorithms, cryptography, approximation
algorithms, parallel algorithms, polynomial hierarchy, PSPACE-completeness
-
Logic in Computer Science: Foundations,
Helsinki University of Technology,
spring 2007,
autumn 2003
Propositional logic and predicate logic, proof theory and
applications
-
Introduction to Theoretical Computer Science Y,
Helsinki University of Technology,
spring 2006
-
Introduction to Theoretical Computer Science T
spring 2006,
2005,
2004: autumn,
spring,
2002: autumn,
spring
Finite automata and regular languages, context-free grammars and pushdown
automata, Turing machines
-
Seminar on Theoretical Computer Science,
Helsinki University of Technology,
spring 2003:
Propositional Satisfiability Checking Techniques
-
Basic Course in Programming L1,
Helsinki University of Technology, autumn 2001