Matti Jarvisalo
Matti Järvisalo |
|
|
|
[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 |
|
![[AT]](at_small.gif)
helsinki.fiI 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.
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, ...
- 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.
- Exceptional full paper at AAAI 2008.
- Runner-up for the CP'07 Best Paper Award at CP 2007.
- Best Student Paper award at ICLP 2007.
- 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).
- 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]
- BBMarkov: a branch-and-bound approach to learning optimal decomposable graphs [NIPS'17]
- MaxPre: an extended MaxSAT preprocessor [SAT'17]
- Dseptor: a core-guided approach to learning optimal causal graphs [IJCAI'17]
- aba2af: a system for reasoning about acceptance in structured argumentation via abstract argumentation [ECSQARU'17]
- AFSynth: synthesizing argumentation frameworks from examples via constraint optimization [ECAI'16]
- AbHS: a propositional abduction solver based on the implicit hitting set paradigm [KR'16]
- LMHS: a hybrid SAT-IP MaxSAT solver based on the implicit hitting set paradigm [SAT'16]
- Pakota: a system for enforcement in abstract argumentation based on constraint optimization [AAAI'16 , IJCAI'16, JELIA'16]
- SATDiscoverer: a general SAT-based procedure for learning causal models [UAI'13]
- CEGARTIX: 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]
Professional Activities
Invited Talks and Tutorials
- 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
- SAT: International Conferences on Theory and Applications of Satisfiability Testing, 2013-2017.
- Program Committee Chair, PoS 2018: 9th International Workshop on Pragmatics of SAT, Oxford, UK.
- 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
- 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
- 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
- IJCAI 2016: 25th International Joint Conference on Artificial Intelligence Senior PC
- 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
- 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
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
- 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)
- SAT Association
- Association for Automated Reasoning
- Association for Constraint Programming
- Association for Logic Programming
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.
TeachingLectured (teacher-in-charge of) the following courses at the University of Helsinki:
- Combinatorial Optimization (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