Constraint Reasoning and Optimization

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 (as an independent research group), as well as with HIIT Helsinki Institute for Information Technology (as one of the focus areas of Complex Systems Computation).

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: Dr Matti Järvisalo, Academy Research Fellow, Adjunct Professor

Team:

Former members:

Research-Related Software and Benchmarks

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

  • Cost-Optimal Constrained Correlation Clustering via Weighted Partial Maximum Satisfiability. Jeremias Berg and Matti Järvisalo. Artificial Intelligence, to appear (2015).
  • Separating OR, SUM, and XOR circuits. Magnus Find, Mika Göös, Matti Järvisalo, Petteri Kaski, Mikko Koivisto, and Janne H. Korhonen. Journal of Computer and System Sciences 82(5):793-801, 2016.
  • Synchronous Counting and Computational Algorithm Design. Danny Dolev, Keijo Heljanko, Matti Järvisalo, Janne H. Korhonen, Christoph Lenzen, Joel Rybicki, Jukka Suomela, and Siert Wieringa. Journal of Computer and System Sciences 82(2):310-332, 2016.
  • Optimal Status Enforcement in Abstract Argumentation. Andreas Niskanen, Johannes P. Wallner, and Matti Järvisalo. In ???, editors, Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), pages ???-???. AAAI Press, 2016.
  • LMHS: A SAT-IP Hybrid MaxSAT Solver. Paul Saikko, Jeremias Berg, and Matti Järvisalo. In Nadia Greignou and Daniel Le Berre, editors, Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016), volume ???? of Lecture Notes in Computer Science, pages ???-???. Springer, 2016.
  • Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation. Johannes P. Wallner, Andreas Niskanen, and Matti Järvisalo. In Dale Schuurmans and Michael Wellman, editors, Proceedings of the 30th AAAI Conference on Artificial Intelligence (AAAI 2016), pages 1088-1094. AAAI Press, 2016.
  • Boolean Satisfiability and Beyond: Algorithms, Analysis, and AI Applications. Matti Järvisalo. In ???, editors, Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), pages ???-???. AAAI Press, 2016.

Publications 2015

  • 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.
  • 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.
  • Weak Models of Distributed Computing, with Connections to Modal Logic. Lauri Hella, Matti Järvisalo, Antti Kuusisto, Juhana Laurinharju, Tuomo Lempiäinen, Kerkko Luosto, Jukka Suomela, and Jonni Virtema. Distributed Computing 28(1):31-53, 2015.
  • Complexity-Sensitive Decision Procedures for Abstract Argumentation (Extended Abstract). Wolfgang Dvořák, Matti Järvisalo, Johannes Peter Wallner, and Stefan Woltran. In Qiang Yang and Michael Wooldridge, editors, Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), pages 4073-4077. AAAI Press, 2015.
  • Learning Optimal Chain Graphs with Answer Set Programming. Dag Sonntag, Matti Järvisalo, Jose M. Peña, and Antti Hyttinen. In Tom Heskes and Marina Meila, editors, Proceedings of the 31st Conference on Uncertainty in Artificial Intelligence (UAI 2015), pages 822-831. AUAI Press, 2015.
  • Impact of Learning Strategies on the Quality of Bayesian Networks: An Empirical Evaluation. Brandon Malone, Matti Järvisalo, and Petri Myllymäki. In Tom Heskes and Marina Meila, editors, Proceedings of the 31st Conference on Uncertainty in Artificial Intelligence (UAI 2015), pages 362-371. AUAI Press, 2015.

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]

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 24 May 2016 by Matti Järvisalo - Page created on 6 Sep 2012 by Petri Myllymäki