scholarly journals SUNNY: a Lazy Portfolio Approach for Constraint Solving

2014 ◽  
Vol 14 (4-5) ◽  
pp. 509-524 ◽  
Author(s):  
ROBERTO AMADINI ◽  
MAURIZIO GABBRIELLI ◽  
JACOPO MAURO

AbstractWithin the context of constraint solving, a portfolio approach allows one to exploit the synergy between different solvers in order to create a globally better solver. In this paper we present SUNNY: a simple and flexible algorithm that takes advantage of a portfolio of constraint solvers in order to compute — without learning an explicit model — a schedule of them for solving a given Constraint Satisfaction Problem (CSP). Motivated by the performance reached by SUNNY vs. different simulations of other state of the art approaches, we developedsunny-csp, an effective portfolio solver that exploits the underlying SUNNY algorithm in order to solve a given CSP. Empirical tests conducted on exhaustive benchmarks of MiniZinc models show that the actual performance ofsunny-cspconforms to the predictions. This is encouraging both for improving the power of CSP portfolio solvers and for trying to export them to fields such as Answer Set Programming and Constraint Logic Programming.

2019 ◽  
Vol 20 (2) ◽  
pp. 176-204 ◽  
Author(s):  
MARTIN GEBSER ◽  
MARCO MARATEA ◽  
FRANCESCO RICCA

AbstractAnswer Set Programming (ASP) is a prominent knowledge representation language with roots in logic programming and non-monotonic reasoning. Biennial ASP competitions are organized in order to furnish challenging benchmark collections and assess the advancement of the state of the art in ASP solving. In this paper, we report on the design and results of the Seventh ASP Competition, jointly organized by the University of Calabria (Italy), the University of Genova (Italy), and the University of Potsdam (Germany), in affiliation with the 14th International Conference on Logic Programming and Non-Monotonic Reasoning (LPNMR 2017).


Author(s):  
Roman Barták

Constraints appear in many areas of human endeavour starting from puzzles like crosswords (the words can only overlap at the same letter) and recently popular Sudoku (no number appears twice in a row) through everyday problems such as planning a meeting (the meeting room must accommodate all participants) till solving hard optimization problems for example in manufacturing scheduling (a job must finish before another job). Though all these problems look like being from completely different worlds, they all share a similar base – the task is to find values of decision variables, such as the start time of the job or the position of the number at a board, respecting given constraints. This problem is called a Constraint Satisfaction Problem (CSP). Constraint processing emerged from AI research in 1970s (Montanary, 1974) when problems such as scene labelling were studied (Waltz, 1975). The goal of scene labelling was to recognize a type of line (and then a type of object) in the 2D picture of a 3D scene. The possible types were convex, concave, and occluding lines and the combination of types was restricted at junctions of lines to be physically feasible. This scene labelling problem is probably the first problem formalised as a CSP and some techniques developed for solving this problem, namely arc consistency, are still in the core of constraint processing. Systematic use of constraints in programming systems has started in 1980s when researchers identified a similarity between unification in logic programming and constraint satisfaction (Gallaire, 1985) (Jaffar & Lassez, 1987). Constraint Logic Programming was born. Today Constraint Programming is a separate subject independent of the underlying programming language, though constraint logic programming still plays a prominent role thanks to natural integration of constraints into a logic programming framework. This article presents mainstream techniques for solving constraint satisfaction problems. These techniques stay behind the existing constraint solvers and their understanding is important to exploit fully the available technology.


2020 ◽  
Vol 177 (3-4) ◽  
pp. 275-296
Author(s):  
Manuel Bichler ◽  
Michael Morak ◽  
Stefan Woltran

State-of-the-art answer set programming (ASP) solvers rely on a program called a grounder to convert non-ground programs containing variables into variable-free, propositional programs. The size of this grounding depends heavily on the size of the non-ground rules, and thus, reducing the size of such rules is a promising approach to improve solving performance. To this end, in this paper we announce lpopt, a tool that decomposes large logic programming rules into smaller rules that are easier to handle for current solvers. The tool is specifically tailored to handle the standard syntax of the ASP language (ASP-Core) and makes it easier for users to write efficient and intuitive ASP programs, which would otherwise often require significant handtuning by expert ASP engineers. It is based on an idea proposed by Morak and Woltran (2012) that we extend significantly in order to handle the full ASP syntax, including complex constructs like aggregates, weak constraints, and arithmetic expressions. We present the algorithm, the theoretical foundations on how to treat these constructs, as well as an experimental evaluation showing the viability of our approach.


2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Manuel Bodirsky ◽  
Bertalan Bodor

Abstract Let K exp + \mathcal{K}_{{\operatorname{exp}}{+}} be the class of all structures 𝔄 such that the automorphism group of 𝔄 has at most c ⁢ n d ⁢ n cn^{dn} orbits in its componentwise action on the set of 𝑛-tuples with pairwise distinct entries, for some constants c , d c,d with d < 1 d<1 . We show that K exp + \mathcal{K}_{{\operatorname{exp}}{+}} is precisely the class of finite covers of first-order reducts of unary structures, and also that K exp + \mathcal{K}_{{\operatorname{exp}}{+}} is precisely the class of first-order reducts of finite covers of unary structures. It follows that the class of first-order reducts of finite covers of unary structures is closed under taking model companions and model-complete cores, which is an important property when studying the constraint satisfaction problem for structures from K exp + \mathcal{K}_{{\operatorname{exp}}{+}} . We also show that Thomas’ conjecture holds for K exp + \mathcal{K}_{{\operatorname{exp}}{+}} : all structures in K exp + \mathcal{K}_{{\operatorname{exp}}{+}} have finitely many first-order reducts up to first-order interdefinability.


2020 ◽  
Vol 176 (3-4) ◽  
pp. 271-297
Author(s):  
Mario Alviano ◽  
Carmine Dodaro

Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K, which generalizes ONE and PMRES. Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition.


Sign in / Sign up

Export Citation Format

Share Document