PaperlayerView exact revision on arXiv

Source-linked AI summary

Multi-shot ASP solving with clingo

Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Torsten Schaub

arXiv:1705.09811v2cs.AI

TL;DR

The paper addresses the rigidity of one-shot ASP when logic programs evolve during reasoning. It introduces multi-shot ASP solving with operational semantics and implements it in clingo through modular program control, external atoms, and an API. The framework supports applications built on evolving ASP processes and has been used in several ASP-based reasoning systems.

  • Problem

    One-shot ASP uses a fixed grounding-and-solving process, limiting reasoning tasks whose programs change during computation.

  • Method

    The paper defines operational semantics for evolving grounder and solver states and implements multi-shot control in clingo using subprograms, externals, and an API.

  • Results

    Clingo’s multi-shot framework has been used to implement several ASP-based reasoning systems and aggregate extensions.

  • Takeaways & Limitations

    Multi-shot solving supports engineering declarative systems that combine ASP modeling with traditional programming to control reasoning processes.

  • Takeaways & Limitations

    Composing interacting subprograms requires care because contextual grounding affects inputs, outputs, and resulting ground programs.

Abstract

from arXiv · show

We introduce a new flexible paradigm of grounding and solving in Answer Set Programming (ASP), which we refer to as multi-shot ASP solving, and present its implementation in the ASP system clingo. Multi-shot ASP solving features grounding and solving processes that deal with continuously changing logic programs. In doing so, they remain operative and accommodate changes in a seamless way. For instance, such processes allow for advanced forms of search, as in optimization or theory solving, or interaction with an environment, as in robotics or query-answering. Common to them is that the problem specification evolves during the reasoning process, either because data or constraints are added, deleted, or replaced. This evolutionary aspect adds another dimension to ASP since it brings about state changing operations. We address this issue by providing an operational semantics that characterizes grounding and solving processes in multi-shot ASP solving. This characterization provides a semantic account of grounder and solver states along with the operations manipulating them. The operative nature of multi-shot solving avoids redundancies in relaunching grounder and solver programs and benefits from the solver's learning capacities. clingo accomplishes this by complementing ASP's declarative input language with control capacities. On the declarative side, a new directive allows for structuring logic programs into named and parameterizable subprograms. The grounding and integration of these subprograms into the solving process is completely modular and fully controllable from the procedural side. To this end, clingo offers a new application programming interface that is conveniently accessible via scripting languages.

1 Introduction

Traditional ASP systems use a fixed ground-then-solve process, while multi-shot ASP solving supports continuously changing programs through operative, controllable grounding and solving processes.

  • Traditional ASP systems ground a logic program and then compute stable models of the resulting propositional program.
  • Earlier incremental and reactive systems still relied on predefined control loops without user control.
  • Multi-shot solving introduces state-changing operations for adding, grounding, and solving programs and setting external atom truth values.
  • Clingo combines declarative ASP with procedural control, including modular subprogram integration and an API accessible through scripting languages.

2 Formal preliminaries

The preliminaries define normal logic programs, grounding, stable models, dependency structure, modules, and compositional joins used to formalize multi-shot solving.

  • A normal logic program consists of rules with heads and positive or negative body atoms, and grounding replaces variables with ground terms.
  • The positive atom dependency graph and its strongly connected components expose recursive structure in a grounded program.
  • Stable models are characterized as minimal models of the grounded program after removing rules whose negative bodies conflict with the candidate.
  • A module comprises a ground program with disjoint input and output atoms, with every rule head included among its outputs.
  • Compositional modules prohibit overlapping outputs and positive recursion across modules, enabling their join and stable-model combination under the module theorem.

3 Multi-shot solving with clingo at a glance

Clingo makes multi-shot solving programmable by organizing rules into parameterized subprograms and controlling grounding, solving, and external atoms procedurally.

  • The #program directive partitions non-ground rules into named subprograms with optional parameters.
  • Without additional control instructions, clingo grounds and solves only the base subprogram, preserving standard one-shot behavior.
  • Python control routines choose which subprograms to ground and then invoke solving, including parameterized instantiations such as acid(42).
  • Changing external truth values can activate or deactivate rules, supporting evolving reasoning processes such as modified planning problems.
  • External atoms declared with #external can remain undefined during grounding and later receive truth values through clingo’s API.

4 Multi-shot solving

Multi-shot ASP solving provides formal and operational foundations for evolving logic programs, together with modular grounding, external control, and state-changing solving operations.

  • Parameterizable subprograms: Named, parameterizable subprograms let clingo instantiate and ground program components modularly within a controllable process.A declaration associates a name and parameters with a subprogram scope; instantiation replaces parameters with supplied terms.
  • Contextual grounding: Contextual grounding uses an atom base to avoid irrelevant rule instances while preserving stable models under the stated compositionality condition.For example, the irrelevant instance c(42,42) ← a(42) is dropped, and Proposition 1 establishes stable-model equivalence under its assumptions.
  • Extensible logic programs: Programs with external atoms support truth assignments that determine stable models, making externals a major building block of multi-shot solving.The assignment distinguishes true and undefined inputs, while unassigned inputs are treated as false by default.
  • Composing logic programs with externals: Composing extensible subprograms requires care because contextual grounding can alter inputs, outputs, and resulting programs, and may violate compositionality in later joins.The paper identifies a condition restricting subsequent heads to prior input atoms, while noting that even then contextual and full grounding can remain imbalanced.
  • State-based characterization: Multi-shot solving characterizes evolving grounding and solving through an operational semantics over sequences of system states and associated operations.The semantics accounts for programs retained by the grounder and solver during successive solving steps.
  • Example: Changing an external assignment can switch the solving outcome: making p(3) true yields {p(0), p(3)}, whereas withdrawing that derivation yields no stable model.The solve operation leaves the system state intact while reporting the models associated with the current assignment and grounded program.

5 Using multi-shot solving in practice

The paper illustrates multi-shot solving through several case studies, using them to demonstrate clingo’s functionalities in practice.

  • Several case studies illustrate the usage of multi-shot solving.
  • The examples follow the formal foundations and an overview of clingo’s constructs.
  • The paper uses practical examples to demonstrate multi-shot functionalities.

5.1 Incremental ASP solving

Incremental ASP solving adapts the Towers of Hanoi encoding into a clingo-controlled, iterative process. Each iteration grounds parameterized subprograms, updates external query atoms, solves, and accumulates the evolving program state.

  • Incremental solving gradually processes problem extensions instead of repeatedly re-processing the entire extended problem.This avoids redundancies in iterative deepening-style reasoning.
  • The Towers of Hanoi encoding separates static knowledge, transitions, and the query into base, step(t), and an external-controlled constraint.The base contains the instance and initial facts; step(t) describes transitions, while the query’s volatility is controlled externally.
  • The Python control loop uses imin, imax, and istop to govern iteration bounds and termination criteria.The loop assembles subprogram calls, performs cleanup, grounds them, assigns externals, and solves.
  • Each iteration grounds check(step) and step(step), activates the current query(step), and releases the previous query.Only the current integrity constraint remains effective because released query atoms are false under stable-model semantics.
  • Solver-determined atom values are communicated to the grounder, enabling simplifications during subsequent grounding steps.cleanup removes atoms from the current atom base and may mark some as facts.
  • 16 solver calls find a plan of length 15, producing one model in 0.020s.The reported result is SATISFIABLE with Models : 1 and Calls : 16.
  • The evolving system state includes non-ground subprograms, accumulated grounded modules, the current query atom, output atoms, and its partial assignment.The trace describes successive solve invocations over these state components.

5.2 n-Queens problem

The n-Queens example incrementally extends boards and reuses grounded rules while encoding row, column, and diagonal cardinality constraints. The construction supports solving an increasing series of board sizes without redundant instantiation.

  • The example solves a series of n-Queens problems with increasing board sizes rather than a single fixed board.
  • Incremental cardinality constraints: At-most-one encodings incrementally add positions, propagate attack information, and forbid selecting an attacked position.The encoding uses q(i) for positions and a(i) for auxiliary attack indicators.
  • Incremental cardinality constraints: The incremental exactly-one encoding has stable models corresponding one-to-one with singleton subsets of {q1, . . . , qn}.
  • An incremental encoding: Increasing the board from n to n+1 adds one row and column while interconnecting cells through predecessor and successor attack links.The links cover backward and forward diagonals, horizontal rows, and vertical columns.
  • An incremental encoding: The complete encoding combines at-most-one constraints for diagonals with exactly-one constraints for rows and columns.Choice rules place queens, attack rules identify attacked cells, and integrity constraints enforce the cardinality conditions.
  • An incremental encoding: The main routine can process arbitrary increasing board sequences while grounding intermediate board sizes whose rules remain relevant.For example, six requested boards can require instantiating board(n) with nine successive parameter terms.

5.3 Ricochet Robots

The Ricochet Robots example models board movement, externally supplied positions and goals, and shortest bounded plans. Multi-shot solving then supports playing successive rounds from the previous round’s resulting positions.

  • Encoding Ricochet Robots: Ricochet Robots uses a 16×16 grid, four colored robots, barriers, and moves that continue until a barrier or another robot is encountered.
  • Encoding Ricochet Robots: External atoms allow initial robot positions and target goals to be supplied from outside the solving process.Each robot can be placed at 256 locations, and goal atoms select target locations.
  • Encoding Ricochet Robots: The encoding represents time steps, directions, movement, stopping conditions, and persistent positions, then enforces the target at the horizon.
  • Encoding Ricochet Robots: From cornered initial positions, the resulting plan reaches goal(13) after nine steps, with a tenth move redundantly repeating the goal-achieving move.
  • Playing in rounds: Playing successive rounds requires the next goal to start from the robots’ positions after the previous round.The multi-shot approach uses a single operational clingo control object in a loop.

5.4 Optimization

clingo supports incremental optimization as evolving programs change objective functions. Objectives can accumulate new terms or dismiss terms through externally controlled activation atoms.

  • Incremental optimization adapts objective functions while a program evolves, including shortest-plan search with non-consecutive horizons.
  • Grounding cumulativeObjective(t) for successive t values extends each priority-level objective while retaining earlier move terms.
  • Externally activated objective terms can be disabled so the corresponding move literals are removed from the objective function.

6 Application program interfaces

clingo’s APIs expose parsing, grounding, and solving through interfaces available in several programming languages. They support program construction, inspection, callbacks, and interactions with solver models.

  • clingo provides C, C++, Lua, and Python APIs with shared functionality.
  • Control objects capture grounder and solver states and can be created independently for multiple interacting clingo processes.
  • Parsing: The parsing interface produces or accepts abstract syntax trees, enabling transformations of non-ground programs.
  • Grounding: Grounding interfaces incrementally augment programs from files or strings and support dynamically generated programs.
  • Grounding: Lower-level grounding access permits inspecting ground atoms, adding aspif rules, and injecting symbols during grounding.
  • Solving: The solve interface supports model callbacks that inspect stable models and can add constraints or perform final tests.

7 Experiments

Experiments compare single-shot solving with four multi-shot settings across Towers of Hanoi, Ricochet Robots, and PDDL benchmarks. Multi-shot solving generally reduces conflicts and runtime, but the value of retaining long nogoods and heuristic values depends on the benchmark.

  • Experimental setup: Multi-shot solving was evaluated by retaining or discarding recorded nogoods and heuristic values between solver calls, alongside single-shot solving from scratch.The four multi-shot settings isolate the effects of retaining each type of solver information.
  • Experimental setup: Cactus plots order instances by time and conflicts, with separate y-axes reporting runtimes and conflict counts.The magnitude of conflicts is given above the lower plot’s y-axis.
  • Towers of Hanoi: On Towers of Hanoi, single-shot solving completed none of 45 instances within 3000 seconds, while multi-shot settings discarding recorded nogoods completed all 45.The comparison is attributed to incremental grounding and reduced search conflicts in multi-shot solving.
  • Towers of Hanoi: On Towers of Hanoi, retaining long nogoods reduced runtime and conflicts by factors of about 5 and 1.5 in the multi and multi-heuristic settings, respectively.The reported savings outweighed memory overhead on this benchmark, whereas retaining heuristic values did not pay off.
  • Ricochet Robots: On Ricochet Robots, single-shot solving completed 22 of 38 instances, whereas multi-heuristic-nogoods solved all 38; retaining long nogoods did not significantly reduce conflicts.The two settings discarding long nogoods led in runtime and solved instances.
  • PDDL and cross-benchmark observations: On PDDL benchmarks, only the two settings discarding long nogoods completed all instances in time, while retaining long nogoods incurred overhead without corresponding benefits.Across all benchmarks, multi-shot settings had fewer conflicts than single-shot, and nogood treatment influenced runtime more than heuristic treatment.
  • Memory use: Peak memory consumption was 187 MB for multi-shot solving versus 150 MB for single-shot solving across the benchmarks.The authors attribute the difference probably to larger databases of learned clauses in multi-shot settings.

8 Related work

Related systems provide incremental solving, procedural attachment, or external computation, but they differ in modeling support and control granularity. clingo combines ASP modeling with repeated grounding and solving under procedural control.

  • Earlier clingo: Earlier clingo scripting supported deterministic computations during grounding but did not provide library functions in clingo 3.This contrasts with the broader control capacities described for the multi-shot framework.
  • External computation: dlvhex integrates external computation sources through higher-order logic programs and external higher-order atoms evaluated procedurally during solving.These external atoms are distinguished from clingo’s #external directive.
  • Procedural attachment: The idp system supports multiple grounder and solver calls, solution inspection, and reactions to external input through C++ and Lua interfaces.Unlike clingo, its emphasis is high-level control integrated with the modeling language rather than fine-grained process control.
  • SAT interfaces: SAT incremental interfaces support low-level solving under assumptions, but SAT solvers and APIs lack support for modeling languages and grounding.The clingo framework adds these capabilities around ASP’s modeling and grounding process.

9 Conclusion

The conclusion presents clingo as an integrated framework for evolving ASP programs under procedural control. It broadens ASP applications and supports an engineering style that combines ASP modeling with traditional programming, while identifying further work on program change operations.

  • Framework: clingo integrates declarative ASP with procedural control for adding, deleting, and replacing programs within one grounding and solving process.Its API supports evolving logic programs and customizable subprogram instantiation between solver invocations.
  • Applications: The framework targets applications involving evolving programs, including planning, robotics, stream reasoning, user interaction, theory solving, and advanced search.The paper contrasts this customizable approach with the dedicated, rigid procedures of earlier systems such as iclingo and oclingo.
  • Semantics and future work: The semantic framework uses module theory to capture dynamic combinations of logic programs generically, while noting that composing ASP subprograms is difficult because ASP is nonmonotonic.The conclusion identifies practicalizing update, forgetting, revision, and merging operations as future work.
  • Scope: clingo supports normal and extended disjunctive logic programs and includes multi-threaded solving and domain-specific heuristics through clasp.The presented formal development focuses on normal logic programs.
  • Adoption: Since its first release, clingo’s multi-shot framework has supported systems including asprin, aspic, rosoclingo, and dflat, as well as implementations of aggregate forms.The conclusion presents these uses as evidence of the framework’s potential impact.
  • Conclusion: Multi-shot solving broadens ASP applications and combines ASP modeling with traditional programming to control an ASP solving process.The paper presents this engineering facet as important for putting ASP into practice.
Loading 1705.09811v2…