Software

Solving Graph Problems via Potential Maximal Cliques

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

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

For the source code and more details, see here.

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 ???, editors, Proceedings of the 27th International Joint Conference on Artificial Intelligence and the 23rd European Conference on Artificial Intelligence (IJCAI-ECAI 2018), pages ???-???. 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 recently proposed in [2] as an natural generalization of extension enforcement.

For the source code and more details, 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]

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.

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.

For the source code and more details, see here.

Reference:

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.
[doi:10.3233/978-1-61499-672-9-551] [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]