The paper is available locally. The solver extended by this paper is described by A Flexible Solver for Finite Arithmetic Circuits (2012). This is a companion paper to Towards Weighted Default Reasoning (2017) and sets the stage for that work.

Rejected from ICLP’17, but this was a precursor to chapter 3 of my thesis.

Abstract:

Weighted logic programs specify potentially infinite generalized computational circuits; here, we consider an extension of our solver to handle these circuits. To maintain computational tractability and to improve efficiency, we extend that algorithm with set-at-a-time reasoning, wherein potentially infinite sets of structurally related steps of the solver are processed as a single step. The new algorithm manipulates representations of sets and bags of trees generated by the weighted logic program being solved. It assumes, among other operations, the ability to take unions, intersections, and differences of such sets, to test whether they are subsets of one another, and to determine their cardinality. We discuss some simple cases where this assumption is reasonable before introducing a proposal to weaken the assumption and allow for a wider class of programs.

BibTeX:

@TechReport{filardo:setatatime,
  author  = {Filardo, Nathaniel Wesley and Eisner, Jason},
  title   = {Set-at-a-Time Solving in Weighted Logic Programs},
  year    = {2017},
  month   = {6}
}