Author name cluster

Paul Saikko

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.

8 papers

2 author rows

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.

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

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

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 speciﬁc instantiations of the approach—based on interactions between a Boolean satisﬁability (SAT) solver and an integer programming (IP) solver—in the context of maximum satisﬁability (MaxSAT). The framework opens up opportunities for developing implicit hitting set algorithms for various important reasoning problems in KR by implementing domain-speciﬁc reasoning modules with SAT and IP solvers. We detail instantiations of the framework for the minimum satisﬁability 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 efﬁciency 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. Speciﬁcally (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-speciﬁc ways via SAT and IP solvers speciﬁcally well-suited for the respective tasks of providing proofs of unsatisﬁability and optimization. We detail novel instantiations of the general framework, using as a running example minimum satisﬁability, 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 efﬁciency of an approach based on encoding and solving propositional abduction instances as disjunctive logic programming under answer set semantics (Brewka, Eiter, and Truszczyń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

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

IJCAI Conference 2015 Conference Paper

Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT

Jeremias Berg
Paul Saikko
Matti J
auml; rvisalo

Solvers for the Maximum satisfiability (MaxSAT) problem find an increasing number of applications today. We focus on improving MaxHS—one of the most successful recent MaxSAT algorithms— via SAT-based preprocessing. We show that employing SAT-based preprocessing via the so-called labelled CNF (LCNF) framework before calling MaxHS can in some cases greatly degrade the performance of the solver. As a remedy, we propose a lifting of MaxHS that works directly on LCNFs, allowing for a tighter integration of SAT-based preprocessing and MaxHS. Our empirical results on standard crafted and industrial weighted partial MaxSAT Evaluation benchmarks show overall improvements over the original MaxHS algorithm both with and without SAT-based preprocessing.

PDF Details