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.
Looking for a research-oriented Master's thesis topic, with a possibility of
a part-time or full-time research assistant position?
We are always on the lookout for talented students with
- a CS background, especially in algorithms/machine learning;
- a Math / Operations Research background, especially in optimization/logic/complexity, with interest in algorithms; and/or
- strong implementation skills (C/C++) who are motivated by challenging programming tasks
to work with us on forefront research problems within the
Constraint Reasoning
and Optimization Group.
For more information, contact me by email.
Disclaimer: Apart from truly exceptional cases, internships are only available to
student locally in the Helsinki region. I am not able to respond to every international query about internship opportunities.
In case you are interested in a postdoc position and already have a proven track record in (PhD-level) research areas
closely related to my group's work, feel free to contact me by email with your CV to enquire possible opportunities.
News
|
See also recent work for new publications.
- Our JAIR article Clause Elimination for SAT and QSAT has been selected as the winner of the 2019 IJCAI-JAIR Best Paper Prize as
an outstanding paper published in JAIR in the preceding five calendar years.
- I will co-chair the IJCAI-PRICAI 2020 Demo Track.
- I am editorial board member of Journal on Satisfiability, Boolean Modeling and Computation (JSAT).
- In 2020, I am on the PCs of
AAAI 2020,
FoIKS 2020,
and
SAC 2020 (KRR track).
- In 2019, I am on the senior PCs of
IJCAI 2019 and
AAAI 2019, and
on the PCs of
SAT 2019,
UAI 2019,
CPAIOR 2019,
ICML 2019,
NeurIPS 2019,
SoCS 2019,
ICTAI 2019 SAT/CSP track,
and
SAC 2019 KRR track.
Further activities are listed here.
- Starting 1/2018 I'm on the University of Helsinki tenure track as Associate Professor of computer science.
- My Academy of Finland project
Decision Procedures for the Polynomial Hierarchy,
Boolean Optimization, and Model Counting
(9/2014-8/2019) is funded under the Academy Research Fellow scheme.
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 Doctoral Dissertation Award to my student Jeremias Berg.
- Best Student Paper Award at PGM 2018 to my student Kari Rantanen.
- Distinguished Paper Award at CP 2017.
- Invited paper at AAAI 2017 in the What's Hot track.
- Early Career Spotlight at IJCAI 2016
as one of 22 (6 within Europe) most active early career researchers in all representative areas of AI.
- Runner-Up Best Student Paper Award at ECAI 2016.
-
Best solver at MaxSAT Evaluation 2015 on industrial and crafted weighted partial MaxSAT instances
for our solver LMHS.
-
Honorary Mention at ICCMA 2015,
for our Cegartix solver
-
Distinguished Student Paper Prize at KR 2012.
-
Best Researcher Award in 2011, Department of Computer Science,
University of Helsinki.
-
Runner-up for the CP'07 Best Paper Award at CP 2007.
-
Best Student Paper award at ICLP 2007.
Projects
-
Declarative Boolean Optimization: Pushing the Envelope (9/2019-8/2023; PI)
funded by Academy of Finland (Academy project funding for early-career researchers)
-
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
- Synthesizing Argumentation Frameworks from Examples, J. Artificial Intelligence Research (2019)
[pdf]
- MaxSAT Evaluation 2019: New Developments and Detailed Results, J. Satisfiability, Boolean Modeling and Computation (2019)
[pdf]
- SAT Competition 2019, J. Satisfiability, Boolean Modeling and Computation (2019)
[pdf]
- Enumerating Potential Maximal Cliques via SAT and ASP, IJCAI 2019
[pdf]
- Centrality Heuristics for Exact Model Counting, ICTAI 2019
[pdf]
- Solving Graph Problems via Potential Maximal Cliques: An Experimental Evaluation of the Bouchitté-Todinca Algorithm,
ACM J. Experimental Algorithmics (2019) [pdf]
- Reasoning over Assumption-Based Argumentation Frameworks via Direct Answer Set Programming Encodings,
AAAI 2019 [pdf]
- Unifying Reasoning and Core-Guided Search for Maximum Satisfiability,
JELIA 2019 [pdf]
- Preprocessing Argumentation Frameworks via Replacement Patterns,
JELIA 2019 [pdf],
- A Hybrid Approach to Optimization in Answer Set Programming,
KR 2018 [pdf]
- Extension Enforcement under Grounded Semantics in Abstract Argumentation,
KR 2018 [pdf]
-
Cautious Reasoning in ASP via Minimal Models and Unsatisfiable Cores, Theory and Practice of Logic Programming (2018)
[pdf]
-
Learning Optimal Causal Graphs with Exact Search, PGM 2018
[pdf]
-
SAT-based Approaches to Adjusting, Repairing, and Computing Largest Extensions of Argumentation Frameworks, COMMA 2018
[pdf]
- Premise Set Caching for Enumerating Minimal Correction Subsets, AAAI 2018
[pdf]
- A Preference-Based Approach to Backbone Computation with Application to Argumentation, SAC 2018
[pdf]
- Empirical Hardness of Finding Optimal Bayesian Network Structures:
Algorithm Selection and Runtime Prediction, Machine Learning (2018)
[pdf]
- Learning Chordal Markov Networks via Branch and Bound, NIPS 2017
[pdf]
- A Constraint Optimization Approach to Causal Discovery from Subsampled Time Series Data,
Int. J. Approximate Reasoning (2017)
[pdf]
- Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation, J. Artificial Intelligence Research (2017)
[pdf]
- On Computing Generalized Backbones, ICTAI 2017
[pdf]
- Improving MCS Enumeration via Caching, SAT 2017
[pdf]
- MaxPre: An Extended MaxSAT Preprocessor, SAT 2017
[pdf]
- Weight-Aware Core Extraction in SAT-Based MaxSAT Solving, CP 2017
[pdf]
- Reduced Cost Fixing in MaxSAT, CP 2017
[pdf]
- Minimum-Width Confidence Bands via Constraint Optimization, CP 2017
[pdf]
- A Core-Guided Approach to Learning Optimal Causal Graphs, IJCAI 2017
[pdf]
- From Structured to Abstract Argumentation: Assumption-Based Acceptance via AF Reasoning, ECSQARU 2017
[pdf]
- Bayesian Network Structure Learning with Integer Programming: Polytopes, Facets and Complexity, J. Artificial Intelligence Research (2017)
[pdf]
- Cost-Optimal Constrained Correlation Clustering via Weighted Partial Maximum Satisfiability,
Artificial Intelligence (2017)
[pdf]
- SAT Competition 2016: Recent Developments, AAAI 2017
[pdf]
Research-Related Software
See here.
Professional Activities
Invited Talks and Tutorials
- Keynote talk at 2nd
International Workshop on Systems and Algorithms for Formal Argumentation (SAFA 2018), Poland.
- Invited talk at 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), USA: Early Career Spotlight
- Invited talk at 1st International Workshop on Argumentation in Logic Programming and Non-Monotonic Reasoning (Arg-LPNMR 2016 at IJCAI 2016), USA
- Invited lecture at 1st International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning, Portugal 2016
- Tutorial speaker at 30th AAAI Conference on Artificial Intelligence (AAAI 2016), USA
- Invited talk at Linköping University IDA Machine Learning Seminar, Sweden 2015
- Invited tutorial at Dagstuhl seminar Theory and Practice of SAT Solving, Germany 2015
- Invited tutorial at BIRS workshop Theoretical Foundations of Applied SAT Solving, Canada 2014
- Invited guest lecture at KTH CSC, Sweden 2011
- Invited talk at the KU Leuven DTAI seminar, Belgium 2011
- Invited talk at Dagstuhl seminar Algorithms and Applications for Next Generation SAT Solvers, Germany 2009
Editorial Board Memberships
Steering Committee Memberships
Program Committee Chairing, Guest Editorials, Senior PC Memberships
- 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 (together with Jia Jia)
-
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
Organization
- Co-organizer, SAT Race 2019
- Co-organizer, MaxSAT Evaluation 2019
- Co-organizer, SAT Competition 2018
- Co-organizer, MaxSAT Evaluation 2018
- Co-organizer, SAT Competition 2017
- Co-organizer, MaxSAT Evaluation 2017
- Co-organizer, SAT Competition 2016
- Co-organizer, SAT Competition 2014
- Local Chair, SAT 2013:
16th International
Conference on Theory and
Applications of Satisfiability Testing, July 8-12, 2013, Helsinki, Finland
- Co-organizer, SAT Competition 2013
- Co-organizer, SAT-SMT Summer School 2013
- Co-organizer, SAT Challenge 2012
- Local organizer, SWAT 2012:
13th Scandinavian Symposium and Workshops on Algorithm Theory, July 4-6, 2012, Helsinki, Finland
- Co-organizer, SAT Competition 2011
- Local Chair, JELIA 2010:
12th European Conference on
Logics in Artificial Intelligence,
September 13-15, 2010, Helsinki, Finland
- Organizer, HIIT Seminar Kumpula research seminar, 2010-2011
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
Conferences (not including PC memberships):
Grants
- Research grant for project
"Decision Procedures for the Polynomial Hierarchy, Boolean Optimization,
and Model Counting",
Academy of Finland (Academy Research Fellow 9/2014-8/2019).
-
Research grant for project "Harnessing Constraint Reasoning for Structure Discovery",
Research Funds of the University of Helsinki (1/2015-12/2017).
- Research grant for project
"Extending the Reach of Boolean Constraint Reasoning",
Academy of Finland (Postdoctoral project 1/2010-4/2013).
Associations
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:
- 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)
- 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