Arrow Research search

Author name cluster

Matti Järvisalo

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

82 papers
2 author rows

Possible papers

82

AAAI Conference 2026 Conference Paper

Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach

  • Hannes Ihalainen
  • Dieter Vandesande
  • André Schidler
  • Jeremias Berg
  • Bart Bogaerts
  • Matti Järvisalo

The implicit hitting set (IHS) approach offers a general framework for solving computationally hard combinatorial optimization problems declaratively. IHS iterates between a decision oracle used for extracting sources of inconsistency and an optimizer for computing so-called hitting sets (HSs) over the accumulated sources of inconsistency. While the decision oracle is language-specific, the optimizers is usually instantiated through integer programming. We explore alternative algorithmic techniques for hitting set optimization based on different ways of employing pseudo-Boolean (PB) reasoning as well as stochastic local search. We extensively evaluate the practical feasibility of the alternatives in particular in the context of pseudo-Boolean (0-1 IP) optimization as one of the most recent instantiations of IHS. Highlighting a trade-off between efficiency and reliability, while a commercial IP solver turns out to remain the most effective way to instantiate HS computations, it can cause correctness issues due to numerical instability; in fact, we show that exact HS computations instantiated via PB reasoning can be made competitive with a numerically exact IP solver. Furthermore, the use of PB reasoning as a basis for HS computations allows for obtaining certificates for the correctness of IHS computations, generally applicable to any IHS instantiation in which reasoning in the declarative language at hand can be captured in the PB-based proof format we employ.

PDF Details DOI

AAAI Conference 2026 Conference Paper

Ordered Objectives in Maximum Satisfiability

  • Jeremias Berg
  • André Schidler
  • Matti Järvisalo

Maximum satisfiability (MaxSAT) is a viable approach to solving NP-hard combinatorial optimization problems through propositional encodings. Understanding how problem structure and encodings impact the behaviour of different MaxSAT solving algorithms is an important challenge. In this work, we identify MaxSAT instances in which the constraints entail an ordering of the objective variables as an interesting instance class from the perspectives of problem structure and MaxSAT solving. From the problem structure perspective, we show that a non-negligible percentage of instances in commonly used MaxSAT benchmark sets have ordered objectives and further identify various examples of such problem domains to which MaxSAT solvers have been successfully applied. From the algorithmic perspective, we argue that MaxSAT instances with ordered objectives, provided an ordering, can be solved (at least) as efficiently with a very simplistic algorithmic approach as with modern core-based MaxSAT solving algorithms. We show empirically that state-of-the-art MaxSAT solvers suffer from overheads and are outperformed by the simplistic approach on real-world optimization problems with ordered objectives.

PDF Details DOI

AAAI Conference 2026 Conference Paper

Symmetry Breaking for Inductive Logic Programming

  • Andrew Cropper
  • David M. Cerna
  • Matti Järvisalo

The goal of inductive logic programming (ILP) is to search for a hypothesis that generalises training data and background knowledge. The challenge is searching vast hypothesis spaces, which is exacerbated because many logically equivalent hypotheses exist. To address this challenge, we introduce a method to break symmetries in the hypothesis space. We implement our idea in answer set programming. Our experiments on multiple domains, including visual reasoning and game playing, show that our approach can reduce solving times from over an hour to just 17 seconds.

PDF Details DOI

JAIR Journal 2025 Journal Article

Argumentative Reasoning in ASPIC+ under Incomplete Information

  • Daphne Odekerken
  • Tuomo Lehtonen
  • Johannes P. Wallner
  • Matti Järvisalo

Reasoning under incomplete information is an important research direction in the study of computational argumentation. Most advances in this direction so far have focused on abstract argumentation frameworks. In particular, development of computational approaches to reasoning under incomplete information in structured formalisms remains to a large extent a challenge. We address this challenge by studying the problems of determining stability and relevance—with the aim of analyzing aspects of resilience of acceptance statuses in light of new information—in the central structured formalism of ASPIC+. The specific ASPIC+ instantiation and grounded argumentation semantics we focus on are motivated by current applications in criminal investigation at the Netherlands Police. Our contributions consist of a theoretical analysis of the complexity of deciding stability and relevance as well as first exact algorithms for reasoning about stability and relevance in incomplete ASPIC+ theories. In terms of complexity results, we show that deciding stability is coNP-complete for incomplete ASPIC+ when assuming a preference ordering on defeasible rules via the last-link ordering, while deciding relevance is significantly more complex, namely NP^NP-complete. Complementing the complexity results, we develop practical algorithms for deciding stability and relevance based on the declarative paradigm of answer set programming (ASP). Furthermore, we provide an open-source implementation of the algorithms, and show empirically that the implementation exhibits promising scalability on both real-world and synthetic data. Our exact approach to stability is competitive with a previously proposed inexact approach, and the run times of our algorithms for both stability and relevance are sufficiently low on real-world data to be used in online settings.

PDF Details DOI

AAMAS Conference 2025 Conference Paper

Computing Efficient and Envy-Free Allocations under Dichotomous Preferences using SAT

  • Ari Conati
  • Andreas Niskanen
  • Ronald de Haan
  • Matti Järvisalo

We study the problems of computing envy-free Pareto-efficient allocations in the context of fair allocation and hedonic games under dichotomous preferences. We establish Σ p 2-completeness of deciding the existence of envy-free Pareto-efficient allocations, refining earlier related results. We also develop iterative SAT-based exact algorithms for computing envy-free Pareto-efficient allocations, and extend the approach to computing minimum-envy Pareto-efficient allocations under different combinations of aggregation functions. We provide open-source implementations of the algorithms and show empirically that the approach scales to computing envy-free Pareto-efficient allocations up to hundreds of agents.

PDF

KR Conference 2025 Conference Paper

Cost-Optimal Delete-Free Classical Planning via Maximum Satisfiability

  • Masood Feyzbakhsh Rankooh
  • Andreas Niskanen
  • Matti Järvisalo

We propose a maximum satisfiability (MaxSAT) based approach to cost-optimal delete-free planning, also known as optimal relaxed planning. Relaxed planning is a central subclass of classical planning, consisting of computing the h+ heuristic for classical planning. As an alternative to the existing approaches to exactly computing h+, we propose a maximum satisfiability (MaxSAT) based approach, motivated by the success of SAT-based planners and significant recent advances in MaxSAT solvers. Concretely, we both adapt a recent answer set optimization approach to computing h+ for MaxSAT, propose further MaxSAT encoding variants for both representing cost-optimal plans and plan acyclicity, and combine them for further runtime improvements. Overall, our MaxSAT approach compares favourably to the current state-of-the-art answer set optimization approach.

PDF Details DOI

AIJ Journal 2025 Journal Article

ICCMA 2023: 5th International Competition on Computational Models of Argumentation

  • Matti Järvisalo
  • Tuomo Lehtonen
  • Andreas Niskanen

The study of computational models of argumentation and the development of practical automated approaches to reasoning over the models has developed into a vibrant area of artificial intelligence research in recent years. The series of International Competitions on Computational Models of Argumentation (ICCMA) aims at nurturing research and development of practical reasoning algorithms for models of argumentation. Organized biennially, the ICCMA competitions provide a snapshot of the current state of the art in algorithm implementations for central fundamental reasoning tasks over models of argumentation. The year 2023 marked the 5th instantiation of International Competitions on Computational Models of Argumentation, ICCMA 2023. We provide a comprehensive overview of ICCMA 2023, including details on the various new developments introduced in 2023, overview of the participating solvers, extensive details on the competition benchmarks and results, as well as lessons learned.

Details DOI

KR Conference 2025 Conference Paper

Reasoning in Assumption-Based Argumentation via SAT

  • Andreas Niskanen
  • Masood Feyzbakhsh Rankooh
  • Tuomo Lehtonen
  • Matti Järvisalo

The dominant approaches for solving NP-hard reasoning problems in computational argumentation are declarative—namely, Boolean satisfiability (SAT) in the case of abstract argumentation and answer set programming (ASP) in the case of structured formalisms such as assumption-based argumentation (ABA). ASP is particularly suited for the commonly-studied logic programming variant of ABA as acyclic derivations in ABA can be naturally modelled in ASP. In this work, we develop and evaluate various alternative approaches to realizing SAT-based reasoning for ABA, motivated by the success of SAT solvers in the realm of abstract argumentation. In contrast to ASP, non-trivial encodings or extensions to SAT solvers are needed to efficiently handle the acyclicity constraint underlying ABA reasoning. We develop and evaluate both advanced encodings and user-defined propagation mechanisms for realizing efficient SAT-based reasoning in ABA. As a result, we provide a first SAT-based ABA reasoner that can outperform the current state-of-the-art ASP approach to ABA.

PDF Details DOI

ECAI Conference 2024 Conference Paper

Complexity Results and Algorithms for Manipulation and Bribery in Judgment Aggregation

  • Ari Conati
  • Andreas Niskanen
  • Ronald de Haan
  • Matti Järvisalo

The study of limits of strategic behavior in collective decision making is a central topic in computational social choice. Focusing on judgment aggregation, we provide complexity results and algorithms for manipulation and bribery under various aggregation rules. Specifically, we show that manipulation and bribery are complete for the second level of the Polynomial Hierarchy and detail aggregation-rule-specific strong refinements for effective counterexample-guided abstraction refinement algorithms based on iterative calls to a maximum satisfiability solver for both manipulation and bribery. We provide an open-source implementation of the approach and empirically evaluate its performance on standard PrefLib datasets, showing that the strong refinement strategies developed in this work enable scaling up to solving more instances.

Details

KR Conference 2024 Conference Paper

Complexity Results and Algorithms for Preferential Argumentative Reasoning in ASPIC+

  • Tuomo Lehtonen
  • Daphne Odekerken
  • Johannes P. Wallner
  • Matti Järvisalo

We provide complexity results and algorithms for reasoning in the central structured argumentation formalism of ASPIC+. Considering ASPIC+ accommodated with preferences under the last-link principle, the results are made possible by rephrasing several argumentation semantics---admissible, complete, stable, preferred and grounded---in terms of defeasible elements of an ASPIC+ theory for both democratic and elitist last-link lifting. Via the rephrasing, we establish that acceptance is polynomial-time computable under grounded semantics, and complete for either NP, coNP, or Pi_P^2, depending on the reasoning mode and semantics. We also detail answer set programming encodings for deciding acceptance for the NP/coNP-complete reasoning tasks, and empirically show that it scales significantly better than first translating ASPIC+ reasoning tasks to abstract argumentation. Finally, we show that, in contrast to the last-link principle, it is NP-hard to compute the grounded extension under the weakest-link principle.

PDF Details DOI

JAIR Journal 2024 Journal Article

Declarative Approaches to Outcome Determination in Judgment Aggregation

  • Ari Conati
  • Andreas Niskanen
  • Matti Järvisalo

Judgment aggregation (JA) offers a generic formal framework for modeling various settings involving information aggregation by social choice mechanisms. For many judgment aggregation rules, computing collective judgments is computationally notoriously hard. The central outcome determination problem, in particular, is often complete for higher levels of the polynomial hierarchy. This complexity barrier makes it challenging to develop practical exact algorithms to outcome determination. Taking on this challenge, in this work we develop practical exact algorithms for outcome determination under a range of the most central JA rules—namely Kemeny, Slater, MaxHamming, Young, Dodgson, Reversal scoring, Condorcet, Ranked agenda, and LexiMax—by harnessing the declarative approach, in particular, Boolean satisfiability (SAT) and integer programming techniques. For the Kemeny, Slater, MaxHamming, Young, and Dodgson rules, we detail direct approaches based on maximum satisfiability (MaxSAT) and integer programming. For the Reversal scoring, Condorcet, Ranked agenda, and LexiMax rules, we develop iterative algorithms, including algorithms based on the counterexample-guided abstraction refinement (CEGAR) paradigm, making use of recent advances in incremental MaxSAT solving and preferential SAT-based reasoning. We provide an open-source implementation of the algorithms, and empirically evaluate them using real-world preference data. We compare the performance of our implementation to a recent approach which makes use of declarative solver technology for answer set programming (ASP). The results demonstrate that our approaches scale significantly beyond the reach of the ASP-based algorithms for all of the judgment aggregation rules considered.

PDF Details DOI

JAIR Journal 2024 Journal Article

From Single-Objective to Bi-Objective Maximum Satisfiability Solving

  • Christoph Jabs
  • Jeremias Berg
  • Andreas Niskanen
  • Matti Järvisalo

The declarative approach is key to efficiently finding optimal solutions to various types of NP-hard real-world combinatorial optimization problems. Most work on practical declarative solvers—ranging from classical integer programming to finite-domain constraint optimization and maximum satisfiability (MaxSAT)—has focused on optimization under a single objective; fewer advances have been made towards efficient declarative techniques for multi-objective optimization problems. Motivated by significant recent advances in practical solvers for MaxSAT, in this work we develop BiOptSat, an exact declarative approach for finding Pareto-optimal solutions to bi-objective optimization problems, with propositional logic as the underlying constraint language. BiOptSat can be viewed as an instantiation of the lexicographic method. The approach makes use of a single Boolean satisfiability solver that is incrementally employed throughout the entire search procedure, allowing for finding a single Pareto-optimal solution, finding one representative solution for each non-dominated point, and enumerating all Pareto-optimal solutions. We detail several algorithmic instantiations of BiOptSat, each building on recent algorithms proposed for single-objective MaxSAT. We empirically evaluate the instantiations compared to recently-proposed alternative approaches to multi-objective MaxSAT solving on several real-world domains from the literature, showing the practical benefits of our approach.

PDF Details DOI

IJCAI Conference 2024 Conference Paper

Learning Big Logical Rules by Joining Small Rules

  • Céline Hocquette
  • Andreas Niskanen
  • Rolf Morel
  • Matti Järvisalo
  • Andrew Cropper

A major challenge in inductive logic programming is learning big rules. To address this challenge, we introduce an approach where we join small rules to learn big rules. We implement our approach in a constraint-driven system and use constraint solvers to efficiently join rules. Our experiments on many domains, including game playing and drug design, show that our approach can (i) learn rules with more than 100 literals, and (ii) drastically outperform existing approaches in terms of predictive accuracies.

PDF Details DOI

AAAI Conference 2024 Conference Paper

Learning MDL Logic Programs from Noisy Data

  • Céline Hocquette
  • Andreas Niskanen
  • Matti Järvisalo
  • Andrew Cropper

Many inductive logic programming approaches struggle to learn programs from noisy data. To overcome this limitation, we introduce an approach that learns minimal description length programs from noisy data, including recursive programs. Our experiments on several domains, including drug design, game playing, and program synthesis, show that our approach can outperform existing approaches in terms of predictive accuracies and scale to moderate amounts of noise.

PDF Details DOI

ECAI Conference 2024 Conference Paper

SAT-Based Approaches to Reasoning in Choice Logics

  • Tuomo Lehtonen
  • Andreas Niskanen
  • Matti Järvisalo

Representing and reasoning about preferences is a fundamental task in artificial intelligence. Various logic-based languages for representing preferences have been proposed. However, developing practical algorithms for reasoning in such logic-based languages remains a challenge due to high computational complexity. In this work, we develop practical algorithms based on Boolean satisfiability (SAT) for computing preferred models and for deciding preferred model entailment in qualitative and conjunctive choice logics QCL and CCL under the so-called minmax, lexicographic, and inclusion-based preference semantics. For each of the problem variants, we detail an algorithm which adheres to the computational complexity of the reasoning task, based on either maximum satisfiability (MaxSAT) or SAT with preferences (PrefSAT) solvers. We empirically evaluate our implementation of the algorithms, and show that our approach scales significantly better than a recently proposed answer set programming approach to computing preferred models.

Details

JAIR Journal 2024 Journal Article

Unifying SAT-Based Approaches to Maximum Satisfiability Solving

  • Hannes Ihalainen
  • Jeremias Berg
  • Matti Järvisalo

Maximum satisfiability (MaxSAT), employing propositional logic as the declarative language of choice, has turned into a viable approach to solving NP-hard optimization problems arising from artificial intelligence and other real-world settings. A key contributing factor to the success of MaxSAT is the rise of increasingly effective exact solvers that are based on iterative calls to a Boolean satisfiability (SAT) solver. The three types of SAT-based MaxSAT solving approaches, each with its distinguishing features, implemented in current state-of-the-art MaxSAT solvers are the core-guided, the implicit hitting set (IHS), and the objective-bounding approaches. The objective-bounding approach is based on directly searching over the objective function range by iteratively querying a SAT solver if the MaxSAT instance at hand has a solution under different bounds on the objective. In contrast, both core-guided and IHS are so-called unsatisfiability-based approaches that employ a SAT solver as an unsatisfiable core extractor to determine sources of inconsistencies, but critically differ in how the found unsatisfiable cores are made use of towards finding a provably optimal solution. Furthermore, a variety of different algorithmic variants of the core-guided approach in particular have been proposed and implemented in solvers. It is well-acknowledged that each of the three approaches has its advantages and disadvantages, which is also witnessed by instance and problem-domain specific runtime performance differences (and at times similarities) of MaxSAT solvers implementing variants of the approaches. However, the questions of to what extent the approaches are fundamentally different and how the benefits of the individual methods could be combined in a single algorithmic approach are currently not fully understood. In this work, we approach these questions by developing UniMaxSAT, a general unifying algorithmic framework. Based on the recent notion of abstract cores, UniMaxSAT captures in general core-guided, IHS and objective-bounding computations. The framework offers a unified way of establishing quite generally the correctness of the current approaches. We illustrate this by formally showing that UniMaxSAT can simulate the computations of various algorithmic instantiations of the three types of MaxSAT solving approaches. Furthermore, UniMaxSAT can be instantiated in novel ways giving rise to new algorithmic variants of the approaches. We illustrate this aspect by developing a prototype implementation of an algorithmic variant for MaxSAT based on the framework.

PDF Details DOI

KR Conference 2023 Conference Paper

Argumentative Reasoning in ASPIC+ under Incomplete Information

  • Daphne Odekerken
  • Tuomo Lehtonen
  • Annemarie Borg
  • Johannes P. Wallner
  • Matti Järvisalo

Reasoning under incomplete information is an important research direction in AI argumentation. Most computational advances in this direction have so-far focused on abstract argumentation frameworks. Development of computational approaches to reasoning under incomplete information in structured formalisms remains to-date to a large extent a challenge. We address this challenge by studying the so-called stability and relevance problems---with the aim of analyzing aspects of resilience of acceptance statuses in light of new information---in the central structured formalism of ASPIC+. Focusing on the case of the grounded semantics and an ASPIC+ fragment motivated through application scenarios, we develop exact ASP-based algorithms for stability and relevance in incomplete ASPIC+ theories, and pinpoint the complexity of reasoning about stability (coNP-complete) and relevance (Sigma_2^P-complete), further justifying our ASP-based approaches. Empirically, the algorithms exhibit promising scalability, outperforming even a recent inexact approach to stability, with our ASP-based iterative approach being the first algorithm proposed for reasoning about relevance in ASPIC+.

PDF Details DOI

JELIA Conference 2023 Conference Paper

Computing MUS-Based Inconsistency Measures

  • Isabelle Kuhlmann
  • Andreas Niskanen
  • Matti Järvisalo

Abstract We detail two instantiations of a generic algorithm for the problematic and MUS-variable-based inconsistency measures, based on answer set programming and Boolean satisfiability (SAT). Empirically, the SAT-based approach allows for more efficiently computing the measures when compared to enumerating all minimal correction subsets of a knowledge base.

Details

ECAI Conference 2023 Conference Paper

MaxSAT-Based Inconsistency Measurement

  • Andreas Niskanen
  • Isabelle Kuhlmann
  • Matthias Thimm
  • Matti Järvisalo

Inconsistency measurement aims at obtaining a quantitative assessment of the level of inconsistency in knowledge bases. While having such a quantitative assessment is beneficial in various settings, inconsistency measurement of propositional knowledge bases is under most existing measures a significantly challenging computational task. In this work, we harness Boolean satisfiability (SAT) based solving techniques for developing practical inconsistency measurement algorithms. Our algorithms—some of which constitute, to the best of our knowledge, the first practical approaches for specific inconsistency measures—are based on using natural choices of SAT-based techniques for the individual inconsistency measures, ranging from direct maximum satisfiability (MaxSAT) encodings to MaxSAT-based column generation techniques making use of incremental computations. We show through an extensive empirical evaluation that our approaches scale well in practice and significantly outperform recently-proposed answer set programming approaches to inconsistency measurement.

Details

ECAI Conference 2023 Conference Paper

Oracle-Based Local Search for Pseudo-Boolean Optimization

  • Ashlin Iser
  • Jeremias Berg
  • Matti Järvisalo

Significant advances have been recently made in the development of increasingly effective in-exact (or incomplete) search algorithms—particularly geared towards finding good though not provably optimal solutions fast—for the constraint optimization paradigm of maximum satisfiability (MaxSAT). One of the most successful recent approaches is a new type of stochastic local search in which a Boolean satisfiability (SAT) solver is used as a decision oracle for moving from a solution to another. In this work, we strive for extending the success of the approach to the more general realm of pseudo-Boolean optimization (PBO), where constraints are expressed as linear inequalities over binary variables. As a basis for the approach, we make use of recent advances in practical approaches to satisfiability checking pseudo-Boolean constraints. We outline various heuristics within the oracle-based approach to anytime PBO solving, and show that the approach compares in practice favorably both to a recently-proposed local search approach for PBO that is in comparison a more traditional instantiation of the stochastic local search paradigm as well as a recent exact PBO approach when used as an anytime solver.

Details

AAMAS Conference 2023 Conference Paper

SAT-based Judgment Aggregation

  • Ari Conati
  • Andreas Niskanen
  • Matti Järvisalo

Judgment aggregation (JA) offers a generic formal logical framework for modeling various settings where agents must reach joint agreements through aggregating the preferences, judgments, or beliefs of individual agents by social choice mechanisms. In this work, we develop practical JA algorithms for outcome determination by harnessing Boolean satisfiability (SAT) based solvers as the underlying reasoning engines, leveraging on their ability to efficiently reason over logical representations incrementally. Concretely, we provide algorithms for outcome determination under a range of aggregation rules, using natural choices of SAT-based techniques adhering to the computational complexity of the problem for the individual rules. We also implement and empirically evaluate the approach using both synthetic and PrefLib data, showing that the approach can scale significantly beyond recently proposed alternative algorithms for JA.

PDF

IJCAI Conference 2023 Conference Paper

Unifying Core-Guided and Implicit Hitting Set Based Optimization

  • Hannes Ihalainen
  • Jeremias Berg
  • Matti Järvisalo

Two of the most central algorithmic paradigms implemented in practical solvers for maximum satisfiability (MaxSAT) and other related declarative paradigms for NP-hard combinatorial optimization are the core-guided (CG) and implicit hitting set (IHS) approaches. We develop a general unifying algorithmic framework, based on the recent notion of abstract cores, that captures both CG and IHS computations. The framework offers a unified way of establishing the correctness of variants of the approaches, and can be instantiated in novel ways giving rise to new algorithmic variants of the core-guided and IHS approaches. We illustrate the latter aspect by developing a prototype implementation of an algorithm variant for MaxSAT based on the framework.

PDF Details DOI

KR Conference 2022 Conference Paper

Computing Stable Conclusions under the Weakest-Link Principle in the ASPIC+ Argumentation Formalism

  • Tuomo Lehtonen
  • Johannes P. Wallner
  • Matti Järvisalo

Rephrasing argumentation semantics in terms of subsets of defeasible elements allows for gaining new insights for reasoning about acceptance in established fragments of the central structured argumentation formalism of ASPIC+. We provide a non-trivial generalization of these recent results, capturing preferences in ASPIC+. In particular, considering preferences under the weakest-link principle, we show that the stable semantics can be phrased in terms of subsets of defeasible elements. We employ the rephrasing for establishing both complexity results and practical algorithms for reasoning about acceptance in this variant of ASPIC+. Justified by completeness for the second level of the polynomial hierarchy, we develop an iterative answer set solving based approach to reasoning about acceptance under the so-called elitist lifting in ASPIC+ frameworks. Our implementation of the approach scales well in practice.

PDF Details DOI

SAT Conference 2022 Conference Paper

Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization

  • Pavel Smirnov 0003
  • Jeremias Berg
  • Matti Järvisalo

The development of practical approaches to efficiently reasoning over pseudo-Boolean constraints has recently increasing attention as a natural generalization of Boolean satisfiability (SAT) solving. Analogously, solvers for pseudo-Boolean optimization draw inspiration from techniques developed for maximum satisfiability (MaxSAT) solving. Recently, the first practical solver lifting the implicit hitting set (IHS) approach - one of the most efficient approaches in modern MaxSAT solving - to the realm of PBO was developed, employing a PB solver as a core extractor together with an integer programming solver as a hitting set solver. In this work, we make practical improvements to the IHS approach to PBO. We propose the integration of solution-improving search to the PBO-IHS approach, resulting in a hybrid approach to PBO which makes use of both types of search towards an optimal solution. Furthermore, we explore the potential of different variants of core extraction within PBO-IHS - including recent advances in PB core extraction, allowing for extracting more general PB constraints compared to the at-least-one constraints typically relied on in IHS - in speeding up PBO-IHS search. We show that the empirical efficiency of PBO-IHS - recently shown to outperform other specialized PBO solvers - is further improved by the integration of these techniques.

Details

SAT Conference 2022 Conference Paper

Incremental Maximum Satisfiability

  • Andreas Niskanen
  • Jeremias Berg
  • Matti Järvisalo

Boolean satisfiability (SAT) solvers allow for incremental computations, which is key to efficient employment of SAT solvers iteratively for developing complex decision and optimization procedures, including maximum satisfiability (MaxSAT) solvers. However, enabling incremental computations on the level of constraint optimization remains a noticeable challenge. While incremental computations have been identified to have great potential in speeding up MaxSAT-based approaches for solving various real-world optimization problems, enabling incremental computations in MaxSAT remains to most extent unexplored. In this work, we contribute towards making incremental MaxSAT solving a reality. Firstly, building on the IPASIR interface for incremental SAT solving, we propose the IPAMIR interface for implementing incremental MaxSAT solvers and for developing applications making use of incremental MaxSAT. Secondly, we expand our recent adaptation of the implicit hitting set based MaxHS MaxSAT solver to a fully-fledged incremental MaxSAT solver in terms of implementing the IPAMIR specification in full, and detail in particular how, in addition to weight changes, assumptions are enabled without losing incrementality. Thirdly, we provide further empirical evidence on the benefits of incremental MaxSAT solving under assumptions.

Details

SAT Conference 2022 Conference Paper

MaxSAT-Based Bi-Objective Boolean Optimization

  • Christoph Jabs
  • Jeremias Berg
  • Andreas Niskanen
  • Matti Järvisalo

We explore a maximum satisfiability (MaxSAT) based approach to bi-objective optimization. Bi-objective optimization refers to the task of finding so-called Pareto-optimal solutions in terms of two objective functions. Bi-objective optimization problems naturally arise in various real-world settings. For example, in the context of learning interpretable representations, such as decision rules, from data, one wishes to balance between two objectives, the classification error and the size of the representation. Our approach is generally applicable to bi-objective optimizations which allow for propositional encodings. The approach makes heavy use of incremental Boolean satisfiability (SAT) solving and draws inspiration from modern MaxSAT solving approaches. In particular, we describe several variants of the approach which arise from different approaches to MaxSAT solving. In addition to computing a single representative solution per each point of the Pareto front, the approach allows for enumerating all Pareto-optimal solutions. We empirically compare the efficiency of the approach to recent competing approaches, showing practical benefits of our approach in the contexts of learning interpretable classification rules and bi-objective set covering.

Details

AIJ Journal 2021 Journal Article

Acceptance in incomplete argumentation frameworks

  • Dorothea Baumeister
  • Matti Järvisalo
  • Daniel Neugebauer
  • Andreas Niskanen
  • Jörg Rothe

argumentation frameworks (AFs), originally proposed by Dung, constitute a central formal model for the study of computational aspects of argumentation in AI. Credulous and skeptical acceptance of arguments in a given AF are well-studied problems both in terms of theoretical analysis—especially computational complexity—and the development of practical decision procedures for the problems. However, AFs make the assumption that all attacks between arguments are certain (i. e. , present attacks are known to exist, and missing attacks are known to not exist), which can in various settings be a restrictive assumption. A generalization of AFs to incomplete AFs was recently proposed as a formalism that allows the representation of both uncertain attacks and uncertain arguments in AFs. In this article, we explore the impact of allowing for modeling such uncertainties in AFs on the computational complexity of natural generalizations of acceptance problems to incomplete AFs under various central AF semantics. Complementing the complexity-theoretic analysis, we also develop the first practical decision procedures for all of the NP-hard variants of acceptance in incomplete AFs. In terms of complexity analysis, we establish a full complexity landscape, showing that depending on the variant of acceptance and property/semantics, the complexity of acceptance in incomplete AFs ranges from polynomial-time decidable to completeness for Σ 3 p. In terms of algorithms, we show through an extensive empirical evaluation that an implementation of the proposed decision procedures, based on boolean satisfiability (SAT) solving, is effective in deciding variants of acceptance under uncertainties. We also establish conditions for what type of atomic changes are guaranteed to be redundant from the perspective of preserving extensions of completions of incomplete AFs, and show that the results allow for considerably improving the empirical efficiency of the proposed SAT-based counterexample-guided abstraction refinement algorithms for acceptance in incomplete AFs for problem variants with complexity beyond NP.

Details DOI

JAIR Journal 2021 Journal Article

Declarative Algorithms and Complexity Results for Assumption-Based Argumentation

  • Tuomo Lehtonen
  • Johannes P. Wallner
  • Matti Järvisalo

The study of computational models for argumentation is a vibrant area of artificial intelligence and, in particular, knowledge representation and reasoning research. Arguments most often have an intrinsic structure made explicit through derivations from more basic structures. Computational models for structured argumentation enable making the internal structure of arguments explicit. Assumption-based argumentation (ABA) is a central structured formalism for argumentation in AI. In this article, we make both algorithmic and complexity-theoretic advances in the study of ABA. In terms of algorithms, we propose a new approach to reasoning in a commonly studied fragment of ABA (namely the logic programming fragment) with and without preferences. While previous approaches to reasoning over ABA frameworks apply either specialized algorithms or translate ABA reasoning to reasoning over abstract argumentation frameworks, we develop a direct declarative approach to ABA reasoning by encoding ABA reasoning tasks in answer set programming. We show via an extensive empirical evaluation that our approach significantly improves on the empirical performance of current ABA reasoning systems. In terms of computational complexity, while the complexity of reasoning over ABA frameworks is well-understood, the complexity of reasoning in the ABA+ formalism integrating preferences into ABA is currently not fully established. Towards bridging this gap, our results suggest that the integration of preferential information into ABA via so-called reverse attacks results in increased problem complexity for several central argumentation semantics.

PDF Details DOI

UAI Conference 2021 Conference Paper

Maximal ancestral graph structure learning via exact search

  • Kari Rantanen
  • Antti Hyttinen
  • Matti Järvisalo

Generalizing Bayesian networks, maximal ancestral graphs (MAGs) are a theoretically appealing model class for dealing with unobserved variables. Despite significant advances in developing practical exact algorithms for learning score-optimal Bayesian networks, practical exact algorithms for learning score-optimal MAGs have not been developed to-date. We develop here methodology for score-based structure learning of directed maximal ancestral graphs. In particular, we develop local score computation employing a linear Gaussian BIC score, as well as score pruning techniques, which are essential for exact structure learning approaches. Furthermore, employing dynamic programming and branch and bound, we present a first exact search algorithm that is guaranteed to find a globally optimal MAG for given local scores. The experiments show that our approach is able to find considerably higher scoring MAGs than previously proposed in-exact approaches.

Details

AIJ Journal 2021 Journal Article

SAT Competition 2020

  • Nils Froleyks
  • Marijn Heule
  • Ashlin Iser
  • Matti Järvisalo
  • Martin Suda

The SAT Competitions constitute a well-established series of yearly open international algorithm implementation competitions, focusing on the Boolean satisfiability (or propositional satisfiability, SAT) problem. In this article, we provide a detailed account on the 2020 instantiation of the SAT Competition, including the new competition tracks and benchmark selection procedures, overview of solving strategies implemented in top-performing solvers, and a detailed analysis of the empirical data obtained from running the competition.

Details DOI

ECAI Conference 2020 Conference Paper

Algorithms for Dynamic Argumentation Frameworks: An Incremental SAT-Based Approach

  • Andreas Niskanen
  • Matti Järvisalo

Motivated by the fact that argumentation is intrinsically a dynamic process, the study of representational and computational aspects of dynamics in argumentation is starting to gain more traction. This is also witnessed by the most recent 2019 edition of the International Competition on Computational Models of Argumentation (ICCMA 2019), which introduced a new track focusing on dynamic argumentation frameworks. In this paper, we present an efficient Boolean satisfiability (SAT) based approach to reasoning over dynamic argumentation frameworks. In particular, based on employing incremental SAT solving, we detail algorithms covering all of the reasoning tasks—credulous and skeptical acceptance, as well as the computation of a single and all extensions—and semantics—complete, preferred, stable, and grounded—constituting the ICCMA 2019 dynamic track. Furthermore, we demonstrate empirically that an implementation of the approach is highly competitive.

Details

KR Conference 2020 Conference Paper

An Answer Set Programming Approach to Argumentative Reasoning in the ASPIC+ Framework

  • Tuomo Lehtonen
  • Johannes P. Wallner
  • Matti Järvisalo

A major research direction in AI argumentation is the study and development of practical computational techniques for reasoning in different argumentation formalisms. Compared to abstract argumentation, developing algorithmic techniques for different structured argumentation formalisms, such as assumption-based argumentation and the general ASPIC+ framework, is more challenging. At present, there is a lack of efficient approaches to reasoning in ASPIC+. We develop a direct declarative approach based on answer set programming (ASP) to reasoning in an instantiation of the ASPIC+ framework. We establish formal foundations for direct declarative encodings for reasoning in ASPIC+ without preferences for several central argumentation semantics, and detail ASP encodings of semantics for which reasoning about acceptance is NP-hard in ASPIC+. Empirically, the ASP approach scales up to frameworks of significant size, thereby answering the current lack of practical computational approaches to reasoning in ASPIC+ and providing a promising base for capturing further generalizations within ASPIC+.

PDF Details DOI

IJCAI Conference 2020 Conference Paper

Controllability of Control Argumentation Frameworks

  • Andreas Niskanen
  • Daniel Neugebauer
  • Matti Järvisalo

Control argumentation frameworks (CAFs) allow for modeling uncertainties inherent in various argumentative settings. We establish a complete computational complexity map of the central computational problem of controllability in CAFs for five key semantics. We also develop Boolean satisfiability based counterexample-guided abstraction refinement algorithms and direct encodings of controllability as quantified Boolean formulas, and empirically evaluate their scalability on a range of NP-hard variants of controllability.

PDF Details DOI

AAAI Conference 2020 Conference Paper

Deciding Acceptance in Incomplete Argumentation Frameworks

  • Andreas Niskanen
  • Daniel Neugebauer
  • Matti Järvisalo
  • Jörg Rothe

Expressing incomplete knowledge in abstract argumentation frameworks (AFs) through incomplete AFs has recently received noticeable attention. However, algorithmic aspects of deciding acceptance in incomplete AFs are still underdeveloped. We address this current shortcoming by developing algorithms for NP-hard and coNP-hard variants of acceptance problems over incomplete AFs via harnessing Boolean satisfiability (SAT) solvers. Focusing on nonempty conflict-free or admissible sets and on stable extensions, we also provide new complexity results for a refined variant of skeptical acceptance in incomplete AFs, ranging from polynomial-time computability to hardness for the second level of the polynomial hierarchy. Furthermore, central to the proposed SAT-based counterexample-guided abstraction re- finement approach for the second-level problem variants, we establish conditions for redundant atomic changes to incomplete AFs from the perspective of preserving extensions. We show empirically that the resulting SAT-based approach for incomplete AFs scales at least as well as existing SAT-based approaches to deciding acceptance in AFs.

PDF Details

LPAR Conference 2020 Conference Paper

Finding Periodic Apartments via Boolean Satisfiability and Orderly Generation

  • Jarkko Savela
  • Emilia Oikarinen
  • Matti Järvisalo

Motivated by Gromov’s subgroup conjecture (GSC), a fundamental open conjecture in the area of geometric group theory, we tackle the problem of the existence of partic- ular types of subgroups—arising from so-called periodic apartments—for a specific set of hyperbolic groups with respect to which GSC is currently open. This problem is equiv- alent to determining whether specific types of graphs with a non-trivial combination of properties exist. The existence of periodic apartments allows for ruling the groups out as some of the remaining potential counterexamples to GSC. Our approach combines both automated reasoning techniques—in particular, Boolean satisfiability (SAT) solving—with problem-specific orderly generation. Compared to earlier attempts to tackle the problem through computational means, our approach scales noticeably better, and allows for both confirming results from a previous computational treatment for smaller parameter values as well as ruling out further groups out as potential counterexamples to GSC.

Details

ECAI Conference 2020 Conference Paper

Learning Chordal Markov Networks via Stochastic Local Search

  • Kari Rantanen
  • Antti Hyttinen
  • Matti Järvisalo

We present a novel stochastic local search (SLS) approach for the computationally hard task of finding a chordal Markov network structure that maximizes a given scoring function (CMSL for short). Current state of the art in exact algorithms for CMSL only scale up to circa 20 variables. Beyond this, the scalability of exact approaches is obstructed by the drastically increasing number of clique scores which grows exponentially with the number of variables. We show that, in practice, using only a fraction of the running times of the exact approaches, our SLS approach provides optimal or very close to optimal solutions for instance sizes that are within the reach of exact algorithms. Furthermore, we propose an on-the-fly clique score computation approach that enables scaling up our SLS approach towards hundreds of variables. In particular, on-the-fly score computation circumvents the need to enforce low treewidth bounds, which enable pre-computation of scores before search, but which also may severely limit the accuracy of the learned models.

Details

ECAI Conference 2020 Conference Paper

Preprocessing in Incomplete MaxSAT Solving

  • Marcus Leivo
  • Jeremias Berg
  • Matti Järvisalo

Motivated by the success of preprocessing in Boolean satisfiability (SAT) solving, development and analysis of preprocessing in maximum satisfiability (MaxSAT)—the optimization extension of SAT—has received noticeable attention recently. The correctness of preprocessing techniques for MaxSAT is standardly established by arguing that optimal solutions are maintained. However, the effects of preprocessing on the relative perceived costs of non-optimal solutions has not been considered, despite the fact that one of the most recent directions in MaxSAT research is developing incomplete solvers, i. e. , solvers that are designed to provide good (but not necessarily optimal) solutions fast. In this paper, we bridge this gap by showing that employing central preprocessing techniques misleads MaxSAT solvers in terms of their interpretation of the costs of non-optimal solutions seen during search. This issue impacts both complete and incomplete solvers and the effects can be shown to be present also in practice with different types of MaxSAT solvers. Furthermore, we propose ideas for circumventing these negative effects in the context of stochastic local search algorithms for MaxSAT.

Details

KR Conference 2020 Conference Paper

Smallest Explanations and Diagnoses of Rejection in Abstract Argumentation

  • Andreas Niskanen
  • Matti Järvisalo

Deciding acceptance of arguments is a central problem in the realm of abstract argumentation. Beyond mere acceptance status, when an argument is rejected it would be informative to analyze reasons for the rejection. Recently, two complementary notions---explanations and diagnoses---were proposed for capturing underlying reasons for rejection in terms of (small) subsets of arguments or attacks. We provide tight complexity results for deciding and computing argument-based explanations and diagnoses. Computationally, we identify that smallest explanations and diagnoses for argumentation frameworks can be computed as so-called smallest unsatisfiable subsets (SMUSes) and smallest correction sets of propositional formulas. Empirically, we show that SMUS extractors and maximum satisfiability solvers (computing smallest correction sets) offer effective ways of computing smallest explanations and diagnoses.

PDF Details DOI

ECAI Conference 2020 Conference Paper

Strong Refinements for Hard Problems in Argumentation Dynamics

  • Andreas Niskanen
  • Matti Järvisalo

Going beyond the more classically studied reasoning problems over argumentation frameworks (AFs), the study of dynamics in argumentation gives rise to new types of computational challenges. This work studies ways of extending the scalability of computational approaches to reasoning about dynamics of abstract argumentation frameworks. In particular, we focus on three recently proposed optimization problems underlying AF dynamics—two variants of enforcement in abstract argumentation and the synthesis of argumentation frameworks from examples—for semantics under which the problems are (presumably) complete for the second level of the polynomial hierarchy. As the main contributions, we show that by bridging recent theoretical results on the persistence of extensions under changes to the structure of AFs with Boolean satisfiability (SAT) counterexample-guided abstraction refinement algorithms for the considered problems, the scalability of state-of-the-art practical algorithms for each of the three problems can be significantly improved.

Details

KR Conference 2020 System Paper

µ-toksia: An Efficient Abstract Argumentation Reasoner

  • Andreas Niskanen
  • Matti Järvisalo

We describe the µ-toksia argumentation reasoning system. The system supports a range of different reasoning tasks over both standard and dynamic abstract argumentation frameworks under essentially all central argumentation semantics, covering all tracks and reasoning tasks considered in the most recent International Competition on Computational Models of Argumentation (ICCMA 2019). µ-toksia ranked first in all reasoning tasks in the main track of ICCMA 2019, and has been shown to scale noticeably better on the dynamic track tasks than its current competitors. In this paper, we provide an overview of µ-toksia and its algorithmic and implementation-level details, and provide further empirical evidence beyond ICCMA 2019 on the efficiency of µ-toksia compared to related systems.

PDF Details DOI

IJCAI Conference 2019 Conference Paper

Enumerating Potential Maximal Cliques via SAT and ASP

  • Tuukka Korhonen
  • Jeremias Berg
  • Matti Järvisalo

The Bouchitté-Todinca algorithm (BT), operating dynamic programming over the so-called potential maximal cliques (PMCs), yields a practically efficient approach to treewidth and generalized hypertreewidth. The enumeration of PMCs is a scalability bottleneck for BT in practice. We propose the use of declarative solvers for PMC enumeration as a substitute for the specialized PMC enumeration algorithms employed in current BT implementations. The presented Boolean satisfiability (SAT) and answer set programming (ASP) based PMC enumeration approaches open up new possibilities for improving the efficiency of BT in practice.

PDF Details

JELIA Conference 2019 Conference Paper

Preprocessing Argumentation Frameworks via Replacement Patterns

  • Wolfgang Dvorák
  • Matti Järvisalo
  • Thomas Linsbichler
  • Andreas Niskanen
  • Stefan Woltran

Abstract A fast-growing research direction in the study of formal argumentation is the development of practical systems for central reasoning problems underlying argumentation. In particular, numerous systems for abstract argumentation frameworks (AF solvers) are available today, covering several argumentation semantics and reasoning tasks. Instead of proposing another algorithmic approach for AF solving, we introduce in this paper distinct AF preprocessing techniques as a solver-independent approach to obtaining performance improvements of AF solvers. We establish a formal framework of replacement patterns to perform local simplifications that are faithful with respect to standard semantics for AFs. Moreover, we provide a collection of concrete replacement patterns. Towards potential applicability, we employ the patterns in a preliminary empirical evaluation of their influence on AF solver performance.

Details

AAAI Conference 2019 Conference Paper

Reasoning over Assumption-Based Argumentation Frameworks via Direct Answer Set Programming Encodings

  • Tuomo Lehtonen
  • Johannes P. Wallner
  • Matti Järvisalo

Focusing on assumption-based argumentation (ABA) as a central structured formalism to AI argumentation, we propose a new approach to reasoning in ABA with and without preferences. While previous approaches apply either specialized algorithms or translate ABA reasoning to reasoning over abstract argumentation frameworks, we develop a direct approach by encoding ABA reasoning tasks in answer set programming. This significantly improves on the empirical performance of current ABA reasoning systems. We also give new complexity results for reasoning in ABA+, suggesting that the integration of preferential information into ABA results in increased problem complexity for several central argumentation semantics.

PDF Details

JAIR Journal 2019 Journal Article

Synthesizing Argumentation Frameworks from Examples

  • Andreas Niskanen
  • Johannes P. Wallner
  • Matti Järvisalo

Argumentation is today a topical area of artificial intelligence (AI) research. Abstract argumentation, with argumentation frameworks (AFs) as the underlying knowledge representation formalism, is a central viewpoint to argumentation in AI. Indeed, from the perspective of AI and computer science, understanding computational and representational aspects of AFs is key in the study of argumentation. Realizability of AFs has been recently proposed as a central notion for analyzing the expressive power of AFs under different semantics. In this work, we propose and study the AF synthesis problem as a natural extension of realizability, addressing some of the shortcomings arising from the relatively stringent definition of realizability. In particular, realizability gives means of establishing exact conditions on when a given collection of subsets of arguments has an AF with exactly the given collection as its set of extensions under a specific argumentation semantics. However, in various settings within the study of dynamics of argumentation---including revision and aggregation of AFs---non-realizability can naturally occur. To accommodate such settings, our notion of AF synthesis seeks to construct, or synthesize, AFs that are semantically closest to the knowledge at hand even when no AFs exactly representing the knowledge exist. Going beyond defining the AF synthesis problem, we study both theoretical and practical aspects of the problem. In particular, we (i) prove NP-completeness of AF synthesis under several semantics, (ii) study basic properties of the problem in relation to realizability, (iii) develop algorithmic solutions to NP-hard AF synthesis using the constraint optimization paradigms of maximum satisfiability and answer set programming, (iv) empirically evaluate our algorithms on different forms of AF synthesis instances, as well as (v) discuss variants and generalizations of AF synthesis.

PDF Details DOI

JELIA Conference 2019 Conference Paper

Unifying Reasoning and Core-Guided Search for Maximum Satisfiability

  • Jeremias Berg
  • Matti Järvisalo

Abstract A central algorithmic paradigm in maximum satisfiability solving geared towards real-world optimization problems is the core-guided approach. Furthermore, recent progress on preprocessing techniques is bringing in additional reasoning techniques to MaxSAT solving. Towards realizing their combined potential, understanding formal underpinnings of interleavings of preprocessing-style reasoning and core-guided algorithms is important. It turns out that earlier proposed notions for establishing correctness of core-guided algorithms and preprocessing, respectively, are not enough for capturing correctness of interleavings of the techniques. We provide an in-depth analysis of these and related MaxSAT instance transformations, and propose correction set reducibility as a notion that captures inprocessing MaxSAT solving within a state-transition style abstract MaxSAT solving framework. Furthermore, we establish a general theorem of correctness for applications of SAT-based preprocessing techniques in MaxSAT. The results pave way for generic techniques for arguing about the formal correctness of MaxSAT algorithms.

Details

KR Conference 2018 Conference Paper

A Hybrid Approach to Optimization in Answer Set Programming

  • Paul Saikko
  • Carmine Dodaro
  • Mario Alviano
  • Matti Järvisalo

Answer set programming (ASP) is today a successful approach to knowledge representation and reasoning in various real-world problem domains. ASP offers an expressive rule-based constraint modelling language, supporting concise declarative modelling of both decision and optimization problems within the first or the second level of the polynomial hierarchy. In this paper, we propose a new approach to solving optimization problems via ASP, i. e. , to the problem of finding optimal solutions (in terms of optimal answer sets or stable models) under a given weight function over soft atoms (weak constraints). Our approach constitutes the first adaptation of the so-called implicit hitting set approach in the context of ASP. In particular, in contrast to the earlier proposed family of core-guided algorithms for optimization in answer set programming, we present a hybrid approach which makes use of interactions between an ASP decision solver (as an unsatisfiable core extractor) and an integer programming solver (as a minimum-cost hitting set algorithm). We explain how various concepts and features specific to ASP and IP can be harnessed within the approach, including several ways for obtaining better upper and lower bounds during search, with the aim of speeding up the computation of an optimal answer set. By a careful integration of the interactions between state-of-the-art ASP and IP solvers, we show that already our first implementation provides a complementary approach when empirically compared to the currently available solvers supporting optimization in answer set programming.

KR Conference 2018 Conference Paper

Extension Enforcement under Grounded Semantics in Abstract Argumentation

  • Andreas Niskanen
  • Johannes P. Wallner
  • Matti Järvisalo

The study of dynamics in abstract argumentation gives rise to optimization problems that are NP-hard also under the grounded semantics, in contrast to argument acceptance problems over argumentation frameworks (AF). Developing efficient systems for AF reasoning under grounded semantics has received less attention compared to other central AF semantics under which acceptance is NP-hard. In particular, grounded semantics is not currently supported by recent systems for extension enforcement, despite (or due to) its nontriviality. In this work, we propose and empirically evaluate three first approaches to enforcement under grounded semantics. While each of the approaches is based on employing constraint optimization solvers, we show empirically that there are significant differences in the scalability of the approaches.

AAAI Conference 2018 Conference Paper

Premise Set Caching for Enumerating Minimal Correction Subsets

  • Alessandro Previti
  • Carlos Mencía
  • Matti Järvisalo
  • Joao Marques-Silva

Methods for explaining the sources of inconsistency of overconstrained systems find an ever-increasing number of applications, ranging from diagnosis and configuration to ontology debugging and axiom pinpointing in description logics. Ef- ficient enumeration of minimal correction subsets (MCSes), defined as sets of constraints whose removal from the system restores feasibility, is a central task in such domains. In this work, we propose a novel approach to speeding up MCS enumeration over conjunctive normal form propositional formulas by caching of so-called premise sets (PSes) seen during the enumeration process. Contrasting to earlier work, we move from caching unsatisfiable cores to caching PSes and propose a more effective way of implementing the cache. The proposed techniques noticeably improves on the performance of state-of-the-art MCS enumeration algorithms in practice.

PDF Details

IJCAI Conference 2018 Conference Paper

Reduced Cost Fixing for Maximum Satisfiability

  • Fahiem Bacchus
  • Antti Hyttinen
  • Matti Järvisalo
  • Paul Saikko

Maximum satisfiability (MaxSAT) offers a competitive approach to solving NP-hard real-world optimization problems. While state-of-the-art MaxSAT solvers rely heavily on Boolean satisfiability (SAT) solvers, a recent trend, brought on by MaxSAT solvers implementing the so-called implicit hitting set (IHS) approach, is to integrate techniques from the realm of integer programming (IP) into the solving process. This allows for making use of additional IP solving techniques to further speed up MaxSAT solving. In this line of work, we investigate the integration of the technique of reduced cost fixing from the IP realm into IHS solvers, and empirically show that reduced cost fixing considerable speeds up a state-of-the-art MaxSAT solver implementing the IHS approach.

PDF Details

IJCAI Conference 2017 Conference Paper

A Core-Guided Approach to Learning Optimal Causal Graphs

  • Antti Hyttinen
  • Paul Saikko
  • Matti Järvisalo

Discovery of causal relations is an important part of data analysis. Recent exact Boolean optimization approaches enable tackling very general search spaces of causal graphs with feedback cycles and latent confounders, simultaneously obtaining high accuracy by optimally combining conflicting independence information in sample data. We propose several domain-specific techniques and integrate them into a core-guided maximum satisfiability solver, thereby speeding up current state of the art in exact search for causal graphs with cycles and latent confounders on simulated and real-world data.

PDF Details

JAIR Journal 2017 Journal Article

Bayesian Network Structure Learning with Integer Programming: Polytopes, Facets and Complexity

  • James Cussens
  • Matti Järvisalo
  • Janne H. Korhonen
  • Mark Bartlett

The challenging task of learning structures of probabilistic graphical models is an important problem within modern AI research. Recent years have witnessed several major algorithmic advances in structure learning for Bayesian networks - arguably the most central class of graphical models - especially in what is known as the score-based setting. A successful generic approach to optimal Bayesian network structure learning (BNSL), based on integer programming (IP), is implemented in the GOBNILP system. Despite the recent algorithmic advances, current understanding of foundational aspects underlying the IP based approach to BNSL is still somewhat lacking. Understanding fundamental aspects of cutting planes and the related separation problem is important not only from a purely theoretical perspective, but also since it holds out the promise of further improving the efficiency of state-of-the-art approaches to solving BNSL exactly. In this paper, we make several theoretical contributions towards these goals: (i) we study the computational complexity of the separation problem, proving that the problem is NP-hard; (ii) we formalise and analyse the relationship between three key polytopes underlying the IP-based approach to BNSL; (iii) we study the facets of the three polytopes both from the theoretical and practical perspective, providing, via exhaustive computation, a complete enumeration of facets for low-dimensional family-variable polytopes; and, furthermore, (iv) we establish a tight connection of the BNSL problem to the acyclic subgraph problem.

PDF Details DOI

IJCAI Conference 2017 Conference Paper

Bayesian Network Structure Learning with Integer Programming: Polytopes, Facets and Complexity (Extended Abstract)

  • James Cussens
  • Matti Järvisalo
  • Janne H. Korhonen
  • Mark Bartlett

Developing accurate algorithms for learning structures of probabilistic graphical models is an important problem within modern AI research. Here we focus on score-based structure learning for Bayesian networks as arguably the most central class of graphical models. A successful generic approach to optimal Bayesian network structure learning (BNSL), based on integer programming (IP), is implemented in the Gobnilp system. Despite the recent algorithmic advances, current understanding of foundational aspects underlying the IP based approach to BNSL is still somewhat lacking. In this paper, we provide theoretical contributions towards understanding fundamental aspects of cutting planes and the related separation problem in this context, ranging from NP-hardness results to analysis of polytopes and the related facets in connection to BNSL.

PDF Details

JAIR Journal 2017 Journal Article

Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation

  • Johannes P. Wallner
  • Andreas Niskanen
  • Matti Järvisalo

Argumentation is an active area of modern artificial intelligence (AI) research, with connections to a range of fields, from computational complexity theory and knowledge representation and reasoning to philosophy and social sciences, as well as application-oriented work in domains such as legal reasoning, multi-agent systems, and decision support. Argumentation frameworks (AFs) of abstract argumentation have become the graph-based formal model of choice for many approaches to argumentation in AI, with semantics defining sets of jointly acceptable arguments, i.e., extensions. Understanding the dynamics of AFs has been recently recognized as an important topic in the study of argumentation in AI. In this work, we focus on the so-called extension enforcement problem in abstract argumentation as a recently proposed form of argumentation dynamics. We provide a nearly complete computational complexity map of argument-fixed extension enforcement under various major AF semantics, with results ranging from polynomial-time algorithms to completeness for the second level of the polynomial hierarchy. Complementing the complexity results, we propose algorithms for NP-hard extension enforcement based on constraint optimization under the maximum satisfiability (MaxSAT) paradigm. Going beyond NP, we propose novel MaxSAT-based counterexample-guided abstraction refinement procedures for the second-level complete problems and present empirical results on a prototype system constituting the first approach to extension enforcement in its generality.

PDF Details DOI

AIJ Journal 2017 Journal Article

Cost-optimal constrained correlation clustering via weighted partial Maximum Satisfiability

  • Jeremias Berg
  • Matti Järvisalo

Integration of the fields of constraint solving and data mining and machine learning has recently been identified within the AI community as an important research direction with high potential. This work contributes to this direction by providing a first study on the applicability of state-of-the-art Boolean optimization procedures to cost-optimal correlation clustering under constraints in a general similarity-based setting. We develop exact formulations of the correlation clustering task as Maximum Satisfiability (MaxSAT), the optimization version of the Boolean satisfiability (SAT) problem. For obtaining cost-optimal clusterings, we apply a state-of-the-art MaxSAT solver for solving the resulting MaxSAT instances optimally, resulting in cost-optimal clusterings. We experimentally evaluate the MaxSAT-based approaches to cost-optimal correlation clustering, both on the scalability of our method and the quality of the clusterings obtained. Furthermore, we show how the approach extends to constrained correlation clustering, where additional user knowledge is imposed as constraints on the optimal clusterings of interest. We show experimentally that added user knowledge allows clustering larger datasets, and at the same time tends to decrease the running time of our approach. We also investigate the effects of MaxSAT-level preprocessing, symmetry breaking, and the choice of the MaxSAT solver on the efficiency of the approach.

Details DOI

SAT Conference 2017 Conference Paper

Improving MCS Enumeration via Caching

  • Alessandro Previti
  • Carlos Mencía
  • Matti Järvisalo
  • João Marques-Silva 0001

Abstract Enumeration of minimal correction sets (MCSes) of conjunctive normal form formulas is a central and highly intractable problem in infeasibility analysis of constraint systems. Often complete enumeration of MCSes is impossible due to both high computational cost and worst-case exponential number of MCSes. In such cases partial enumeration is sought for, finding applications in various domains, including axiom pinpointing in description logics among others. In this work we propose caching as a means of further improving the practical efficiency of current MCS enumeration approaches, and show the potential of caching via an empirical evaluation.

Details

NeurIPS Conference 2017 Conference Paper

Learning Chordal Markov Networks via Branch and Bound

  • Kari Rantanen
  • Antti Hyttinen
  • Matti Järvisalo

We present a new algorithmic approach for the task of finding a chordal Markov network structure that maximizes a given scoring function. The algorithm is based on branch and bound and integrates dynamic programming for both domain pruning and for obtaining strong bounds for search-space pruning. Empirically, we show that the approach dominates in terms of running times a recent integer programming approach (and thereby also a recent constraint optimization approach) for the problem. Furthermore, our algorithm scales at times further with respect to the number of variables than a state-of-the-art dynamic programming algorithm for the problem, with the potential of reaching 20 variables and at the same time circumventing the tight exponential lower bounds on memory consumption of the pure dynamic programming approach.

PDF Details

SAT Conference 2017 Conference Paper

MaxPre: An Extended MaxSAT Preprocessor

  • Tuukka Korhonen
  • Jeremias Berg
  • Paul Saikko
  • Matti Järvisalo

Abstract We describe MaxPre, an open-source preprocessor for (weighted partial) maximum satisfiability (MaxSAT). MaxPre implements both SAT-based and MaxSAT-specific preprocessing techniques, and offers solution reconstruction, cardinality constraint encoding, and an API for tight integration into SAT-based MaxSAT solvers.

Details

AAAI Conference 2016 Conference Paper

Complexity Results and Algorithms for Extension Enforcement in Abstract Argumentation

  • Johannes Wallner
  • Andreas Niskanen
  • Matti Järvisalo

Understanding the dynamics of argumentation frameworks (AFs) is important in the study of argumentation in AI. In this work, we focus on the so-called extension enforcement problem in abstract argumentation. We provide a nearly complete computational complexity map of fixed-argument extension enforcement under various major AF semantics, with results ranging from polynomial-time algorithms to completeness for the second-level of the polynomial hierarchy. Complementing the complexity results, we propose algorithms for NP-hard extension enforcement based on constrained optimization. Going beyond NP, we propose novel counterexample-guided abstraction refinement procedures for the second-level complete problems and present empirical results on a prototype system constituting the first approach to extension enforcement in its generality.

PDF Details

KR Conference 2016 Conference Paper

Implicit Hitting Set Algorithms for Reasoning Beyond NP

  • Paul Saikko
  • Johannes Peter Wallner
  • Matti Järvisalo

Lifting a recent proposal by Moreno-Centeno and Karp, we propose a general framework for so-called implicit hitting set algorithms for reasoning beyond NP. The framework is motivated by empirically successful specific instantiations of the approach—based on interactions between a Boolean satisfiability (SAT) solver and an integer programming (IP) solver—in the context of maximum satisfiability (MaxSAT). The framework opens up opportunities for developing implicit hitting set algorithms for various important reasoning problems in KR by implementing domain-specific reasoning modules with SAT and IP solvers. We detail instantiations of the framework for the minimum satisfiability problem— as a natural dual of MaxSAT—and, as a central KR problem, for propositional abduction, covering the second level of the polynomial hierarchy. We show empirically that an implementation of the instantiation for propositional abduction surpasses the efficiency of an approach based on encoding and solving propositional abduction instances as disjunctive logic programming under answer set semantics. We also study key properties of the general framework. 1 Motivated by this success, in this work we outline a general framework for implicit hitting set algorithms. Specifically (but by no means restricted to), the framework is developed with instantiations based on SAT and IP solvers in mind; the SAT solver acts (or, going beyond NP, multiple SAT solvers act) the role of a “core extractor” used for extracting non-solutions, and the IP solver acts as a hitting set optimizer, used for ruling out the thus far found nonsolutions from further consideration. The framework thus provides novel algorithms for a variety of hard reasoning tasks via modularly instantiating the core extraction and hitting set modules in domain-specific ways via SAT and IP solvers specifically well-suited for the respective tasks of providing proofs of unsatisfiability and optimization. We detail novel instantiations of the general framework, using as a running example minimum satisfiability, the dual of MaxSAT that has recently received increasing attention, and, most interestingly, going beyond NP, for the problem of propositional abduction that is hard for the second-level of the polynomial hierarchy. To illustrate the practical potential of the framework, we present results from an empirical evaluation of a prototype implementation of the instantiation for abduction. We show empirically that the implementation for propositional abduction surpasses the efficiency of an approach based on encoding and solving propositional abduction instances as disjunctive logic programming under answer set semantics (Brewka, Eiter, and Truszczyński 2011). Furthermore, from a more theoretical perspective, we discuss fundamental properties and correctness of the general

SAT Conference 2016 Conference Paper

LMHS: A SAT-IP Hybrid MaxSAT Solver

  • Paul Saikko
  • Jeremias Berg
  • Matti Järvisalo

Abstract We describe LMHS, an open-source weighted partial maximum satisfiability (MaxSAT) solver. LMHS is a hybrid SAT-IP MaxSAT solver that implements the implicit hitting set approach to MaxSAT. On top of the main algorithm, LMHS offers integrated preprocessing, solution enumeration, an incremental API, and the use of a choice of SAT and IP solvers. We describe the main features of LMHS, and give empirical results on the influence of preprocessing and the choice of the underlying SAT and IP solvers on the performance of LMHS.

Details

JELIA Conference 2016 Conference Paper

Pakota: A System for Enforcement in Abstract Argumentation

  • Andreas Niskanen
  • Johannes P. Wallner
  • Matti Järvisalo

Abstract In this paper we describe Pakota, a system implementation that allows for solving enforcement problems over argumentation frameworks. Via harnessing Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT) solvers, Pakota implements algorithms for extension and status enforcement under various central AF semantics, covering a range of NP-complete—via direct MaxSAT encodings—and \(\mathrm{\Sigma }_{2}^{P}\) -complete—via MaxSAT-based counterexample-guided abstraction refinement—enforcement problems. We overview the algorithmic approaches implemented in Pakota, and describe in detail the system architecture, features, interfaces, and usage of the system. Furthermore, we present an empirical evaluation on the impact of the choice of MaxSAT solvers on the scalability of the system, and also provide benchmark generators for extension and status enforcement.

Details

ECAI Conference 2016 Conference Paper

Subsumed Label Elimination for Maximum Satisfiability

  • Jeremias Berg
  • Paul Saikko
  • Matti Järvisalo

We propose subsumed label elimination (SLE), a socalled label-based preprocessing technique for the Boolean optimization paradigm of maximum satisfiability (MaxSAT). We formally show that SLE is orthogonal to previously proposed SAT-based preprocessing techniques for MaxSAT in that it can simplify the underlying minimal unsatisfiable core structure of MaxSAT instances. We also formally show that SLE can considerably reduce the number of internal SAT solver calls within modern core-guided MaxSAT solvers. Empirically, we show that combining SLE with SAT-based preprocessing improves the performance of various state-of-the-art MaxSAT solvers on standard industrial weighted partial MaxSAT benchmarks.

Details

ECAI Conference 2016 Conference Paper

Synthesizing Argumentation Frameworks from Examples

  • Andreas Niskanen
  • Johannes P. Wallner
  • Matti Järvisalo

Argumentation is nowadays a core topic in AI research. Understanding computational and representational aspects of abstract argumentation frameworks (AFs) is a central topic in the study of argumentation. The study of realizability of AFs aims at understanding the expressive power of AFs under different semantics. We propose and study the AF synthesis problem as a natural extension of realizability, addressing some of the shortcomings arising from the relatively stringent definition of realizability. Specifically, AF synthesis seeks to construct, or synthesize, AFs that are semantically closest to the knowledge at hand even when no AFs exactly representing the knowledge exist. Going beyond defining the AF synthesis problem, we (i) prove NP-completeness of AF synthesis under several semantics, (ii) study basic properties of the problem in relation to realizability, (iii) develop algorithmic solutions to AF synthesis using constrained optimization, (iv) empirically evaluate our algorithms on different forms of AF synthesis instances, as well as (v) discuss variants and generalization of AF synthesis.

Details

JAIR Journal 2015 Journal Article

Clause Elimination for SAT and QSAT

  • Marijn Heule
  • Matti Järvisalo
  • Florian Lonsing
  • Martina Seidl
  • Armin Biere

The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of various computationally hard problems can be efficiently solved. This success has been achieved through several breakthroughs in practical implementations of decision procedures for SAT and QSAT, that is, in SAT and QSAT solvers. Here, simplification techniques for conjunctive normal form (CNF) for SAT and for prenex conjunctive normal form (PCNF) for QSAT---the standard input formats of SAT and QSAT solvers---have recently proven very effective in increasing solver efficiency when applied before (i.e., in preprocessing) or during (i.e., in inprocessing) satisfiability search. In this article, we develop and analyze clause elimination procedures for pre- and inprocessing. Clause elimination procedures form a family of (P)CNF formula simplification techniques which remove clauses that have specific (in practice polynomial-time) redundancy properties while maintaining the satisfiability status of the formulas. Extending known procedures such as tautology, subsumption, and blocked clause elimination, we introduce novel elimination procedures based on asymmetric variants of these techniques, and also develop a novel family of so-called covered clause elimination procedures, as well as natural liftings of the CNF-level procedures to PCNF. We analyze the considered clause elimination procedures from various perspectives. Furthermore, for the variants not preserving logical equivalence under clause elimination, we show how to reconstruct solutions to original CNFs from satisfying assignments to simplified CNFs, which is important for practical applications for the procedures. Complementing the more theoretical analysis, we present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It turns out that the importance of applying the clause elimination procedures developed in this work is empirically emphasized in the context of state-of-the-art QSAT solving.

PDF Details DOI

UAI Conference 2015 Conference Paper

Do-calculus when the True Graph Is Unknown

  • Antti Hyttinen
  • Frederick Eberhardt
  • Matti Järvisalo

One of the basic tasks of causal discovery is to estimate the causal effect of some set of variables on another given a statistical data set. In this article we bridge the gap between causal structure discovery and the do-calculus by proposing a method for the identification of causal effects on the basis of arbitrary (equivalence) classes of semi-Markovian causal models. The approach uses a general logical representation of the equivalence class of graphs obtained from a causal structure discovery algorithm, the properties of which can then be queried by procedures implementing the do-calculus inference for causal effects. We show that the method is more efficient than determining causal effects using a naive enumeration of graphs in the equivalence class. Moreover, the method is complete with respect to the identifiability of causal effects for settings, in which extant methods that do not require knowledge of the true graph, offer only incomplete results. The method is entirely modular and easily adapted for different background settings.

Details

UAI Conference 2015 Conference Paper

Impact of Learning Strategies on the Quality of Bayesian Networks: An Empirical Evaluation

  • Brandon M. Malone
  • Matti Järvisalo
  • Petri Myllymäki

We present results from an empirical evaluation of the impact of Bayesian network structure learning strategies on the learned structures. In particular, we investigate how learning algorithms with different optimality guarantees compare in terms of structural aspects and generalisability of the produced network structures. For example, in terms of generalization to unseen testing data, we show that local search algorithms often benefit from a tight constraint on the number of parents of variables in the networks, while exact approaches tend to benefit from looser parent restrictions. Overall, we find that learning strategies with weak optimality guarantees show good performance on synthetic datasets, but, compared to exact approaches, perform poorly on the more “real-world” datasets. The exact approaches, which guarantee to find globally optimal solutions, consistently generalize well to unseen testing data, motivating further work on increasing the robustness and scalability of such algorithmic approaches to Bayesian network structure learning.

Details

UAI Conference 2015 Conference Paper

Learning Optimal Chain Graphs with Answer Set Programming

  • Dag Sonntag
  • Matti Järvisalo
  • Jose M. Peña 0001
  • Antti Hyttinen

Learning an optimal chain graph from data is an important hard computational problem. We present a new approach to solve this problem for various objective functions without making any assumption on the probability distribution at hand. Our approach is based on encoding the learning problem declaratively using the answer set programming (ASP) paradigm. Empirical results show that our approach provides at least as accurate solutions as the best solutions provided by the existing algorithms, and overall provides better accuracy than any single previous algorithm.

Details

AIJ Journal 2015 Journal Article

Overview and analysis of the SAT Challenge 2012 solver competition

  • Adrian Balint
  • Anton Belov
  • Matti Järvisalo
  • Carsten Sinz

Programs for the Boolean satisfiability problem (SAT), i. e. , SAT solvers, are nowadays used as core decision procedures for a wide range of combinatorial problems. Advances in SAT solving during the last 10–15 years have been spurred by yearly solver competitions. In this article, we report on the main SAT solver competition held in 2012, SAT Challenge 2012. Besides providing an overview of how SAT Challenge 2012 was organized, we present an in-depth analysis of key aspects of the results obtained during the competition.

Details DOI

JELIA Conference 2014 Conference Paper

Answer Set Solver Backdoors

  • Emilia Oikarinen
  • Matti Järvisalo

Abstract Backdoor variables offer a generic notion for providing insights to the surprising success of constraint satisfaction solvers in solving remarkably complex real-world instances of combinatorial problems. We study backdoors in the context of answer set programming (ASP), and focus on studying the relative size of backdoors in terms of different state-of-the-art answer set solving algorithms. We show separations of ASP solver families in terms of the smallest existing backdoor sets for the solvers.

Details

AIJ Journal 2014 Journal Article

Complexity-sensitive decision procedures for abstract argumentation

  • Wolfgang Dvořák
  • Matti Järvisalo
  • Johannes Peter Wallner
  • Stefan Woltran

argumentation frameworks (AFs) provide the basis for various reasoning problems in the area of Artificial Intelligence. Efficient evaluation of AFs has thus been identified as an important research challenge. So far, implemented systems for evaluating AFs have either followed a straight-forward reduction-based approach or been limited to certain tractable classes of AFs. In this work, we present a generic approach for reasoning over AFs, based on the novel concept of complexity-sensitivity. Establishing the theoretical foundations of this approach, we derive several new complexity results for preferred, semi-stable and stage semantics which complement the current complexity landscape for abstract argumentation, providing further understanding on the sources of intractability of AF reasoning problems. The introduced generic framework exploits decision procedures for problems of lower complexity whenever possible. This allows, in particular, instantiations of the generic framework via harnessing in an iterative way current sophisticated Boolean satisfiability (SAT) solver technology for solving the considered AF reasoning problems. First experimental results show that the SAT-based instantiation of our novel approach outperforms existing systems.

Details DOI

SAT Conference 2014 Conference Paper

Conditional Lower Bounds for Failed Literals and Related Techniques

  • Matti Järvisalo
  • Janne H. Korhonen

Abstract We prove time-complexity lower bounds for various practically relevant probing-based CNF simplification techniques, namely failed literal detection and related techniques. Specifically, we show that improved algorithms for these simplification techniques would give a 2 δn time algorithm for CNF-SAT for some δ < 1, violating the Strong Exponential Time Hypothesis.

Details

UAI Conference 2014 Conference Paper

Constraint-based Causal Discovery: Conflict Resolution with Answer Set Programming

  • Antti Hyttinen
  • Frederick Eberhardt
  • Matti Järvisalo

Recent approaches to causal discovery based on Boolean satisfiability solvers have opened new opportunities to consider search spaces for causal models with both feedback cycles and unmeasured confounders. However, the available methods have so far not been able to provide a principled account of how to handle conflicting constraints that arise from statistical variability. Here we present a new approach that preserves the versatility of Boolean constraint solving and attains a high accuracy despite the presence of statistical errors. We develop a new logical encoding of (in)dependence constraints that is both well suited for the domain and allows for faster solving. We represent this encoding in Answer Set Programming (ASP), and apply a state-of-theart ASP solver for the optimization task. Based on different theoretical motivations, we explore a variety of methods to handle statistical errors. Our approach currently scales to cyclic latent variable models with up to seven observed variables and outperforms the available constraintbased methods in accuracy.

Details

AAAI Conference 2014 Conference Paper

Optimal Neighborhood Preserving Visualization by Maximum Satisfiability

  • Kerstin Bunte
  • Matti Järvisalo
  • Jeremias Berg
  • Petri Myllymäki
  • Jaakko Peltonen
  • Samuel Kaski

We present a novel approach to low-dimensional neighbor embedding for visualization, based on formulating an information retrieval based neighborhood preservation cost function as Maximum satisfiability on a discretized output display. The method has a rigorous interpretation as optimal visualization based on the cost function. Unlike previous lowdimensional neighbor embedding methods, our formulation is guaranteed to yield globally optimal visualizations, and does so reasonably fast. Unlike previous manifold learning methods yielding global optima of their cost functions, our cost function and method are designed for low-dimensional visualization where evaluation and minimization of visualization errors are crucial. Our method performs well in experiments, yielding clean embeddings of datasets where a stateof-the-art comparison method yields poor arrangements. In a real-world case study for semi-supervised WLAN signal mapping in buildings we outperform state-of-the-art methods.

PDF Details

UAI Conference 2013 Conference Paper

Discovering Cyclic Causal Models with Latent Variables: A General SAT-Based Procedure

  • Antti Hyttinen
  • Patrik O. Hoyer
  • Frederick Eberhardt
  • Matti Järvisalo

We present a very general approach to learning the structure of causal models based on d-separation constraints, obtained from any given set of overlapping passive observational or experimental data sets. The procedure allows for both directed cycles (feedback loops) and the presence of latent variables. Our approach is based on a logical representation of causal pathways, which permits the integration of quite general background knowledge, and inference is performed using a Boolean satisfiability (SAT) solver. The procedure is complete in that it exhausts the available information on whether any given edge can be determined to be present or absent, and returns “unknown” otherwise. Many existing constraint-based causal discovery algorithms can be seen as special cases, tailored to circumstances in which one or more restricting assumptions apply. Simulations illustrate the effect of these assumptions on discovery and how the present algorithm scales.

Details

KR Conference 2012 Conference Paper

Complexity-Sensitive Decision Procedures for Abstract Argumentation

  • Wolfgang Dvorak
  • Matti Järvisalo
  • Johannes Peter Wallner
  • Stefan Woltran

of this paper is both on the identification of such lowercomplexity fragments of second-level reasoning problems arising from abstract argumentation, and on exploiting this knowledge in developing efficient complexity-sensitive decision procedures for the generic second-level problems. Tractable (i. e., polynomial-time decidable) fragments have been quite thoroughly studied in the literature (see, e. g., (Coste-Marquis, Devred, and Marquis 2005; Dunne 2007; Dvořák, Szeider, and Woltran 2010; Dvořák, Pichler, and Woltran 2011; Ordyniak and Szeider 2011)). However, there is only little work on the identification of fragments which are located on the first level (NP-coNP layer), that is, inbetween tractability and full second-level complexity. Identification of first-level fragments of second-level reasoning tasks is important due to several reasons. First, from a theoretical point of view, such fragments show particular (but not all) sources of complexity of the considered problems and pave the way towards “trichotomy”-like results (e. g. (Truszczynski 2011) in the context of answer-set programming). Second, NP fragments can be efficiently reduced to the problem of satisfiability in classical propositional logic (SAT). This allows for realizations of argumentation procedures by employing highly sophisticated SAT solver technology in reasoning on argumentation problems. Going even further, we aim at designing decision procedures for larger fragments based on decision procedures developed for an NP-fragment, using the NP decision procedures as an NP oracle in an iterative fashion. Such procedures fall under the general counter-example guided abstraction refinement (CEGAR) approach originating from the field of model checking (Clarke et al. 2003; Clarke, Gupta, and Strichman 2004). For problems complete for the second level of the polynomial hierarchy, this leads to a general procedure which, in the worst case, requires an exponential number of calls to the NP oracle, which is indeed unavoidable under the assumption that the polynomial hierarchy does not collapse. Nevertheless, such procedures can be designed to behave adequately on input instances that fall into the considered NP fragment and on instances for which a relatively low number of oracle calls is sufficient. As a generic notion, we say that such a procedure is complexity-sensitive w. r. t. the NP fragment at hand. For instance, for the second level problem of answer-set existence for disjunctive logic programs, the successful loop-formula Abstract argumentation frameworks (AFs) provide the basis for various reasoning problems in the areas of Knowledge Representation and Artificial Intelligence. Efficient evaluation of AFs has thus been identified as an important research challenge. So far, implemented systems for evaluating AFs have either followed a straight-forward reduction-based approach or been limited to certain tractable classes of AFs. In this work, we present a generic approach for reasoning over AFs, based on the novel concept of complexity-sensitivity. Establishing the theoretical foundations of this approach, we derive several new complexity results for preferred, semistable and stage semantics which complement the current complexity landscape for abstract argumentation, providing further understanding on the sources of intractability of AF reasoning problems. The introduced generic framework exploits decision procedures for problems of lower complexity whenever possible. This allows, in particular, instantiations of the generic framework via harnessing in an iterative way current sophisticated Boolean satisfiability (SAT) solver technology for solving the considered AF reasoning problems. First experimental results show that the SAT-based instantiation of our novel approach outperforms existing systems.

SAT Conference 2012 Conference Paper

Finding Efficient Circuits for Ensemble Computation

  • Matti Järvisalo
  • Petteri Kaski
  • Mikko Koivisto
  • Janne H. Korhonen

Abstract Given a Boolean function as input, a fundamental problem is to find a Boolean circuit with the least number of elementary gates (AND, OR, NOT) that computes the function. The problem generalises naturally to the setting of multiple Boolean functions: find the smallest Boolean circuit that computes all the functions simultaneously. We study an NP-complete variant of this problem titled Ensemble Computation and, especially, its relationship to the Boolean satisfiability (SAT) problem from both the theoretical and practical perspectives, under the two monotone circuit classes: OR-circuits and SUM-circuits. Our main result relates the existence of nontrivial algorithms for CNF-SAT with the problem of rewriting in subquadratic time a given OR-circuit to a SUM-circuit. Furthermore, by developing a SAT encoding for the ensemble computation problem and by employing state-of-the-art SAT solvers, we search for concrete instances that would witness a substantial separation between the size of optimal OR-circuits and optimal SUM-circuits. Our encoding allows for exhaustively checking all small witness candidates. Searching over larger witness candidates presents an interesting challenge for current SAT solver technology.

Details

SAT Conference 2011 Conference Paper

Efficient CNF Simplification Based on Binary Implication Graphs

  • Marijn J. H. Heule
  • Matti Järvisalo
  • Armin Biere

Abstract This paper develops techniques for efficiently detecting redundancies in CNF formulas. We introduce the concept of hidden literals, resulting in the novel technique of hidden literal elimination. We develop a practical simplification algorithm that enables “ Unhiding ” various redundancies in a unified framework. Based on time stamping literals in the binary implication graph, the algorithm applies various binary clause based simplifications, including techniques that, when run repeatedly until fixpoint, can be too costly. Unhiding can also be applied during search, taking learnt clauses into account. We show that Unhiding gives performance improvements on real-world SAT competition benchmarks.

Details

SAT Conference 2010 Conference Paper

Reconstructing Solutions after Blocked Clause Elimination

  • Matti Järvisalo
  • Armin Biere

Abstract Preprocessing has proven important in enabling efficient Boolean satisfiability (SAT) solving. For many real application scenarios of SAT it is important to be able to extract a full satisfying assignment for original SAT instances from a satisfying assignment for the instances after preprocessing. We show how such full solutions can be efficiently reconstructed from solutions to the conjunctive normal form (CNF) formulas resulting from applying a combination of various CNF preprocessing techniques implemented in the PrecoSAT solver—especially, blocked clause elimination combined with SatElite-style variable elimination and equivalence reasoning.

Details

LPAR Conference 2008 Conference Paper

Justification-Based Local Search with Adaptive Noise Strategies

  • Matti Järvisalo
  • Tommi A. Junttila
  • Ilkka Niemelä

Abstract We study a framework called BC SLS for a novel type of stochastic local search (SLS) for propositional satisfiability (SAT). Aimed specifically at solving real-world SAT instances, the approach works directly on a non-clausal structural representation for SAT. This allows for don’t care detection and justification guided search heuristics in SLS by applying the circuit-level SAT technique of justification frontiers. In this paper we extend the BC SLS approach first by developing generalizations of BC SLS which are probabilistically approximately complete (PAC). Second, we develop and study adaptive noise mechanisms for BC SLS, including mechanisms based on dynamically adapting the waiting period for noise increases. Experiments show that a preliminary implementation of the novel adaptive, PAC generalization of the method outperforms a well-known CNF level SLS method with adaptive noise (AdaptNovelty+) on a collection of structured real-world SAT instances.

Details

ECAI Conference 2008 Conference Paper

Justification-Based Non-Clausal Local Search for SAT

  • Matti Järvisalo
  • Tommi A. Junttila
  • Ilkka Niemelä

While stochastic local search (SLS) techniques are very efficient in solving hard randomly generated propositional satisfiability (SAT) problem instances, a major challenge is to improve SLS on structured problems. Motivated by heuristics applied in complete circuit-level SAT solvers in electronic design automation, we develop novel SLS techniques by harnessing the concept of justification frontiers. This leads to SLS heuristics which concentrate the search into relevant parts of instances, exploit observability don't cares and allow for an early stopping criterion. Experiments with a prototype implementation of the framework presented in this paper show up to a four orders of magnitude decrease in the number of moves on real-world bounded model checking instances when compared to WalkSAT on the standard CNF encodings of the instances.

Details

AAAI Conference 2008 Conference Paper

On the Power of Top-Down Branching Heuristics

  • Matti Järvisalo

We study the relative best-case performance of DPLL-based structure-aware SAT solvers in terms of the power of the underlying proof systems. The systems result from (i) varying the style of branching and (ii) enforcing dynamic restrictions on the decision heuristics. Considering DPLL both with and without clause learning, we present a relative efficiency hierarchy for refinements of DPLL resulting from combinations of decision heuristics (top-down restricted, justification restricted, and unrestricted heuristics) and branching styles (typical DPLL-style and ATPG-style branching). An an example, for DPLL without clause learning, we establish a strict hierarchy, with the ATPG-style, justification restricted branching variant as the weakest system.

PDF Details

AAAI Conference 2006 Short Paper

Further Investigations into Regular XORSAT

  • Matti Järvisalo

Recent years have witnessed rapid progress both in the foun- dations of and in applying state-of-art solvers for the propo- sitional satisfiability problem (SAT). The study of sources for hard SAT instances is motivated by the need for inter- esting benchmarks for solver development and on the other hand by theoretical analysis of different proof systems. In this respect satisfiable instance families are espe- cially interesting. In contrast to unsatis iable instance families, there are few theoretical results for satisfiable formulas; for the successful DPLL method, restricted heuristics need to be considered. While real-world problems serve as best benchmark in- stances in many sense, such instances are typically very large and unavailable in abundance. More artificial empirically hard satisfiable CNF families include regular random k-SAT, encodings of quasi-group completion, XORSAT models inspired by statistical physics, and the regular XORSAT model motivated by expansion properties of random regular bipartite graphs. Experimental comparison with other available generators for notably hard satisfiable 3-CNF formulas shows that the regular XORSAT model gives extremely hard instances for state-of-the art clausal SAT solvers. In this paper we generalize the regular XORSAT model for k > 3, and investigate how this relates to the hardness of the instances. By increasing the degree of the underlying regular constraint graphs, we observe a sharp increase in problem difficulty with respect to the number of variables, motivating further analysis of regular XORSAT.

PDF Details
v2026.09.13