1,721,046 research outputs found
A MaxSAT algorithm using cardinality constraints of bounded size
No full textCore-guided algorithms proved to be effective on industrial instances of MaxSAT, the optimization variant of the satisfiability problem for propositional formulas. These algorithms work by iteratively checking satisfiability of a formula that is relaxed at each step by using the information provided by unsatisfiable cores. The paper introduces a new core-guided algorithm that adds cardinality constraints for each detected core, but also limits the number of literals in each constraint in order to control the number of refutations in subsequent satisfiability checks. The performance gain of the new algorithm is assessed on the industrial instances of the 2014 MaxSAT Evaluation
External propagators in wasp: Preliminary report
No full textState-of-the-art ASP solvers are based on a variant of the CDCL algorithm. One of the key features of CDCL is the propagation step, whose role is to implement deterministic consequences of the input theory. It is well-known that the performance of solvers can be considerably improved on specific benchmarks by adding custom propagation functions. However, embedding a new propagator into an existing solver often requires non-trivial modifications. In this paper, we report on an extension of the ASP solver WASP that allows to provide new propagators externally, i.e. no modifications of the solver are needed. We assess our proposal on a recent application of ASP to abduction in Natural Language Understanding, where plain ASP solvers are not effective. Preliminary experiments on real-world instances show encouraging results
Multi-engine ASP solving with policy adaptation
Full text linkThe recent application of Machine Learning techniques to the Answer Set Programming (ASP) field proved to be effective. In particular, the multi-engine ASP solverME-ASPis efficient: it is able to solve more instances than any other ASP system that participated to the 3rd ASP Competition on the "System Track" benchmarks. In theME-ASPapproach, classification methods inductively learn off-line algorithm selection policies starting from both a set offeaturesof instances in atrainingset,
and the solvers performance on such instances.In this paper we present an improvement to the multi-engine framework ofME-ASP, in which we add the capability of updating the learned policies when the original approach fails to give good predictions. An experimental analysis, conducted on training and test sets of ground instances obtained from the ones submitted to the "System Track" of the 3rd ASP Competition, shows that the policy adaptation improves the performance ofME-ASPwhen applied to test sets containing domains of instances that were not considered for training
Anytime computation of cautious consequences in answer set programming
No full textQuery answering in Answer Set Programming (ASP) is usually solved by computing (a subset of) the cautious consequences of a logic program. This task is computationally very hard, and there are programs for which computing cautious consequences is not viable in reasonable time. However, current ASP solvers produce the (whole) set of cautious consequences only at the end of their computation. This paper reports on strategies for computing cautious consequences, also introducing anytime algorithms able to produce sound answers during the computation. © 2014 Cambridge University Press
JWASP: A new Java-based ASP solver
No full textAnswer Set Programming (ASP) is a well-known declarative programming language for knowledge representation and non-monotonic reasoning. ASP solvers are usually written in C/C++ with the aim of extremely optimizing their performance. Indeed, C/C++ allow for several low level optimizations, which however come at the price of a less portable implementation. This is a problem for some real world use cases which do not actually require an extremely efficient computation, but would benefit from platform-independent and easilydeployable implementation. Motivated by such use cases, we develop JWASP, a new ASP solver written in Java and extending the open source library SAT4J in order to process ASP programs with atomic heads. We also report on a preliminary experiment assessing the performance of JWASP, whose results are encouraging: JWASP is a good candidate as an alternative ASP solver for platform-independent applications, which cannot rely on current ASP solvers
ASPQ: An ASP-based 2QBF solver
No full textAnswer Set Programming (ASP) is an established logic-based programming paradigm which has been successfully applied for solving complex problems. Since ASP can model problems up to the second level of the polynomial hierarchy, it can be used to model and solve the 2QBF problem. In this paper we show how to obtain a fairly effective 2QBF solver by just resorting to state-of-The-Art ASP solvers
Applying machine learning techniques to ASP solving
Full text linkHaving in mind the task of improving the solving methods for Answer Set Programming (ASP), there are two usual ways to reach this goal: (i) extending state-of-the-art techniques and ASP solvers, or (ii) designing a new ASP solver from scratch. An alternative to these trends is to build on top of state-of-the-art solvers, and to apply machine learning techniques for choosing automatically the
“best” available solver on a per-instance basis.In this paper we pursue this latter direction. We first define a set of cheap-to- compute syntactic features that characterize several aspects of ASP programs. Then, we apply classification methods that, given the features of the instances in a training set and the solvers performance on these instances, inductively learn algorithm selection strategies to be applied to a test set. We report the results of a number of experiments considering solvers and different training and test sets of instances taken from the ones submitted to the “System Track” of the 3rdASP competition. Our analysis shows that, by applying machine learning techniques to ASP solving, it is possible to obtain very robust performance: our approach can solve a significantly higher number of instances compared with any
solver that entered the 3rdASP competition
- …
