2. CoSCo
  3. Research
  4. Research groups
  5. Complex Systems Computation
  6. Focus areas
  7. Constraint Reasoning and Optimization

Constraint Reasoning and Optimization

Research

Overview

The  Constraint Reasoning and Optimization group focuses on the development and analysis of state-of-the-art decision, search, and optimization procedures, and their applications in computationally hard problem domains with real-world relevance. Especially, the group contributes to the development state-of-the-art Boolean satisfiability (SAT) solvers, their extensions to Boolean optimization, and applications of SAT-based and other types of discrete search and optimization procedures in exactly solving intrinsically hard (NP-complete and beyond) computational tasks. Recent domain-specific studies include exactly solving machine learning problems (different types of clustering, classification, and structure learning tasks) via constrained optimization, and computational aspects of argumentation theory.

We are affiliated with Department of Computer Science at University of Helsinki.

Our research is financially supported by Academy of Finland, Research Funds of the University of Helsinki, and the Doctoral Programme in Computer Science DoCS.

PI: Associate Professor Matti Järvisalo

Team:

  • Dr Bernhard Bliem, postdoc
  • Dr Antti Hyttinen, Academy of Finland postdoc
  • Dr Alessandro Previti, postdoc
  • MSc Jeremias Berg, PhD student
  • MSc Andreas Niskanen, PhD student
  • MSc Kari Rantanen, PhD student
  • MSc Paul Saikko, PhD student
  • Tuukka Korhonen, BSc student
  • Tuomo Lehtonen, BSc student

Former members:

  • Dr Juho-Kustaa Kangas 2013-2017 (affiliated PhD student, moved on to Aalto University) 
  • Dr Brandon Malone 2012-2014 (postdoc, moved on to MPI Cologne, Germany)
  • Dr Johannes P. Wallner 2016-2017 (postdoc, moved on to Vienna University of Technology, Austria)

Visitors:

  • Prof Mario Alviano (University of Calabria, Italy), 8/2017
  • MSc Neha Lodha (Vienna University of Technology, Austria), 3-5/2017
  • Prof Fahiem Bacchus (University of Toronto, Canada), 9-10/2016
  • Dr James Cussens (University of York, UK), 4/2015
  • Dr Brandon Malone (MPI, Germany), 4/2015

Research-Related Software and Benchmarks

  • 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]
  • 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 [IJCAI'15, AIJ'14, 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.

Projects

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

Teaching

Publications 2018-

  • 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, accepted for publication (2017).
    [doi:???] [pdf] [abstract/bibtex]
  • Towards Transformational Creation of Novel Songs. Jukka M. Toivanen, Matti Järvisalo, Olli Alm, Dan Ventura, Martti Vainio, and Hannu Toivonen. Connection Science, accepted for publication (2018).
    [doi:???] [pdf] [abstract/bibtex]
  • Abstract Dialectical Frameworks. An Overview. Gerhard Brewka, Stefan Ellmauthaler, Hannes Strass, Johannes P. Wallner, and Stefan Woltran. In Pietro Baroni, Dov Gabbay, Massimiliano Giacomin, and Leon van der Torre, editors, Chapter 5 of Handbook of Formal Argumentation, pages ???-???. College Publications, 2018 (to appear).
  • Foundations of Implementations for Formal Argumentation. Federico Cerutti, Sarah A. Gaggl, Matthias Thimm, and Johannes P. Wallner. In Pietro Baroni, Dov Gabbay, Massimiliano Giacomin, and Leon van der Torre, editors, Chapter 14 of Handbook of Formal Argumentation, pages ???-???. College Publications, 2018 (to appear).

Publications 2017

  • Abstract Dialectical Frameworks. An Overview. Gerhard Brewka, Stefan Ellmauthaler, Hannes Strass, Johannes P. Wallner, and Stefan Woltran. Journal of Logics and their Applications, 4(8):2263–2317, 2017.
  • Foundations of Implementations for Formal Argumentation. Federico Cerutti, Sarah A. Gaggl, Matthias Thimm, and Johannes P. Wallner. Journal of Logics and their Applications, 4(8):2623–2705, 2017.
  • Learning Score-Optimal Chordal Markov Networks via Branch and Bound. Kari Rantanen. Master's thesis, University of Helsinki, 2017.
  • Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. Tomáš Balyo, Marijn J.H. Heule, and Matti Järvisalo (editors). Volume B-2017-1 of Department of Computer Science Series of Publications B, University of Helsinki, 2017.
    [handle:10138/224324] [bibtex]
  • MaxSAT Evaluation 2017: Solver and Benchmark Descriptions. Carlos Ansotegui, Fahiem Bacchus, Matti Järvisalo, and Ruben Martins (editors). Volume B-2017-2 of Department of Computer Science Series of Publications B, University of Helsinki, 2017.
    [handle:???] [bibtex]
     

Publications 2016

  • Impact of SAT-Based Preprocessing on Core-Guided MaxSAT Solving. Jeremias Berg and Matti Järvisalo. In Michel Rueher, editor, Proceedings of the 22nd International Conference on Principles and Practice of Constraint Programming (CP 2016), volume 9892 of Lecture Notes in Computer Science, pages 66-85. Springer, 2016.
    [doi:10.1007/978-3-319-44953-1_5] [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]
  • Optimal Status Enforcement in Abstract Argumentation. Andreas Niskanen, Johannes P. Wallner, and Matti Järvisalo. In Subbarao Kambhampati, editor, Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), pages 1216-1222. AAAI Press, 2016.
    [Publisher's version] [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]
  • Pakota: A System for Enforcement in Abstract Argumentation. Andreas Niskanen, Johannes P. Wallner, and Matti Järvisalo. In  Loizos Michael and Antonis C. Kakas, editors, Proceedings of the 15th European Conference on Logics in Artificial Intelligence (JELIA 2016), volume 10021 of Lecture Notes in Computer Science, pages 385-400. Springer, 2016.
  • A Logical Approach to Context-Specific Independence. Jukka Corander, Antti Hyttinen, Juha Kontinen, Johan Pensar, and Jouko Väänänen. In Åsa Hirvonen and Ruy J. G. B. de Queiroz, editors, Proceedings of the 23rd International Workshop on Logic, Language, Information, and Computation (WOLLIC 2016), volume 9803 of Lecture Notes in Computer Science, pages 165-182. Springer, 2016.
  • Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions. Tomáš Balyo, Marijn J.H. Heule, and Matti Järvisalo (editors). Volume B-2016-1 of Department of Computer Science Series of Publications B, University of Helsinki, 2016. ISBN 978-951-51-2345-9.
    [handle:10138/164630] [bibtex]
  • Enforcement in Abstract Argumentation via Boolean Optimization. Andreas Niskanen. Master's thesis, University of Helsinki, 2016.

Publications 2015

  • Improved Answer-Set Programming Encodings for Abstract Argumentation. Sarah Alice Gaggl, Norbert Manthey, Alessandro Ronca, Johannes Peter Wallner, and Stefan Woltran. Theory and Practice of Logic Programming 15(4-5):434-448, 2015.
  • Re-implementing and Extending a Hybrid SAT-IP Approach to Maximum Satisfiability. Paul Saikko. Master's thesis, University of Helsinki, 2015.
    [handle:10138/159186]

Publications 2014

  • Finding Optimal Bayesian Network Structures with Constraints Learned from Data. Xiannian Fan, Brandon Malone, and Changhe Yuan. In Jin Tian and Nevin L. Zhang, editors, Proceedings of the 30th Conference on Uncertainty in Artificial Intelligence (UAI 2014), pages 200-209. AUAI Press, 2014.
  • Tightening Bounds for Bayesian Network Structure Learning. Xiannian Fan, Changhe Yuan, and Brandon Malone. In Carla E. Brodley and Peter Stone, editors, Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI 2014), pages 2439-2445. AAAI Press, 2014.
  • A Depth-First Branch and Bound Algorithm for Learning Optimal Bayesian Networks. Brandon M. Malone, and Changhe Yuan. In Madalina Croitoru, Sebastian Rudolph, Stefan Woltran, and Christophe Gonzales, editors, Revised Selected Papers of the Third International Workshop on Graph Structures for Knowledge Representation and Reasoning (GKR 2013), volume 8323 of Lecture Notes in Computer Science, pages 111-122. Springer, 2014.
  • Portfolio-based Selection of Robust Dynamic Loop Scheduling Algorithms using Machine Learning. Nitin Sukhija, Brandon Malone, Srishti Srivastava, Ioana Banicescu, and Florina Ciorba. In IEEE International Symposium on Parallel & Distributed Processing Workshops, pages 1638-1647. IEEE, 2014.
  • Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions. Anton Belov, Daniel Diepold, Marijn J.H. Heule, and Matti Järvisalo (editors), volume B-2014-2 of Department of Computer Science Series of Publications B, University of Helsinki, 2014. ISBN 978-951-51-0043-6.
    [handle:10138/135571]
  • Generating the Uniform Random Benchmarks. Anton Belov, Daniel Diepold, Marijn J.H. Heule, and Matti Järvisalo. In Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions, volume B-2014-2 of Department of Computer Science Series of Publications B, page 80. University of Helsinki, 2014.
    [handle:10138/135571]
  • The Application and the Hard Combinatorial Benchmarks in SAT Competition 2014. Anton Belov, Daniel Diepold, Marijn J.H. Heule, and Matti Järvisalo. In Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions, volume B-2014-2 of Department of Computer Science Series of Publications B, pages 81-82. University of Helsinki, 2014.
    [handle:10138/135571]
  • Cost-Optimal Correlation Clustering via Partial Maximum Satisfiability. Jeremias Berg. Master's thesis, University of Helsinki, 2014.
    [handle:10138/45392]

Publications 2013

  • Theory and Applications of Satisfiability Testing - SAT 2013. Matti Järvisalo and Allen Van Gelder (editors). volume 7962 of Lecture Notes in Computer Science, Springer 2013. ISBN 978-3-642-39070-8. [Book at Springer.com]
  • Learning optimal Bayesian networks: A shortest path perspective. Changhe Yuan and Brandon Malone. Journal of Artificial Intelligence Research, 48:23–65, 2013.
  • Optimal Correlation Clustering via MaxSAT. Jeremias Berg and Matti Järvisalo. In Wei Ding, Takashi Washio, Hui Xiong, George Karypis, Bhavani M. Thuraisingham, Diane J. Cook and Xindong Wu, editors, Proceedings of the 2013 IEEE 13th International Conference on Data Mining Workshops (ICDMW 2013), pages 750--757, IEEE Computer Society , 2013.
  • Predicting the Flexibility of Dynamic Loop Scheduling Using an Artificial Neural Network. Srishti Srivastava, Brandon Malone, Nitin Sukhija, Ioana Banicescu, and Florina Ciorba. Proceedings of the 12th International Symposium on Parallel and Distributed Computing (ISPDC 2013), IEEE Computer Society 2013.
  • Polycomb Group Gene OsFIE2 Regulates Rice (Oryza sativa) Seed Development and Grain Filling via a Mechanism Distinct from Arabidopsis. Babi Ramesh Reddy Nallamilli, Jian Zhang, Hana Mujahid, Brandon M. Malone, Susan M. Bridges, and Zhaohua Peng. PLoS Genetics, 9(3): e1003322, 2013.
  • Evaluating Anytime Algorithms for Learning Optimal Bayesian Networks. Brandon Malone and Changhe Yuan. In Ann Nicholson and Padhraic Smyth, editors, Proceedings of the 29th Conference on Uncertainty in Artificial Intelligence (UAI 2013), pages 301-310. AUAI Press, 2013.
  • Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions. Adrian Balint, Anton Belov, Marijn J.H. Heule, and Matti Järvisalo (editors), Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, volume B-2013-1 of Department of Computer Science Series of Publications B, University of Helsinki, 2013. ISBN 978-952-10-8991-6. [handle:10138/40026]
  • Equivalence Checking of HWMCC 2012 Circuits. Armin Biere, Marijn J.H. Heule, Matti Järvisalo, and Norbert Manthey. In A. Balint, A. Belov, M.J.H. Heule, and M. Järvisalo (editors), Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, volume B-2013-1 of Department of Computer Science Series of Publications B, page 104. University of Helsinki, 2013. [handle:10138/40026]
  • Generating the Uniform Random Benchmarks for SAT Competition 2013. Adrian Balint, Anton Belov, Marijn J.H. Heule, and Matti Järvisalo. In A. Balint, A. Belov, M.J.H. Heule, and M. Järvisalo (editors), Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, volume B-2013-1 of Department of Computer Science Series of Publications B, pages 97-98. University of Helsinki, 2013.
  • The Application and the Hard Combinatorial Benchmarks in SAT Competition 2013. Adrian Balint, Anton Belov, Marijn J.H. Heule, and Matti Järvisalo. In A. Balint, A. Belov, M.J.H. Heule, and M. Järvisalo (editors), volume B-2013-1 of Department of Computer Science Series of Publications B, pages 99-101. University of Helsinki, 2013. [handle:10138/40026]

Publications 2012

  • A Bounded Error, Anytime Parallel Algorithm for Exact Bayesian Network Structure Learning. B. Malone and C. Yuan. In Proceedings of the 6th European Workshop on Probabilistic Graphical Models (PGM 2012), 2012.
  • An Improved Admissible Heuristic for Finding Optimal Bayesian Networks. C. Yuan and B. Malone, . In Proceedings of the 28th Conference on Uncertainty in Artificial Intelligence (UAI 2012), 2012.
  • Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz (editors), volume B-2012-2 of Department of Computer Science Series of Publications B, University of Helsinki, 2012. ISBN 978-952-10-8106-4.
    [handle:10138/34218] [bibtex]
  • CEGARTIX: A SAT-Based Argumentation System. Wolfgang Dvořák, Matti Järvisalo, Johannes Peter Wallner, and Stefan Woltran. In 3rd Workshop on Pragmatics of SAT (PoS 2012), 2012.
  • Finding Circuits for Ensemble Computation via Boolean Satisfiability. Matti Järvisalo, Petteri Kaski, Mikko Koivisto, and Janne H. Korhonen. In Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz, editors, Proceedings of SAT Challenge 2012, volume B-2012-2 of Department of Computer Science Series of Publications B, pages 79-81. University of Helsinki, 2012.
    [handle:10138/34218]
  • Application and Hard Combinatorial Benchmarks in SAT Challenge 2012. Adrian Balint, Anton Belov, Matti Järvisalo, and Carsten Sinz. In Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz, editors, Proceedings of SAT Challenge 2012, volume B-2012-2 of Department of Computer Science Series of Publications B, pages 69-71. University of Helsinki, 2012.
    [handle:10138/34218]
  • SAT Challenge 2012 Random SAT Track: Description of Benchmark Generation. Adrian Balint, Anton Belov, Matti Järvisalo, and Carsten Sinz. In Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz, editors, Proceedings of SAT Challenge 2012, volume B-2012-2 of Department of Computer Science Series of Publications B, pages 72-73. University of Helsinki, 2012.
    [handle:10138/34218]

Last updated on 20 Jan 2018 by Matti Järvisalo - Page created on 6 Sep 2012 by Petri Myllymäki