Software

Exact Algorithm for Treedepth

SMS is an algorithm for computing an optimal treedepth decomposition of a graph.

SMS is based on branching on small minimal separators of the graph, implementing also several lower bound heuristics and preprocessing techniques.

For the source code, see here.

Reference:

SMS in PACE 2020. Tuukka Korhonen. In ???, editors, Proceeding of the 15th International Symposium on Parameterized and Exact Computation (IPEC 2020), volume ??? of LIPIcs, pages ??-??. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020 (to appear). 
[preprint]

SAT-based Reasoner for Incomplete and Control Argumentation Frameworks

Taeydennae is an implementation of a SAT-based approach to deciding acceptance in incomplete argumentation frameworks and controllability in control argumentation frameworks, supporting both credulous and skeptical reasoning and several semantics for which the problems are NP-hard.

For the source code, see here.

References:

Controllability of Control Argumentation Frameworks. Andreas Niskanen, Daniel Neugebauer, and Matti Järvisalo. In Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI-PRICAI 2020), pages 1855-1861. ijcai.org, 2020.
[pdf] [abstract/bibtex]

Deciding Acceptance in Incomplete Argumentation Frameworks. Andreas Niskanen, Daniel Neugebauer, Matti Järvisalo, and Jörg Rothe. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI 2020), pages 2942-2949. AAAI Press, 2020.
[pdf] [abstract/bibtex]

A Stochastic Local Search Approach for Learning Chordal Markov Networks

lsmarkov implements a stochastic local search approach for the computationally hard task of finding a chordal Markov network structure that maximizes a given scoring function.

For the source code, see here.

Reference:

Learning Chordal Markov Networks via Stochastic Local Search. Kari Rantanen, Antti Hyttinen, and Matti Järvisalo. In Giuseppe De Giacomo, Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín and Jérôme Lang, editors, Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020), volume 325 of Frontiers in Artificial Intelligence and Applications, pages 2632-2639. IOS Press, 2020.
[pdf] [abstract/bibtex]

SAT-based Argumentation Reasoner for Static and Dynamic ICCMA Problems

μ-toksia is a SAT-based reasoning engine supporting various abstract argumentation semantics and reasoning modes (credulous and skeptical reasoning, extension enumeration) as well as the problems of the dynamic tracks in the 2019 ICCMA competition.

For the source code, see here.

References:

μ-toksia: An Efficient Abstract Argumentation Reasoner. Andreas Niskanen and Matti Järvisalo. In ???, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), pages ???-???. AAAI Press, 2020.
[pdf] [abstract/bibtex]

Algorithms for Dynamic Argumentation Frameworks: An Incremental SAT-Based Approach. Andreas Niskanen and Matti Järvisalo. In ???, editors, Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020), volume ??? of Frontiers in Artificial Intelligence and Applications, pages ???-???. IOS Press, 2020.
[pdf] [abstract/bibtex]

Core-boosted Linear Search for Incomplete MaxSAT Solving

Loandra is an incomplete solver for (partial weighted) maximum satisfiability (MaxSAT). Loandra implements core-boosted linear search, a two stage search strategy for incomplete MaxSAT solving.  Initially the search starts in a core-guided (lower bounding) phase. If the first phase is unable to find an optimal solution the search switches to a linear (upper bounding) phase. The linear phase runs until either finding an optimal solution, or running out time, at which point the currently best known solution is returned. 

The solver is available here.

Reference: 

Core-Boosted Linear Search for Incomplete MaxSAT. Jeremias Berg, Emir Demirović, and Peter J. Stuckey. In  Louis-Martin Rousseau and Kostas Stergiou, editors, Proceedings of the 16th International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR 2019), volume 11494 of Lecture Notes in Computer Science, pages 39-56. Springer, 2019.
[doi:10.1007/978-3-030-19212-9_3]

Exact Branch-and-Bound for Causal Discovery

Bcause implements a practical exact problem-oriented branch-and-bound algorithm for discovering causal relations from sample data when allowing for latent con founding variables and feedback.

For the source code and more details, see here.

References:

Discovering Causal Graphs with Cycles and Latent Confounders: An Exact Branch-and-Bound Approach. Kari Rantanen, Antti Hyttinen, and Matti Järvisalo. International Journal of Approximate Reasoning 117:29-49, 2020.
[doi:10.1016/j.ijar.2019.10.009] [pdf] [abstract/bibtex]

Learning Optimal Cyclic Causal Graphs from Interventional Data. Kari Rantanen, Antti Hyttinen, and Matti Järvisalo. In ???, editors, Proceedings of the 10th International Conference on Probabilistic Graphical Models (PGM 2020), volume ??? of Proceedings of Machine Learning Research, pages ??-??. JMLR.org, 2020.
[pdf] [abstract/bibtex]

A Hybrid Approach to Optimization in Answer Set Programming

ASP-HS instantiates the implicit hitting set approach to optimization in the realm of answer set programming (ASP). The approach is based on iterative calls to a core extractor and hitting set optimizer, and extends the "plain" implicit hitting set approach with core minimization, disjoint cores, reduced cost fixing, bounds based on Clark's completion, and non-core constraints.

For the source code and more details, see here.

Reference:

A Hybrid Approach to Optimization in Answer Set Programming. Paul Saikko, Carmine Dodaro, Mario Alviano, and Matti Järvisalo. In Michael Thielscher, Francesca Toni, and Frank Wolter, editors, Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018), pages 32-41. AAAI Press, 2018.
[pdf] [abstract/bibtex]

Solving Graph Problems via Potential Maximal Cliques

Triangulator is an implementation of the Bouchitté-Todinca algorithm for finding optimal triangulations of graphs.

Triangulator can be used for finding an optimal solution for the following problems: The treewidth, minimum fill-in, and treelength of a graph, the generalized and fractional hypertreewidth of a hypergraph, the total table size of a Bayesian network, perfect phylogeny, and maximum compatibility of phylogenetic characters.

For the source code, see here.

References:

Finding Optimal Tree Decompositions. Tuukka Korhonen. Master's thesis, University of Helsinki 2020. [handle:10138/316589]

Finding Most Compatible Phylogenetic Trees over Multi-State Characters. Tuukka Korhonen and Matti Järvisalo. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI 2020), pages 1544-1551. AAAI Press, 2020.
[pdf] [abstract/bibtex]

Solving Graph Problems via Potential Maximal Cliques: An Experimental Evaluation of the Bouchitté-Todinca Algorithm. Tuukka Korhonen, Jeremias Berg, and Matti Järvisalo. ACM Journal of Experimental Algorithmics 24(1):1.9, 2019.
[doi:10.1145/3301297] [pdf] [abstract/bibtex]

SAT-based Reasoner for Abstract Dialectical Frameworks

For the source code and more details, see here.

Reference:

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. 
[pdf]

An Enumerator for Minimal Correction Subsets

LBX-cache is a tool for enumerating MCSes,  re-implementing the LBX algorithm extended with a caching mechanism for premise sets.

For downloading LB-cache and more details, see here.

Reference:

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]

A Branch-and-Bound Approach to Learning Optimal Decomposable Graphs 

BBMarkov implements an exact branch-and-bound search for learning optimal chordal Markov network structures with respect to given decomposable scoring functions.

For the source code and more details, see here.

Reference:

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.
[doi:???] [pdf] [abstract/bibtex]

An Extended MaxSAT Preprocessor

MaxPre is an open-source (MIT licensed) preprocessor for weighted partial maximum satisfiability (MaxSAT). MaxPre implements a range of well-known and recent SAT-based preprocessing techniques as well as MaxSAT-specific techniques that make use of weights of soft clauses. Furthermore, MaxPre offers solution reconstruction, cardinality constraint encoding, and an API for integration into SAT-based MaxSAT solvers with minimal I/O overhead.

For the source code and more details, see here.  

Reference:

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]

Reasoning in Structured Argumentation via Abstract Argumentation

Abstract argumentation frameworks (AFs) are a simple and powerful argumentation formalism. An AF consist of arguments and attacks between arguments. AFs are represented as directed graphs where arguments are vertices and attacks are edges. Assumption-based argumentation (ABA) is a form of structured argumentation, where the arguments are not just given, but their structure is explicit. In ABA, arguments are built from assumptions using rules. Attacks between arguments are determined by contraries, of which each assumption has one. ABA is in many senses an extension of abstract argumentation and queries about the acceptabilty of sentences in ABA under many semantics can be answered by translating the ABA framework to an AF and solving a corresponding reasoning task in the AF. This system does that translation, producing the necessary files which can be input to an ASP solver in order to answer the query.

For the implementation and more details, see here.

Reference:

From Structured to Abstract Argumentation: Assumption-Based Acceptance via AF Reasoning. Tuomo Lehtonen, Johannes P. Wallner, and Matti Järvisalo. in Alessandro Antonucci, Laurence Cholvy, and Odile Papini, editors, Proceedings of the 14th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2017), volume 10369 of Lecture Notes in Computer Science, pages 57-68. Springer, 2017.
[doi:10.1007/978-3-319-61581-3_6] [pdf] [abstract/bibtex]

A System for Enforcement in Abstract Argumentation

Extension enforcement is a form of AF dynamics that is concerned with enforcing a set of arguments to be an extension under a specified semantics of AFs via modifying the attack structure. Such an enforcement is strict if the set of arguments must be exactly an extension of the given semantics and non-strict if the set of arguments is a subset of an extension. Each modification of an attack incurs a cost. The software system Pakota implements extension (non-)strict enforcement under several semantics of AFs via constraint optimization solvers. In addition to extension enforcement, Pakota allows also to optimally solve the so-called status enforcement problem as an natural generalization of extension enforcement.

Update (8/2020): A new reimplementation of Pakota based on PySAT is available, now supporting so-called strong refinements on CEGAR algorithms for second-level problem variants.

For the source code, see here.

References:

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]

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]

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.

Strong Refinements for Hard Problems in Argumentation Dynamics. Andreas Niskanen and Matti Järvisalo. In ???, editors, Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020), volume ??? of Frontiers in Artificial Intelligence and Applications, pages ???-???. IOS Press, 2020.
[pdf] [abstract/bibtex]

Synthesizing Argumentation Frameworks from Examples

AF synthesis is a natural generalization of realizability in abstract argumentation. Given a semantics and a set of extensions, realizability is the problem of deciding whether there exists an AF which exactly represents the extensions. The AF synthesis problem allows for studying realizability under incomplete and noisy information. In AF synthesis, we are given a set of positive and a set of negative examples, corresponding to extensions and non-extensions, along with weights associated to each example, expressing the relative trust. The task is to find an AF which optimally represents the examples by minimizing the costs, incurred by including a negative example or not including a positive example in the set of extensions.

AFSynth implements AF synthesis under the conflict-free, admissible and stable semantics via encoding the problem as a weighted partial MaxSAT instance and calling the corresponding solver.

Update (8/2020): A new reimplementation of AFSynth based on PySAT is available, now supporting so-called strong refinements on CEGAR algorithms for second-level problem variants.

For the source code, see here.

References:

Synthesizing Argumentation Frameworks from Examples. Andreas Niskanen, Johannes P. Wallner, and Matti Järvisalo. Journal of Artificial Intelligence Research 65:504-554, 2019.
[doi:10.1613/jair.1.11758] [pdf] [abstract/bibtex]

Strong Refinements for Hard Problems in Argumentation Dynamics. Andreas Niskanen and Matti Järvisalo. In ???, editors, Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020), volume ??? of Frontiers in Artificial Intelligence and Applications, pages ???-???. IOS Press, 2020.
[pdf] [abstract/bibtex]

Propositional Abduction by Implicit Hitting Sets

AbHS is implements a hybrid SAT-IP approach to the propositional propositional abduction problem based on the implicit hitting set paradigm.

For the source code and more details, see here.

Reference:

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]

A Hybrid SAT-IP MaxSAT Solver

LMHS is a from-scratch MaxSAT solver implementation based on the implicit hitting set approach using interacting SAT and IP solvers, as first implemented in the MaxHS solver.

For the source code and more details, see here.

Reference:

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]

A SAT-based Abstract Argumentation Reasoning System

CEGARTIX is an abstract argumentation reasoner, implementing SAT-based approaches to acceptance problems over argumentation frameworks under various central NP-hard argumentation semantics.

For the source code and more details, see here.

Reference:

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]

A SAT-based Procedure for Learning Causal Models

For the source code, see here.

Reference:

Discovering Cyclic Causal Models with Latent Variables: A General SAT-Based Procedure. Antti Hyttinen, Patrik Hoyer, Frederick Eberhardt, and Matti Järvisalo. 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. [pdf] [abstract/bibtex]