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
- 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
- PC Chair, PoS 2022: 13th International Workshop on Pragmatics of SAT,
online (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 - 2019, 2017, 2015
- Journal of Universal Computer Science - 2019
- Artificial Intelligence - 2018, 2015, 2014, 2013, 2012, 2011, 2010
- Annals of Mathematics and Artificial Intelligence - 2018, 2014
- International Journal of Approximate Reasoning - 2017
- Theory and Practice of Logic Programming - 2017, 2016
- IEEE Intelligent Systems - 2016
- Information Sciences - 2015
- Journal of Automated Reasoning - 2015
- Journal of Experimental and Theoretical Artificial Intelligence - 2014, 2013
- Journal on Satisfiability, Boolean Modeling and Computation - 2012, 2011
- AI Communications - 2010
- Journal of Logic and Computation - 2008
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:
- 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