Research

Some of the major research themes of the Constraint Reasoning and Optimization group are highlighted here.

Recent major research projects include:

Next-Generation Unsatisfiability-based Declarative Optimization (9/2023-8/2027, Academy of Finland)
Declarative Boolean Optimization: Pushing the Envelope (9/2019-8/2023, Academy of Finland)
Symbolic Techniques for Formally Verified and Explainable AI (2020-2022, Academy of Finland)
Decision Procedures for the Polynomial Hierarchy, Boolean Optimization, and Model Counting (9/2014-8/2019, Academy of Finland)
Harnessing Constraint Reasoning for Structure Discovery (2015-2017, Research Funds of the University of Helsinki)
COIN Centre of Excellence in Computational Inference Research (2012-2017 Academy of Finland)
Extending the Reach of Boolean Constraint Reasoning (1/2010-4/2013, Academy of Finland)

SAT Solving and Beyond NP

Representative publications:

Premise Set Caching for Enumerating Minimal Correction Subsets. Alessandro Previti, Carlos Mencia, Matti Järvisalo, and Joao Marques-Silva. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018). AAAI Press, 2018.
[pdf] [abstract/bibtex]

Implicit Hitting Set Algorithms for Reasoning Beyond NP. Paul Saikko, Johannes P. Wallner, and Matti Järvisalo. In Chitta Baral, James P. Delgrande and Frank Wolter, editors, Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR 2016), pages 104-113. AAAI Press, 2016.
[Publisher's version] Extended version with proofs: [pdf] [abstract/bibtex]

Overview and Analysis of the SAT Challenge 2012 Solver Competition. Adrian Balint, Anton Belov, Matti Järvisalo, and Carsten Sinz. Artificial Intelligence 223:120-155, 2015.
[doi:10.1016/j.artint.2015.01.002] Preliminary version: [pdf] [abstract/bibtex]

Inprocessing Rules. Matti Järvisalo, Marijn Heule, and Armin Biere. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012), volume 7364 of Lecture Notes in Computer Science (LNCS/LNAI), pages 355-370. Springer, 2012.
[doi:10.1007/978-3-642-31365-3_28] Preliminary version: [pdf] [abstract/bibtex]

Preprocessing

Representative publications:

MaxPre: An Extended MaxSAT Preprocessor. Tuukka Korhonen, Jeremias Berg, Paul Saikko, and Matti Järvisalo. In Serge Gaspers and Toby Walsh, editors, Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017), volume 10491 of Lecture Notes in Computer Science, pages 449-456. Springer, 2017.
[doi:10.1007/978-3-319-66263-3_28] [pdf] [abstract/bibtex]

Clause Elimination for SAT and QSAT. Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, and Armin Biere. Journal of Artificial Intelligence Research 53:127-168, 2015.
[doi:10.1613/jair.4694] [pdf] [abstract/bibtex]
[IJCAI-JAIR Best Paper Prize 2019]

Conditional Lower Bounds for Failed Literals and Related Techniques. Matti Järvisalo and Janne H. Korhonen. In Uwe Egly and Carsten Sinz, editors, Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014), volume 8561 of Lecture Notes in Computer Science, pages 75-84. Springer, 2014.
[doi:10.1007/978-3-319-09284-3_7] [pdf] [abstract/bibtex]

Formula Preprocessing in MUS Extraction. Anton Belov, Matti Järvisalo, and Joao Marques-Silva. In Nir Piterman and Scott Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), volume 7795 of Lecture Notes in Computer Science, pages 110-125. Springer, 2013.
[doi:10.1007/978-3-642-36742-7_8] Preliminary version: [pdf] [abstract/bibtex];

Simulating Circuit-Level Simplifications on CNF. Matti Järvisalo, Armin Biere, and Marijn Heule. Journal of Automated Reasoning 49(4):583-619, 2012.
[doi:10.1007/s10817-011-9239-9] Preliminary version: [pdf] [abstract/bibtex]

Maximum Satisfiability and Discrete Optimization

Representative publications:

Reduced Cost Fixing for Maximum Satisfiability. Fahiem Bacchus, Antti Hyttinen, Matti Järvisalo, and Paul Saikko. In Jerome Lang, editor, Proceedings of the 27th International Joint Conference on Artificial Intelligence and the 23rd European Conference on Artificial Intelligence (IJCAI-ECAI 2018), pages 5209-5213. ijcai.org, 2018.
[IJCAI 2018 Best Sister Conference Paper Track]
[doi:10.24963/ijcai.2018/723] [pdf] [abstract/bibtex]

Learning Chordal Markov Networks via Branch and Bound. Kari Rantanen, Antti Hyttinen, and Matti Järvisalo. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Proceedings of the 30th Annual Conference on Neural Information Processing Systems (NIPS 2017), pages 1845-1855, 2017.
[pdf] [abstract/bibtex]

LMHS: A SAT-IP Hybrid MaxSAT Solver. Paul Saikko, Jeremias Berg, and Matti Järvisalo. In Nadia Creignou and Daniel Le Berre, editors, Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016), volume 9710 of Lecture Notes in Computer Science, pages 539-546. Springer, 2016.
[doi:10.1007/978-3-319-40970-2_34] [pdf] [abstract/bibtex]

Structure Learning

Representative publications:

Empirical Hardness of Finding Optimal Bayesian Network Structures: Algorithm Selection and Runtime Prediction. Brandon Malone, Kustaa Kangas, Matti Järvisalo, Mikko Koivisto, and Petri Myllymäki. Machine Learning 107(1):247-283, 2018.
[doi:10.1007/s10994-017-5680-2] [pdf] [abstract/bibtex]

Bayesian Network Structure Learning with Integer Programming: Polytopes, Facets and Complexity. James Cussens, Matti Järvisalo, Janne H. Korhonen, and Mark Bartlett. Journal of Artificial Intelligence Research 58:185-229, 2017.
[doi:10.1613/jair.5203] [pdf] [abstract/bibtex]

A Core-Guided Approach to Learning Optimal Causal Graphs. Antti Hyttinen, Paul Saikko, and Matti Järvisalo. In Carles Sierra, editor, Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017), pages 645-651. AAAI Press, 2017.
[doi:10.24963/ijcai.2017/90] [pdf] [abstract/bibtex]

Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability. Jeremias Berg, Matti Järvisalo, and Brandon Malone. In Jukka Corander and Samuel Kaski, editors, Proceedings of the 17th International Conference on Artificial Intelligence and Statistics (AISTATS 2014), volume 33 of JMLR Workshop and Conference Proceedings, pages 86-95. JMLR, 2014.
[Publisher's version] [pdf] [abstract/bibtex]

Formal Argumentation

Representative publications:

Novel Algorithms for Abstract Dialectical Frameworks based on Complexity Analysis of Subclasses and SAT Solving. Thomas Linsbichler, Marco Maratea, Andreas Niskanen, Johannes P. Wallner, and Stefan Woltran. In Jerome Lang, editor, Proceedings of the 27th International Joint Conference on Artificial Intelligence and the 23rd European Conference on Artificial Intelligence (IJCAI-ECAI 2018), pages 1905-1911. ijcai.org, 2018.

Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation. Johannes P. Wallner, Andreas Niskanen, and Matti Järvisalo. Journal of Artificial Intelligence Research 60:1-40, 2017.
[doi:10.1613/jair.5415] [pdf] [abstract/bibtex]

Synthesizing Argumentation Frameworks from Examples. Andreas Niskanen, Johannes P. Wallner, and Matti Järvisalo. In Gal A. Kaminka, Maria Fox, Paolo Bouquet, Eyke Hüllermeier, Virginia Dignum, Frank Dignum, and Frank van Harmelen, editors, Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI 2016), volume 285 of Frontiers in Artificial Intelligence and Applications, pages 551-559. IOS Press, 2016.
[Runner-up for ECAI 2016 Best Student Paper Award]
[doi:10.3233/978-1-61499-672-9-551] [pdf] [abstract/bibtex]

Complexity-Sensitive Decision Procedures for Abstract Argumentation. Wolfgang Dvořák, Matti Järvisalo, Johannes Peter Wallner, and Stefan Woltran. Artificial Intelligence 206:53-78, 2014.
[doi:10.1016/j.artint.2013.10.001] [abstract/bibtex]