Standard answer set programming (ASP) targets at solving search problems from the first level of the polynomial time hierarchy (PH). Tackling search problems beyond NP using ASP is less straightforward. The class of d...
详细信息
Standard answer set programming (ASP) targets at solving search problems from the first level of the polynomial time hierarchy (PH). Tackling search problems beyond NP using ASP is less straightforward. The class of disjunctive logic programs offers the most prominent way of reaching the second level of the PH, but encoding respective hard problems as disjunctive programs typically requires sophisticated techniques such as saturation or meta-interpretation. The application of such techniques easily leads to encodings that are inaccessible to non-experts. Furthermore, while disjunctive ASP solvers often rely on calls to a (co-)NP oracle, it may be difficult to detect from the input program where the oracle is being accessed. In other formalisms, such as Quantified Boolean Formulas (QBFs), the interface to the underlying oracle is more transparent as it is explicitly recorded in the quantifier prefix of a formula. On the other hand, ASP has advantages over QBFs from the modeling perspective. The rich high-level languages such as ASP-Core-2 offer a wide variety of primitives that enable concise and natural encodings of search problems. In this paper, we present a novel logicprogramming-based modeling paradigm that combines the best features of ASP and QBFs. We develop so-called combined logic programs in which oracles are directly cast as (normal) logic programs themselves. Recursive incarnations of this construction enable logicprogramming on arbitrarily high levels of the PH. We develop a proof-of-concept implementation for our new paradigm.
Since the introduction of the stable marriage problem (SMP) by Gale and Shapley (1962), several variants and extensions have been investigated. While this variety is useful to widen the application potential, each var...
详细信息
Since the introduction of the stable marriage problem (SMP) by Gale and Shapley (1962), several variants and extensions have been investigated. While this variety is useful to widen the application potential, each variant requires a new algorithm for finding the stable matchings. To address this issue, we propose an encoding of the SMP using answer set programming (ASP), which can straightforwardly be adapted and extended to suit the needs of specific applications. The use of ASP also means that we can take advantage of highly efficient off-the-shelf solvers. To illustrate the flexibility of our approach, we show how our ASP encoding naturally allows us to select optimal stable matchings, i.e. matchings that are optimal according to some user-specified criterion. To the best of our knowledge, our encoding offers the first exact implementation to find sex-equal, minimum regret, egalitarian or maximum cardinality stable matchings for SMP instances in which individuals may designate unacceptable partners and ties between preferences are allowed.
This paper presents the pl-nauty library, a Prolog interface to the nauty graph-automorphism tool. Adding the capabilities of nauty to Prolog combines the strength of the "generate and prune" approach that i...
详细信息
This paper presents the pl-nauty library, a Prolog interface to the nauty graph-automorphism tool. Adding the capabilities of nauty to Prolog combines the strength of the "generate and prune" approach that is commonly used in logicprogramming and constraint solving, with the ability to reduce symmetries while reasoning over graph objects. Moreover, it enables the integration of nauty in existing tool-chains, such as SAT-solvers or finite domain constraints compilers which exist for Prolog. The implementation consists of two components: pl-nauty, an interface connecting nauty's C library with Prolog, and pl-gtools, a Prolog framework integrating the software component of nauty, called gtools, with Prolog. The complete tool is available as a SWI-Prolog module. We provide a series of usage examples including two that apply to generate Ramsey graphs.
In the Declarative Networking paradigm, Datalog-like languages are used to express distributed computations. Whereas recently formal operational semantics for these languages have been developed, a corresponding decla...
详细信息
In the Declarative Networking paradigm, Datalog-like languages are used to express distributed computations. Whereas recently formal operational semantics for these languages have been developed, a corresponding declarative semantics has been lacking so far. The challenge is to capture precisely the amount of nondeterminism that is inherent to distributed computations due to concurrency, networking delays, and asynchronous communication. This paper shows how a declarative, model-based semantics can be obtained by simply using the well-known stable model semantics for Datalog with negation. We show that the model-based semantics matches previously proposed formal operational semantics.
As software systems are getting increasingly connected, there is a need for equipping nonmonotonic logic programs with access to external sources that are possibly remote and may contain information in heterogeneous f...
详细信息
As software systems are getting increasingly connected, there is a need for equipping nonmonotonic logic programs with access to external sources that are possibly remote and may contain information in heterogeneous formats. To cater for this need, hex programs were designed as a generalization of answer set programs with an API style interface that allows to access arbitrary external sources, providing great flexibility. Efficient evaluation of such programs however is challenging, and it requires to interleave external computation and model building;to decide when to switch between these tasks is difficult, and existing approaches have limited scalability in many real-world application scenarios. We present a new approach for the evaluation of logic programs with external source access, which is based on a configurable framework for dividing the non-ground program into possibly overlapping smaller parts called evaluation units. The latter will be processed by interleaving external evaluation and model building using an evaluation graph and a model graph, respectively, and by combining intermediate results. Experiments with our prototype implementation show a significant improvement compared to previous approaches. While designed for hex-programs, the new evaluation approach may be deployed to related rule-based formalisms as well.
The paper proposes a fresh look at the concept of goal and advances that motivational attitudes like desire, goal and intention are just facets of the broader notion of (acceptable) outcome. We propose to encode the p...
详细信息
The paper proposes a fresh look at the concept of goal and advances that motivational attitudes like desire, goal and intention are just facets of the broader notion of (acceptable) outcome. We propose to encode the preferences of an agent as sequences of "alternative acceptable outcomes". We then study how the agent's beliefs and norms can be used to filter the mental attitudes out of the sequences of alternative acceptable outcomes. Finally, we formalise such intuitions in a novel Modal Defeasible logic and we prove that the resulting formalisation is computationally feasible.
Modular logic programs provide a way of viewing logic programs as consisting of many independent, meaningful modules. This paper introduces first-order modular logic programs, which can capture the meaning of many ans...
详细信息
Modular logic programs provide a way of viewing logic programs as consisting of many independent, meaningful modules. This paper introduces first-order modular logic programs, which can capture the meaning of many answer set programs. We also introduce conservative extensions of such programs. This concept helps to identify strong relationships between modular programs as well as between traditional programs. We show how the notion of a conservative extension can be used to justify the common projection rewriting.
In recent years, several frameworks and systems have been proposed that extend Inductive logicprogramming (ILP) to the Answer Set programming (ASP) paradigm. In ILP, examples must all be explained by a hypothesis tog...
详细信息
In recent years, several frameworks and systems have been proposed that extend Inductive logicprogramming (ILP) to the Answer Set programming (ASP) paradigm. In ILP, examples must all be explained by a hypothesis together with a given background knowledge. In existing systems, the background knowledge is the same for all examples;however, examples may be context-dependent. This means that some examples should be explained in the context of some information, whereas others should be explained in different contexts. In this paper, we capture this notion and present a context-dependent extension of the Learning from Ordered Answer Sets framework. In this extension, contexts can be used to further structure the background knowledge. We then propose a new iterative algorithm, ILASP2i, which exploits this feature to scale up the existing ILASP2 system to learning tasks with large numbers of examples. We demonstrate the gain in scalability by applying both algorithms to various learning tasks. Our results show that, compared to ILASP2, the newly proposed ILASP2i system can be two orders of magnitude faster and use two orders of magnitude less memory, whilst preserving the same average accuracy.
Answer Set programming (ASP) is a popular logicprogramming paradigm that has been applied for solving a variety of complex problems. Among the most challenging real-world applications of ASP are two industrial proble...
详细信息
Answer Set programming (ASP) is a popular logicprogramming paradigm that has been applied for solving a variety of complex problems. Among the most challenging real-world applications of ASP are two industrial problems defined by Siemens: the Partner Units Problem (PUP) and the Combined Configuration Problem (CCP). The hardest instances of PUP and CCP are out of reach for state-of-the-art ASP solvers. Experiments show that the performance of ASP solvers could be significantly improved by embedding domain-specific heuristics, but a proper effective integration of such criteria in off-the-shelf ASP implementations is not obvious. In this paper the combination of ASP and domain-specific heuristics is studied with the goal of effectively solving real-world problem instances of PUP and CCP. As a byproduct of this activity, the ASP solver WASP was extended with an interface that eases embedding new external heuristics in the solver. The evaluation shows that our domain-heuristic-driven ASP solver finds solutions for all the real-world instances of PUP and CCP ever provided by Siemens.
Answer set programming (ASP) is a well-established logicprogramming language that offers an intuitive, declarative syntax for problem solving. In its traditional application, a fixed ASP program for a given problem i...
详细信息
Answer set programming (ASP) is a well-established logicprogramming language that offers an intuitive, declarative syntax for problem solving. In its traditional application, a fixed ASP program for a given problem is designed and the actual instance of the problem is fed into the program as a set of facts. This approach typically results in programs with comparably short and simple rules. However, as is known from complexity analysis, such an approach limits the expressive power of ASP;in fact, an entire NP-check can be encoded into a single large rule body of bounded arity that performs both a guess and a check within the same rule. Here, we propose a novel paradigm for encoding hard problems in ASP by making explicit use of large rules which depend on the actual instance of the problem. We illustrate how this new encoding paradigm can be used, providing examples of problems from the first, second, and even third level of the polynomial hierarchy. As state-of-the-art solvers are tuned towards short rules, rule decomposition is a key technique in the practical realization of our approach. We also provide some preliminary benchmarks which indicate that giving up the convenient way of specifying a fixed program can lead to a significant speed-up.
暂无评论