SATcha is a SAT-based system for outcome determination in judgment aggregation, implementing MaxSAT and PrefSAT based algorithms for various NP-hard judgment aggregation rules. The system covers preference aggregation as well as generic judgment aggregation.
For the source code, see [here].
Reference:
SAT-based Judgment Aggregation. Ari Conati, Andreas Niskanen, and Matti Järvisalo. In Proceedings of the 22nd International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2023), pages 1412-1420. ACM, 2023.
iMaxHS is an incremental MaxSAT solver which extends the implicit hitting set based solver MaxHS. Incrementality in iMaxHS is implemented by maintaining so-called conditional cores [1]. iMaxHS implements all of the functionality specified in IPAMIR, an incremental API for MaxSAT, including user-provided assumptions [1] and changing weights of soft clauses [2].
For the source code, see [here].
References:
[1] Incremental Maximum Satisfiability. Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. In Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), volume 236 of LIPIcs, pages 14:1-14:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
[2] Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights. Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. In Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), volume 210 of LIPIcs, pages 44:1--44:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
BiOptSat is solver for enumerating Pareto-optimal solutions to bi-objective MaxSAT instances, i.e., a boolean CNF formula with two pseudo-boolean objectives. The solver supports enumeration of all Pareto-optimal solutions and of one representative solutions per pair of optimal objectives values. Details on the algorithms implemented in BiOptSat are described in [1,2].
For the source code, see [here].
[1] MaxSAT-Based Bi-Objective Boolean Optimization. Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo. In Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), volume 236 of Leibniz International Proceedings in Informatics, pages 12:1-12:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
[doi:10.4230/LIPIcs.SAT.2022.12] [pdf] [abstract/bibtex]
[2] A Maximum Satisfiability Based Approach to Bi-Objective Boolean Optimization. Christoph Jabs. Master's thesis, University of Helsinki, 2022.
[http://urn.fi/URN:NBN:fi:hulib-202206132323]
PBO-IHS is a complete solver for pseudo-Boolean optimization, i.e., for 0-1 integer programs, implementing a implicit hitting set approach, as detailed in [1,2].
For the source code, see here.
References:
[1] Pseudo-Boolean Optimization by Implicit Hitting Sets. Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. In Laurent D. Michel, editor, Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), volume 210 of Leibniz International Proceedings in Informatics, pages 51:1-51:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
[doi:10.4230/LIPIcs.CP.2021.51] [pdf]
[2] Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization. Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. In ???, editor, Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022), volume ??? of Leibniz International Proceedings in Informatics, pages ??:1-??:??. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
[doi:???] [pdf] [abstract/bibtex]
CGSS2 is a complete core-guided (weighted partial) MaxSAT solver implemented in C++. CGSS2 implements the OLL algorithm with refined core relaxation step. It combines weight-aware core extraction---a recently proposed approach that enables relaxing multiple cores instead of a single one during iterations of core-guided search---with a novel form of structure sharing that decreases the size of the cardinality constraints and improves the propagation properties. For more details, see [1,2].
For the source code, see here.
References:
[1] Refined Core Relaxation for Core-Guided MaxSAT Solving. Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. In Laurent D. Michel, editor, Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), volume 210 of Leibniz International Proceedings in Informatics, pages 28:1-28:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
[doi:10.4230/LIPIcs.CP.2021.35] [pdf]
[2] Refined Core Relaxations for Core-Guided Maximum Satisfiability Algorithms. Hannes Ihalainen. Master's thesis, University of Helsinki, 2022.
[http://urn.fi/URN:NBN:fi:hulib-202211303909]
QBF-SMUSer is an optimizer for quantified Boolean formulas, and in particular geared for computing smallest MUSes of QBFs, implementing an implicit hitting set algorithm.
For the source code, see [here].
Reference:
Computing Smallest MUSes of Quantified Boolean Formulas. Andreas Niskanen, Jere Mustonen, Jeremias Berg, and Matti Järvisalo. In Proceedingss of 16th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2022), volume 13416 of Lecture Notes in Computer Science, pages 301-314. Springer, 2022.
SharpSAT-TD is an award-winning exact model counter supporting both weighted and unweighted model counting. SharpSAT-TD extends the SharpSAT model counter with tree-decomposition based heuristics and preprocessing, along with other features.
The source code is available here.
Reference:
Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters. Tuukka Korhonen and Matti Järvisalo. In Laurent D. Michel, editor, Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), volume 210 of Leibniz International Proceedings in Informatics, pages 8:1-8:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
[doi:10.4230/LIPIcs.CP.2021.8] [pdf] [abstract/bibtex]
ASPforASPIC+ implements reasoning in the structured argumentation formalism of ASPIC+ based on direct answer set programming (ASP) encodings and incremental ASP solving, as detailed in [1,2].
For source code and more details, see here.
References:
[1] An Answer Set Programming Approach to Argumentative Reasoning in the ASPIC+ Framework. Tuomo Lehtonen, Johannes P. Wallner, Matti Järvisalo. In Diego Calvanese, Esra Erdem, and Michael Thielscher, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), pages 636-646. IJCAI.org, 2020. [pdf]
[2] Computing Stable Conclusions under the Weakest-Link Principle in the ASPIC+ Argumentation Formalism. Tuomo Lehtonen, Johannes P. Wallner, Matti Järvisalo. In ???, editors, Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning (KR 2022), pages ???-???. IJCAI.org, 2022. [pdf]
ASPforABA implements reasoning in the structured argumentation formalism of assumption-based argumentation (ABA) by making use of anwer set programming (ASP) solving techniques. The approach, as detailed in [1,2], covers various central argumentation semantics and different reasoning modes through either direct ASP encodings or counterexample-guided abstraction refinement algorithms that make use of incremental ASP solving.
For the source code and more details, see here.
References:
[1] Declarative Algorithms and Complexity Results for Assumption-Based Argumentation. Tuomo Lehtonen, Johannes P. Wallner, Matti Järvisalo. Journal of Artificial Intelligence Research 71: 265-318, 2021. [pdf]
[2] Harnessing Incremental Answer Set Solving for Reasoning in Assumption-Based Argumentation. Tuomo Lehtonen, Johannes P. Wallner, Matti Järvisalo. Theory and Practice of Logic Programming 21(6): 717-734, 2021. [pdf]
selitae is a system for computing smallest explanations and diagnoses of acceptance and rejection in abstract argumentation based on MaxSAT and smallest-cardinality unsatisfiable core extraction.
For the source code, see [here].
References:
Smallest Explanations and Diagnoses of Rejection in Abstract Argumentation. Andreas Niskanen and Matti Järvisalo. Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), pages 667-671. IJCAI, 2020.
Computing Smallest MUSes of Quantified Boolean Formulas. Andreas Niskanen, Jere Mustonen, Jeremias Berg, and Matti Järvisalo. In Proceedingss of 16th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2022), volume 13416 of Lecture Notes in Computer Science, pages 301-314. Springer, 2022.
Loandra is an anytime solver for (weighted partial) maximum satisfiability (MaxSAT). It implements the so called core-boosted linear search algorithm, a three-stage search designed for computing low cost solutions of MaxSAT instances within a limited amount of time. In the first stage, the MaxPRE 2 preprocessor is used for simplifying the instance. In the second stage, a lower-bounding core-guided algorithm is invoked on the simplified instance. In the final stage, an upper bounding solution improving search is invoked on the last working instance of the core-guided search. Each stage is invoked under a time limit. The algorithm terminates either when finding an optimal (minimum-cost) solution---which can happen in any of the three stages---or when the solution improving search times out, at which point the lowest cost solution known 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]
MAGsl implements algorithms for learning Maximal Ancestral Graphs, including both a scorer
for computing Gaussian BIC local scores and an exact search algorithm for an optimal Maximal Ancestral Graph for with given BIC local scores. Details on the algorithms can be found in [1].
For the source code, see here.
[1] Maximal Ancestral Graph Structure Learning via Exact Search. Kari Rantanen, Antti Hyttinen, and Matti Järvisalo. In Cassio P. de Campos, Marloes H. Maathuis, and Erik Quaeghebeur,, editors, Proceedings of the 37th Conference on Uncertainty in Artificial Intelligence (UAI 2021), volume 161 of Proceedings of Machine Learning Research, pages 1237-1247. PMLR, 2021.
[pdf] [abstract/bibtex]
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:
Pace Solver Description: SMS. Tuukka Korhonen. In Yixin Cao and Marcin Pilipczuk, editors, Proceeding of the 15th International Symposium on Parameterized and Exact Computation (IPEC 2020), volume 180 of LIPIcs, pages 30:1-30:4. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
[preprint]
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]
Acceptance in Incomplete Argumentation Frameworks. Dorothea Baumeister, Matti Järvisalo, Daniel Neugebauer, Andreas Niskanen, and Jörg Rothe. Artificial Intelligence 295:103470, 2021.
[doi:10.1016/j.artint.2021.103470] [pdf] [abstract/bibtex]
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]
μ-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 Diego Calvanese, Esra Erdem, and Michael Thielscher, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), pages 800-804. AAAI Press, 2020.
[pdf] [abstract/bibtex]
Algorithms for Dynamic Argumentation Frameworks: An Incremental SAT-Based Approach. Andreas Niskanen and Matti Järvisalo. In Giuseppe De Giacomo, Alejandro Catala, Bistra Dilkina, Michela Milano, Senen Barro, Alberto Bugarin, and Jerome Lang, editors, Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020), volume 325 of Frontiers in Artificial Intelligence and Applications, pages 849-856. IOS Press, 2020.
[pdf] [abstract/bibtex]
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 Manfred Jaeger and Thomas Dyhre Nielsen, editors, Proceedings of the 10th International Conference on Probabilistic Graphical Models (PGM 2020), volume 138 of Proceedings of Machine Learning Research, pages 365-376. JMLR.org, 2020.
[pdf] [abstract/bibtex]
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]
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]
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]
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]
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]
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]
For the source code and more details, see here.
Reference:
A Core-Guided Approach to Learning Optimal Causal Graphs. Antti Hyttinen, Paul Saikko, and Matti Järvisalo. In Carles Sierra, editor, Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017), pages 645-651. AAAI Press, 2017.
[doi:10.24963/ijcai.2017/90] [pdf] [abstract/bibtex]
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]
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]
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]
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]
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]
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]
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]