Matti Jarvisalo

Matti Järvisalo

Helsinki Institute for Information Technology

[News and Highlights] [Research] [Publications] [Activities] [Teaching]

Associate Professor of Computer Science
Academy Research Fellow
Academy of Finland, 9/2014-8/2019
Principal Investigator
Constraint Reasoning and Optimization
Docent
Department of Computer Science
Faculty of Science
University of Helsinki

Education
D.Sc.(Tech.) with distinction, 2008
Helsinki University of Technology TKK
[TKK is part of Aalto University since 2010.]
Lic.Sc. (Tech.), 2007, TKK
M.Sc. (Tech.) with distinction, 2004, TKK

Postal Address:	Department of Computer Science / HIIT P.O. Box 68 FI-00014 University of Helsinki Finland
Office:	Room A312, 3rd floor of Exactum, wing A Gustaf Hällströmin katu 2b
Telephone:	+358 50 3199 248
Email:	matti.jarvisalohelsinki.fi

I lead the Constraint Reasoning and Optimization Group at the University of Helsinki.

Interested in a part-time or full-time research assistant position aiming at a Master's thesis?
We are constantly looking 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.

News

See also recent work for new publications.

Starting 1/2018 I'm on the University of Helsinki tenure track as Associate Professor of computer science.
I will chair the 8th Pragmatics of SAT workshop together with Daniel Le Berre at the Federated Logic Conference (FLoC) 2018 in Oxford, UK.
In 2019, I am on the senior PC of AAAI 2019 and on the PC of SAC 2019 KRR track.
In 2018, I am on the PCs of IJCAI-ECAI 2018, AAAI 2018, NIPS 2018 ("reviewer"), CPAIOR 2018, SAT 2018, ICTAI 2018 SAT/CP track, SAC 2018 KRR track, and RCRA 2018.
I'm a member of the Finnish Center for Artificial Intelligence (FCAI) that started in the beginning of 2018.
My project Harnessing Constraint Reasoning for Structure Discovery runs for the years 2015-2018 under the three-year research project funding scheme of the University of Helsinki.
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

I was a member of the COIN Finnish Centre of Excellence in Computational Inference Research (2012-2017).
I served on the steering committee of SAT during 2013-2017.
Invited talk at IJCAI-16: Early Career Spotlight
I gave a AAAI 2016 tutorial Algorithms for Maximum Satisfiability with Applications to AI together with Fahiem Bacchus.
I was Guest Editor (with Marijn Heule) of a special issue of Journal of Satisfiability, Boolean Modeling and Computation in 2014-2015.
I was PC Chair of SAT 2013 - 16th International Conference on Theory and Applications of Satisfiability Testing, July 8-12 2013 in Helsinki, Finland.
I was conferred the title Adjunct Professor (dosentti in Finnish) in computer science at University of Helsinki in May 2012.
I received the Best Researcher Award in 2011 by the Department of Computer Science at University of Helsinki.
I was the PI of an Academy of Finland Postdoctoral project during 2010-2013.
During April-September 2009 I visited Prof. Armin Biere's Institute for Formal Models and Verification at Johannes Kepler University Linz, Austria.
I defended my doctoral thesis Structure-Based Satisfiability Checking: Analyzing and Harnessing the Potential in November 2008.
The official opponent was Prof. Bart Selman (Cornell). Pre-examiners were Prof. Paul Beame and Prof. Joao Marques-Silva, and the supervisor Prof. Ilkka Niemelä.

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

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

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)

Finnish Centre of Excellence in Computational Inference Research COIN (2012-2017), Academy of Finland (member)
Lightweight Formal Methods for Distributed Component-based Embedded Systems (2009), Tekes (member)
Methods for Constructing and Solving Large Constraint Models (2008-2009), Academy of Finland (member)
Advanced Constraint Programming Techniques for Large Structured Problems (2005-2007), Academy of Finland (member)
Applications of Rule-Based Constraint Programming (2002-2005), Academy of Finland (member)

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

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, TPLP (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, International Journal of 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]
Pakota: A System for Enforcement in Abstract Argumentation, JELIA 2016 [pdf]
Causal Discovery from Subsampled Time Series Data by Constraint Optimization, PGM 2016 [pdf]
Impact of SAT-Based Preprocessing on Core-Guided MaxSAT Solving, CP 2016 [pdf]
Subsumed Label Elimination for Maximum Satisfiability, ECAI 2016 [pdf]
Synthesizing Argumentation Frameworks from Examples, ECAI 2016 [pdf]
Optimal Status Enforcement in Abstract Argumentation, IJCAI 2016 [pdf]
LMHS: A SAT-IP Hybrid MaxSAT Solver, SAT 2016 [pdf]
Implicit Hitting Set Algorithms for Reasoning beyond NP, KR 2016 [pdf]
Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation, AAAI 2016 [pdf]
Separating OR, SUM, and XOR circuits, J. Computer and System Sciences (2016 [pdf]
Synchronous Counting and Computational Algorithm Design, J. Computer and System Sciences (2016) [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

Steering Committee Memberships

SAT: International Conferences on Theory and Applications of Satisfiability Testing, 2013-2017.

Program Committee Chairing, Editorships, Senior PC Memberships

Senior PC Member, AAAI 2019: 33rd AAAI Conference on Artificial Intelligence
Program Committee Chair, PoS 2018: 9th International Workshop on Pragmatics of SAT, Oxford, UK.
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
Program Committee Chair, SAT 2013: 16th International Conference on Theory and Applications of Satisfiability Testing, Helsinki, Finland

Program Committee Memberships

SAC 2019: 34th ACM/SIGAPP Symposium On Applied Computing KRR track
AAAI 2018: 32nd AAAI Conference on Artificial Intelligence
CPAIOR 2018: 15th International Conference on Integration of AI and OR Techniques in Constraint Programming
ICTAI 2018: 30th IEEE International Conference on Tools with Artificial Intelligence SAT/CSP Track
IJCAI-ECAI 2018: 27th International Joint Conference on Artificial Intelligence and the 23rd European Conference on Artificial Intelligence
NIPS 2018: 32nd Annual Conference on Neural Information Processing Systems ("Reviewer")
SAT 2018: 21st International Conference on Theory and Applications of Satisfiability Testing
SAC 2018: 33rd ACM/SIGAPP Symposium On Applied Computing KRR track
RCRA 2018: 25th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
CP/ICLP/SAT DP 2017: CP/ICLP/SAT Doctoral Program 2017
ICTAI 2017: 29th IEEE International Conference on Tools with Artificial Intelligence SAT/CSP Track
AAAI 2017: 31st AAAI Conference on Artificial Intelligence
CPAIOR 2017: 14th International Conference on Integration of AI and OR Techniques in Constraint Programming
RCRA 2017: 24th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
IEA/AIE 2017: 30th International Conference on Industrial, Engineering, and Other Applications of Applied Intelligent Systems Special Track on Applications of Argumentation
SAT 2016: 19th International Conference on Theory and Applications of Satisfiability Testing
AAAI 2016: 30th AAAI Conference on Artificial Intelligence
AAAI 2016 Beyond NP: AAAI-16 Workshop on Beyond NP
SAT PoS 2016: 7th Workshop on Pragmatics of SAT
CP 2016 DP: 22nd International Conference on Principles and Practice of Constraint Programming Doctoral Program
IJCAI 2015: 24th International Joint Conference on Artificial Intelligence Main Track
IJCAI 2015 ML: 24th International Joint Conference on Artificial Intelligence Machine Learning Track
AAAI 2015: 29th AAAI Conference on Artificial Intelligence
SAT 2015: 18th International Conference on Theory and Applications of Satisfiability Testing
RCRA 2015: 22nd RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
CP 2015 DP: 21st International Conference on Principles and Practice of Constraint Programming Doctoral Program
ECAI 2014: 21st European Conference on Artificial Intelligence
SAT 2014: 17th International Conference on Theory and Applications of Satisfiability Testing
ECAI CoCoMile 2014: 3rd Workshop on Combining Constraint Solving with Mining and Learning
ICLP-SAT LaSh 2014: 4th International Workshop on Logic and Search
CP 2014 DP: 20th International Conference on Principles and Practice of Constraint Programming Doctoral Program
IJCAI 2013: 23rd International Joint Conference on Artificial Intelligence
AAAI CoCoMile 2013: 2nd Workshop on Combining Constraint Solving with Mining and Learning
RCRA 2013: 20th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
ICLP 2013 DC: 9th ICLP Doctoral Consortium
AAAI 2012: 26th AAAI Conference on Artificial Intelligence
ECML-PKDD 2012: European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases
ECAI CoCoMile 2012: 1st Workshop on Combining Constraint Solving with Mining and Learning
ICLP LoCoCo 2012: 3rd Workshop on Logics for Component Configuration
KR NMR 2012: 14th International Workshop on Non-Monotonic Reasoning
SAT PoS 2012: 3rd Workshop on Pragmatics of SAT
IJCAI 2011: 22nd International Joint Conference on Artificial Intelligence
SAT PoS 2011: 2nd Workshop on Pragmatics of SAT
SAT LoCoCo 2010: 1st Workshop on Logics for Component Configuration

Organization

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:

Artificial Intelligence - 2018, 2015, 2014, 2013, 2012, 2011, 2010
Annals of Mathematics and Artificial Intelligence - 2018, 2014
International Journal of Approximate Reasoning - 2017
Journal of Artificial Intelligence Research - 2017, 2015
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):

ICDCN: International Conference on Distributed Computing and Networking - 2015
ISAIM: International Symposium on Artificial Intelligence and Mathematics - 2014
STACS: Symposium on Theoretical Aspects of Computer Science - 2013
FMCAD: International Conference on Formal Methods in Computer-Aided Design - 2012, 2010
ICDE: IEEE International Conference on Data Engineering - 2012
LPAR: International Conference on Logic for Programming, Artificial Intelligence and Reasoning - 2012
SAT: International Conference on Theory and Applications of Satisfiability Testing - 2012, 2011, 2010, 2005
TACAS: International Conference on Tools and Algorithms for the Construction and Analysis of Systems - 2012, 2010
AAAI: AAAI Conference on Artificial Intelligence - 2011, 2010
ICLP: International Conference on Logic Programming - 2011
LICS: IEEE Symposium on Logic in Computer Science - 2011
JELIA: European Conference on Logics for Artificial Intelligence - 2010
SMT: International Workshop on Satisfiability Modulo Theories - 2009
PADL: International Symposium on Practical Aspects of Declarative Languages - 2009
TIME: International Symposium on Temporal Representation and Reasoning - 2007
CADE: International Conference on Automated Deduction - 2005

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).

Grant for post-doctoral research visit abroad, Finnish Foundation for Technology Promotion TES (2009)
Nokia Scholarship, Nokia Foundation (2007)
Grant for doctoral studies, Jenny and Antti Wihuri Foundation (2007)
Grant for doctoral studies, Finnish Foundation for Technology Promotion TES (2008, 2006)
Grant for doctoral studies, Emil Aaltonen Foundation (2005)
Funded graduate school position for 2005-2008, Helsinki Graduate School in Computer Science and Engineering (HeCSE)

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:

Automated Logical Reasoning (5 ECTS), spring 2019 (planned)
Combinatorial Optimization (5 ECTS), autumn 2018 (planned)
Seminar on Automated Planning (5 ECTS), autumn 2018 (planned)
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