Dr. Matti Järvisalo
[News and Highlights] [Research] [Publications] [Activities] [Teaching]
I lead the
and Optimization Group
at the University of Helsinki and
(within CoSCo) at
Interested in a postdoc position in my group?
We are looking for a talented postdoc with proven potential and
a strong background in theory and/or practice to work with us on
topics related to SAT, constraints, optimization, complexity, argumentation and other KR problems, and/or
Contact me by email for more details!
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
and Optimization Group.
For more information, contact me by email.
M. Järvisalo, A. Van Gelder (eds.), LNCS 7962, Springer, 2013.
Boolean satisfiability and its generalizations,
decision procedures, constraint satisfaction, combinatorial/discrete optimization,
automated reasoning, artificial intelligence, operations research,
knowledge representation, computational/proof complexity, computational aspects of argumentation,
probabilistic graphical models, structure discovery, ...
Awards and Honors
- Paper invited to the IJCAI 2017 journal track.
- Invited paper at AAAI 2017 in the by-invitation-only 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.
Invited for fast-track publication in Artificial Intelligence
and to the award-winning track of Journal of Artificial Intelligence Research.
Best solver at MaxSAT Evaluation 2015 on industrial and crafted weighted partial MaxSAT instances
for our solver LMHS.
Honorary Mention at ICCMA 2015,
1st International Competition on Computational Models of Argumentation, for
the Cegartix solver
One of the best papers at PODC 2012. Invited to a special issue of the journal Distributed Computing.
Distinguished Student Paper Prize at KR 2012, 13th International
Conference on Principles of Knowledge Representation and Reasoning
Best Researcher Award in 2011, Department of Computer Science,
University of Helsinki.
Exceptional full paper at AAAI 2008,
23rd AAAI Conference on Artificial Intelligence. Invited for both
oral and poster presentation.
Runner-up for the CP'07 Best Paper Award at CP 2007,
13th International Conference on Principles and Practice of
Constraint Programming. Invited as one of five best papers out of
165 submissions for submission to a journal special issue dedicated to the best
papers at CP 2007.
Best Student Paper award at ICLP 2007, 23rd International
Conference on Logic Programming
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-2017; PI),
Research Funds of the University of Helsinki (Three-year Research Projects
Extending the Reach of Boolean Constraint Reasoning
Academy of Finland
(Postdoctoral Project funding scheme)
A complete list of my publications with downloadable papers and bibtex entries
is available both
by year and
Some recent work
Google Scholar profile,
Orcid ID 0000-0003-2572-063X (incomplete data),
Scopus Author ID 23397451200 (incomplete data).
- Bayesian Network Structure Learning with Integer Programming: Polytopes, Facets and Complexity, J. Artificial Intelligence Research (2017)
- Cost-Optimal Constrained Correlation Clustering via Weighted Partial Maximum Satisfiability,
Artificial Intelligence (2017)
- SAT Competition 2016: Recent Developments, AAAI 2017
- Pakota: A System for Enforcement in Abstract Argumentation, JELIA 2016
- Causal Discovery from Subsampled Time Series Data by Constraint Optimization, PGM 2016
- Impact of SAT-Based Preprocessing on Core-Guided MaxSAT Solving, CP 2016
- Subsumed Label Elimination for Maximum Satisfiability, ECAI 2016
- Synthesizing Argumentation Frameworks from Examples, ECAI 2016
- Optimal Status Enforcement in Abstract Argumentation, IJCAI 2016
- LMHS: A SAT-IP Hybrid MaxSAT Solver, SAT 2016
- Implicit Hitting Set Algorithms for Reasoning beyond NP, KR 2016
- Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation, AAAI 2016
- Separating OR, SUM, and XOR circuits, J. Computer and System Sciences (2016)
- Synchronous Counting and Computational Algorithm Design, J. Computer and System Sciences (2016)
- Re-using Auxiliary Variables for MaxSAT Preprocessing, ICTAI 2015
- Clause Elimination for SAT and QSAT,
Journal of Artificial Intelligence Research (2015)
- Do-calculus when the True Graph is Unknown, UAI 2015
- Learning Optimal Chain Graphs with Answer Set Programming, UAI 2015
- Impact of Learning Strategies on the Quality of Bayesian Networks: An Empirical Evaluation, UAI 2015
- Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT,
- Overview and Analysis of the SAT Challenge 2012 Solver Competition,
Artificial Intelligence (2015)
- MaxSAT-Based Cutting Planes for Learning Graphical Models, CPAIOR 2015
- Weak Models of Distributed Computing, with Connections
to Modal Logic, Distributed Computing (2015)
A propositional abduction solver based on the implicit hitting set paradigm
LMHS: a hybrid SAT-IP MaxSAT solver based on the implicit hitting set paradigm.
Pakota: A system for extension enforcement in abstract argumentation based on constraint optimization [AAAI'16].
- SATDiscoverer: a general SAT-based procedure for learning causal models [UAI'13].
an abstract argumentation reasoning tool based of SAT solvers [KR'12, PoS'12].
- CRSat: a circuit-level stochastic
local search method for SAT [IJCAI'11].
- Debugging tools for answer set solvers [TPLP'10]:
FuzzASP is a fuzzer that
can be used to generate random answer set programs.
DeltaASP is a
delta-debugger which is able to to automatically minimize
failure-inducing answer set programs in the syntax of lparse.
- Ensemble computation circuit generator
for generating SAT benchmarks [SAT'12].
Invited Talks and Tutorials
Steering Committee Memberships
- 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
Program Committee Chairing and Editorships
SAT: International Conferences on Theory and Applications of Satisfiability Testing
Program Committee Memberships
- Co-organizer, SAT Competition 2016
- Co-organizer, SAT Competition 2014
- Local Chair, SAT 2013:
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
Reviewed scientific manuscripts for
Conferences (not including PC memberships):
- 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).
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.
Lectured (teacher-in-charge of) the following courses:
- Seminar on Computational Social Choice (3 ECTS), University of Helsinki, 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), University of Helsinki,
Central computational aspects of SAT, focusing on techniques that are important for modern real-world applications of SAT. Topics include: 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), University of Helsinki, 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. Possible topics include the study of graphical structure of the underlying problem, language restrictions, approximation algorithms, and kernelization methods, as well as utilizing heuristics in modern SAT-solvers.
Satisfiability, Boolean Modeling and Computation (3 ECTS),
University of Helsinki, 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.
Constraint Solving Meets Machine Learning and Data Mining (3 ECTS), University of Helsinki, 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),
University of Helsinki, 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),
University of Helsinki, autumn 2011.
Combinatorial search spaces and optimization problems. Exhaustive and heuristic methods. Linear and integer programming.
Seminar on Boolean Constraint Reasoning (3 ECTS),
University of Helsinki, autumn 2010.
Theoretical and applied aspects of Boolean satisfiability, SAT
solvers and their extensions.
TA'd (held exercise sessions, prepared material, marked exams and
homework, etc) on the following courses:
Advanced Course in Computational Logic,
Helsinki University of Technology, spring 2009,
Modal logics, applications of temporal logics (LTL, CTL) in concurrent and
Computational Complexity Theory,
Helsinki University of Technology, autumn 2008,
NP-completeness, randomized algorithms, cryptography, approximation
algorithms, parallel algorithms, polynomial hierarchy, PSPACE-completeness
Logic in Computer Science: Foundations,
Helsinki University of Technology,
Propositional logic and predicate logic, proof theory and
Introduction to Theoretical Computer Science Y,
Helsinki University of Technology,
Introduction to Theoretical Computer Science T
Finite automata and regular languages, context-free grammars and pushdown
automata, Turing machines
Seminar on Theoretical Computer Science,
Helsinki University of Technology,
Propositional Satisfiability Checking Techniques
Basic Course in Programming L1,
Helsinki University of Technology, autumn 2001