Matti Jarvisalo

Dr. Matti Järvisalo

Postdoctoral Researcher (Academy of Finland) Department of Computer Science Faculty of Science University of Helsinki Education D.Sc.(Tech.) with distinction, 2008, Helsinki University of Technology TKK Lic.Sc. (Tech.), 2007, TKK M.Sc. (Tech.) with distinction, 2004, TKK Note: TKK is part of Aalto University since 2010.

Postal Address: Department of Computer Science P.O. Box 68 FI-00014 University of Helsinki Finland Office: Room A329, 3rd floor of Exactum, Gustaf Hällströmin katu 2b Telephone: +358 9 191 51377 Email: matti.jarvisalocs.helsinki.fi

News

• I am a member of the COIN Finnish Centre of Excellence in Computational Inference Research that started in the beginning of 2012.
• I'm on the PC of AAAI 2012, ECML-PKDD 2012, and NMR 2012.
• We are organizing SWAT 2012 in Helsinki.
• I'm organizing the SAT Challenge 2012 together with Adrian Balint, Anton Belov, and Carsten Sinz.

• I was awarded the Best Researcher Award in 2011 by the Department of Computer Science at University of Helsinki.
• From the beginning of 2010, I'm primary investigator of the three-year research project "BooleanCORE: Extending the Reach of Boolean Constraint Reasoning" funded by Academy of Finland.

• 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 at TKK. 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ä.

Research

Keywords: Automated reasoning, artificial intelligence, constraint satisfaction, satisfiability, computational logic, formal methods, knowledge representation, computational complexity, proof complexity, discrete optimization, ...

My primary focus is efficient and robust techniques for solving computationally hard (NP-complete and beyond) constraint satisfaction and optimization problems. My research covers both practical and theoretical aspects of decision and optimization procedures, and contemporary applications of such procedures in problem domains with practical relevance. I'm especially interested in the interplay between practical (in)tractability and structural aspects of constraint satisfaction problems.

To date my main research focus has been on analyzing and developing search-based reasoning techniques for Boolean satisfiability (SAT) and related approaches, including constraint programming (CP) and answer set programming (ASP), extensions such as satisfiability modulo theories (SMT), and their optimization variants.

Projects

• BooleanCORE: Extending the Reach of Boolean Constraint Reasoning (2010-2012), funded by Academy of Finland, primary investigator

• Lightweight Formal Methods for Distributed Component-based Embedded Systems (2009), funded by Tekes
• Methods for Constructing and Solving Large Constraint Models (2008-2009), Academy of Finland
• Advanced Constraint Programming Techniques for Large Structured Problems (2005-2007), Academy of Finland
• Applications of Rule-Based Constraint Programming (2002-2005), Academy of Finland

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 DBLP entry (includes only a subset of my papers, though).

Recent work

• Simulating Circuit-Level Simplifications on CNF, J. Automated Reasoning (to appear) [pdf]
• The International SAT Solver Competitions, AI Magazine (to appear)
• Structure-Based Local Search Heuristics for Circuit-Level Boolean Satisfiability, LSCS 2011 [pdf]
• On the Relative Efficiency of DPLL and OBDDs with Axiom and Join, CP 2011 [pdf]
• Depth-Driven Circuit-Level Stochastic Local Search for SAT, IJCAI 2011 [pdf]
• Efficient CNF Simplification based on Binary Implication Graphs, SAT 2011 [pdf]
• Itemset Mining as a Challenge Application for Answer Set Enumeration, LPNMR 2011 [pdf]
• Covered Clause Elimination, LPAR-17 short paper, 2010 [pdf]
• Clause Elimination Procedures for CNF Formulas, LPAR-17, 2010 [pdf]
• Testing and Debugging Techniques for Answer Set Solver Development, TPLP 10(4-6), 2010 [pdf]
• Reconstructing Solutions after Blocked Clause Elimination, SAT 2010 [pdf]
• Blocked Clause Elimination, TACAS 2010 [pdf]
• Limitations of Restricted Branching in Clause Learning, Constraints 14(3), 2009 [pdf]

Professional Activities

Organization

• Organizer, SAT Challenge 2012
• Local organizer, SWAT 2012: 13th Scandinavian Symposium and Workshops on Algorithm Theory, July 2012, Helsinki, Finland
• Organizer, International 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

Program Committees

• 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
• NMR 2012: 14th International Workshop on Non-Monotonic Reasoning
• IJCAI 2011: 22nd International Joint Conference on Artificial Intelligence
• PoS 2011: 2nd Workshop on Pragmatics of SAT
• LoCoCo 2010: 1st Workshop on Logics for Component Configuration

Reviewing

Reviewer for ACM Journal of Experimental Algorithmics.

Reviewed scientific manuscripts for

Journals:

• Artificial Intelligence - 2011, 2010
• Journal on Satisfiability, Boolean Modeling and Computation - 2011
• AI Communications - 2010
• Journal of Logic and Computation - 2008

Conferences (not including PC memberships):

• ICDE: IEEE International Conference on Data Engineering - 2012
• LPAR: International Conference on Logic for Programming, Artificial Intelligence and Reasoning - 2012
• 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
• SAT: International Conference on Theory and Applications of Satisfiability Testing - 2011, 2010, 2005
• FMCAD: International Conference on Formal Methods in Computer-Aided Design - 2010
• 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

• 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 "Extending the Reach of Boolean Constraint Reasoning", Academy of Finland (2010-2012).

• 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

Events and other activities

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:

• Discrete Optimization Project, 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, University of Helsinki, autumn 2011
  Combinatorial search spaces and optimization problems. Exhaustive and heuristic methods. Linear and integer programming.
• Seminar on Boolean Constraint Reasoning, 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

Forthcoming Events

TACAS'12 (Tallinn), KR'12 (Rome), ICAPS'12 (Sao Paulo), CPAIOR'12 (Nantes), IJCAR'12 (Manchester), AAAI'12 (Toronto), SAT'12 (Trento), NMR'12 (Rome), CAV'12 (Berkeley), ECAI'12 (Montpellier), CP'12 (Quebec), ICLP'12 (Budapest), JELIA'12 (Toulouse)

IJCAI'13 (Beijing), CADE'13 (Lake Placid), LPNMR'13 (Corunna)

FLoC'14 (Vienna), ECAI'14 (Prague)