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)
(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 (AAAI 2018). AAAI Press, 2018.

[] []

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 (KR 2016), pages 104-113. AAAI Press, 2016.

[] Extended version with proofs: [] []

Overview and Analysis of the SAT Challenge 2012 Solver Competition. Adrian Balint, Anton Belov, Matti Järvisalo, and Carsten Sinz. 223:120-155, 2015.

[] Preliminary version: [] []

Inprocessing Rules. Matti Järvisalo, Marijn Heule, and Armin Biere. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Proceedings of the (IJCAR 2012), volume 7364 of , pages 355-370. Springer, 2012.

[] Preliminary version: [] []

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 (SAT 2017), volume 10491 of , pages 449-456. Springer, 2017.

[] [] []

Clause Elimination for SAT and QSAT. Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, and Armin Biere. 53:127-168, 2015.

[] [] []

[]

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 (SAT 2014), volume 8561 of , pages 75-84. Springer, 2014.

[] [] []

Formula Preprocessing in MUS Extraction. Anton Belov, Matti Järvisalo, and Joao Marques-Silva. In Nir Piterman and Scott Smolka, editors, Proceedings of the (TACAS 2013), volume 7795 of , pages 110-125. Springer, 2013.

[] Preliminary version: [] [];

Simulating Circuit-Level Simplifications on CNF. Matti Järvisalo, Armin Biere, and Marijn Heule. 49(4):583-619, 2012.

[] Preliminary version: [] []

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 (IJCAI-ECAI 2018), pages 5209-5213. ijcai.org, 2018.

[IJCAI 2018 Best Sister Conference Paper Track]

[] [] []

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 (NIPS 2017), pages 1845-1855, 2017.

[] []

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.

[] [] []

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. 107(1):247-283, 2018.

[] [] []

Bayesian Network Structure Learning with Integer Programming: Polytopes, Facets and Complexity. James Cussens, Matti Järvisalo, Janne H. Korhonen, and Mark Bartlett. 58:185-229, 2017.

[] [] []

A Core-Guided Approach to Learning Optimal Causal Graphs. Antti Hyttinen, Paul Saikko, and Matti Järvisalo. In Carles Sierra, editor, Proceedings of the (IJCAI 2017), pages 645-651. AAAI Press, 2017.

[] [] []

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 (AISTATS 2014), volume 33 of JMLR Workshop and Conference Proceedings, pages 86-95. JMLR, 2014.

[] [] []

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 (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. 60:1-40, 2017.

[] [] []

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 (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]

[] [] []

Complexity-Sensitive Decision Procedures for Abstract Argumentation. Wolfgang Dvořák, Matti Järvisalo, Johannes Peter Wallner, and Stefan Woltran. 206:53-78, 2014.

[] []