Matti Jarvisalo Dr. Matti Järvisalo

Academy Research Fellow Academy of Finland, 9/2014-8/2019 Principal Investigator Constraint Reasoning and Optimization Adjunct Professor (docent) ("kaiken maailman dosentti") 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.jarvisalocs.helsinki.fi

I lead the Constraint Reasoning and Optimization Group at the University of Helsinki and (within CoSCo) at HIIT.

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 background, especially in 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.

Interested in a PhD or Postdoc position in my group?
For queries on potential opportunities, contact me by email for more details!

News

I am on the PCs of AAAI 2017, CPAIOR 2017, and IEA/AIE 2017 (argumentation special track). Invited talk at 1st International Workshop on Argumentation in Logic Programming and Non-Monotonic Reasoning (Arg-LPNMR 2016) @ IJCAI-16 Invited talk at IJCAI-16: Early Career Spotlight I will lead Seminar on Computational Social Choice (3 ECTS) in Autumn 2016. I'm one of the lecturers at the 1st International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning in Lisbon, Portugal. I gave a AAAI 2016 tutorial Algorithms for Maximum Satisfiability with Applications to AI together with Fahiem Bacchus. I'm on the Senior PC of IJCAI 2016 and on the PCs of SAT 2016, AAAI 2016, BeyondNP@AAAI-16, POS 2016, and CP 2016 DP. I'm Guest Editor (with Marijn Heule) of a special issue of Journal of Satisfiability, Boolean Modeling and Computation on the SAT 2014 affiliated competitions and evaluations. More information here. Update: the special issue has been published! I lectured the course Satisfiability, Boolean Modeling and Computation (5 ECTS) in Spring 2016, study period III. My project Harnessing Constraint Reasoning for Structure Discovery was granted funding for the years 2015-2017 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. During 2013-2017 I'm a member of the steering committee of SAT, the International Conferences on Theory and Applications of Satisfiability Testing. I am a member of the COIN Finnish Centre of Excellence in Computational Inference Research that started in the beginning of 2012. Earlier Highlights 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

Keywords: Boolean satisfiability and its generalizations, decision procedures, constraint satisfaction and optimization, automated reasoning, artificial intelligence, knowledge representation, computational/proof complexity, computational aspects of argumentation, graphical models, structure discovery, ...

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-2017; 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)

Research-Related Software

• 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 extension enforcement in abstract argumentation based on constraint optimization [AAAI'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].

Publications

A complete list of my publications with downloadable papers and bibtex entries is available both by year and by type. You can also check out my Google Scholar profile, and my DBLP entry (includes only a subset of my papers, though).

Some recent work

• Bayesian Network Structure Learning with Integer Programming: Polytopes, Facets, and Complexity, submitted [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]
• Cost-Optimal Constrained Correlation Clustering via Weighted Partial Maximum Satisfiability, Artificial Intelligence (2016) [pdf]
• 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 [pdf]
• Clause Elimination for SAT and QSAT, Journal of Artificial Intelligence Research (2015) [pdf]
• Do-calculus when the True Graph is Unknown, UAI 2015 [pdf]
• Learning Optimal Chain Graphs with Answer Set Programming, UAI 2015 [pdf]
• Impact of Learning Strategies on the Quality of Bayesian Networks: An Empirical Evaluation, UAI 2015 [pdf]
• Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT, IJCAI 2015 [pdf]
• Overview and Analysis of the SAT Challenge 2012 Solver Competition, Artificial Intelligence (2015) [pdf]
• MaxSAT-Based Cutting Planes for Learning Graphical Models, CPAIOR 2015 [pdf]
• Weak Models of Distributed Computing, with Connections to Modal Logic, Distributed Computing (2015) [pdf]

Professional Activities

Steering Committee Memberships

• SAT: International Conferences on Theory and Applications of Satisfiability Testing

Program Committee Chairing and Editorships

• 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

• AAAI 2017: 31st AAAI Conference on Artificial Intelligence
• CPAIOR 2017: 14th International Conference on Integration of AI and OR Techniques in Constraint Programming
• 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

Organization

• 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:

• IEEE Intelligent Systems - 2016
• Theory and Practice of Logic Programming - 2016
• Artificial Intelligence - 2015, 2014, 2013, 2012, 2011, 2010
• Information Sciences - 2015
• Journal of Artificial Intelligence Research - 2015
• Journal of Automated Reasoning - 2015
• Annals of Mathematics and Artificial Intelligence - 2014
• 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

Awards and Honors

• Honorary Mention at ICCMA 2015, 1st International Competition on Computational Models of Argumentation, for the Cegartix solver
• 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

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

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

Teaching

Lectured (teacher-in-charge of) the following courses:

• Seminar on Computational Social Choice (3 ECTS), University of Helsinki, autumn 2016.
• Satisfiability, Boolean Modeling and Computation (5 ECTS), University of Helsinki, spring 2016.
• Seminar on Tractability (3 ECTS), University of Helsinki, autumn 2015.
• 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. Topics include: 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: 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, 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