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-

  • 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  ???, editors, Proceedings of the 15th European Conference on Logics in Artificial Intelligence (JELIA 2016), volume ???? of Lecture Notes in Computer Science, pages ???-???. Springer, 2016.
  • Boolean Satisfiability and Beyond: Algorithms, Analysis, and AI Applications. Matti Järvisalo. In Subbarao Kambhampati, editor, Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), pages 4066-4069 AAAI Press, 2016.
    [IJCAI 2016 Early Career Spotlight]
    [Publisher's version] [pdf] [abstract/bibtex]
  • 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]

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.

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