Properties and Applications of Programs with Monotone and Convex Constraints

We study properties of programs with monotone and convex constraints. We extend to these formalisms concepts and results from normal logic programming. They include the notions of strong and uniform equivalence with their characterizations, tight programs and Fages Lemma, program completion and loop formulas. Our results provide an abstract account of properties of some recent extensions of logic programming with aggregates, especially the formalism of lparse programs. They imply a method to compute stable models of lparse programs by means of off-the-shelf solvers of pseudo-boolean constraints, which is often much faster than the smodels system.

Related papers:

title: Semantics of Logic Programs with Aggregates
abstract: We investigate the semantics of aggregates (count, sum, : : :) in logic programs with function symbols and negation. In particular we address the meaning of programs with recursion through aggregation. We extend the two most successful semantic approaches to the problem of recursion through negation, well founded models and stable models, to programs with aggregates. We examine previously deened classes of aggregate programs: aggregate stratiied, group stratiied, magical stratiied, monotonic and closed semi-ring programs and relate our semantics to those previously deened. The well-founded model gives a semantics to all programs containing aggregates, and agrees with two-valued models already deened for aggregate and group stratiied programs. Stable models give a meaning to many programs with aggregation, including all of the above classes, and captures all the models that have been previously deened. Further, there are programs not captured in any previously deened class where the unique stable model agrees with their \intuitive" semantics.

title: Partial Stable Models for Logic Programs with Aggregates
abstract: We introduce a family of partial stable model semantics for logic programs with arbitrary aggregate relations. The semantics are parametrized by the interpretation of aggregate relations in three-valued logic. Any semantics in this family satisfies two important properties: (i) it extends the partial stable semantics for normal logic programs and (ii) total stable models are always minimal. We also give a specific instance of the semantics and show that it has several attractive features.

title: Recursive Aggregates in Disjunctive Logic Programs: Semantics and Complexity
abstract: The addition of aggregates has been one of the most relevant enhancements to the language of answer set programming (ASP). They strengthen the modeling power of ASP, in terms of concise problem representations. While many important problems can be encoded using nonrecursive aggregates, some relevant examples lend themselves for the use of recursive aggregates. Previous semantic definitions typically agree in the nonrecursive case, but the picture is less clear for recursion. Some proposals explicitly avoid recursive aggregates, most others differ, and many of them do not satisfy desirable criteria, such as minimality or coincidence with answer sets in the aggregate-free case.

title: Extending and implementing the stable model semantics
abstract: A novel logic program like language, weight constraint rules, is developed for answer set programming purposes. It generalizes normal logic programs by allowing weight constraints in place of literals to represent, e.g., cardinality and resource constraints and by providing optimization capabilities. A declarative semantics is developed which extends the stable model semantics of normal programs. The computational complexity of the language is shown to be similar to that of normal programs under the stable model semantics. A simple embedding of general weight constraint rules to a small subclass of the language called basic constraint rules is devised. An implementation of the language, the SMODELS system, is developed based on this embedding. It uses a two level architecture consisting of a front-end and a kernel language implementation. The front-end allows restricted use of variables and functions and compiles general weight constraint rules to basic constraint rules. A major part of the work is the development of an efficient search procedure for computing stable models for this kernel language. The procedure is compared with and empirically tested against satisfiability checkers and an implementation of the stable model semantics. It offers a competitive implementation of the stable model semantics for normal programs and attractive performance for problems where the new types of rules provide a compact representation.

title: Strongly equivalent logic programs
abstract: A logic program Π1 is said to be equivalent to a logic program Π2 in the sense of the answer set semantics if Π1 and Π2 have the same answer sets. We are interested in the following stronger condition: for every logic program, Π, Π1, ∪ Π has the same answer sets as Π2 ∪ Π. The study of strong equivalence is important, because we learn from it how one can simplify a part of a logic program without looking at the rest of it. The main theorem shows that the verification of strong equivalence can be accomplished by cheching the equivalence of formulas in a monotonic logic, called the logic of here-and-there, which is intermediate between classical logic and intuitionistic logic.

title: Reducing Strong Equivalence of Logic Programs to Entailment in Classical Propositional Logic
abstract: Recently Lifschitz Pearce and Valverde introduced a notion of strong equivalence be tween two logic programs and showed that it can be captured in a valued logic In this pa per rst for propositional logic programs with default negation constraints and disjunctions we show that there is a simple mapping from these programs to propositional theories that reduces this notion of strong equivalence to en tailment in classical propositional logic Fur thermore we also provide a mapping in the other direction thus show that the problem of checking strong equivalence is co NP complete We then consider logic programs with variables One surprising result is that while the prob lem of deciding whether two logic programs are equivalent goes from decidable to undecidable when we move from logic programs without variables to ones with the problem of deciding whether two logic programs are strongly equiv alent remains to be co NP complete for logic programs with variables and constants

title: Strong equivalence made easy: nested expressions and weight constraints
abstract: Logic programs $P$ and $Q$ are strongly equivalent if, given any program $R$, programs $P \cup R$ and $Q \cup R$ are equivalent (that is, have the same answer sets). Strong equivalence is convenient for the study of equivalent transformations of logic programs: one can prove that a local change is correct without considering the whole program. Lifschitz, Pearce and Valverde showed that Heyting's logic of here-and-there can be used to characterize strong equivalence for logic programs with nested expressions (which subsume the better-known extended disjunctive programs). This note considers a simpler, more direct characterization of strong equivalence for such programs, and shows that it can also be applied without modification to the weight constraint programs of Niemelä and Simons. Thus, this characterization of strong equivalence is convenient for the study of equivalent transformations of logic programs written in the input languages of answer set programming systems dlv and SMODELS. The note concludes with a brief discussion of results that can be used to automate reasoning about strong equivalence, including a novel encoding that reduces the problem of deciding the strong equivalence of a pair of weight constraint programs to that of deciding the inconsistency of a weight constraint program.

title: Uniform Equivalence of Logic Programs under the Stable Model Semantics
abstract: In recent research on nonmonotonic logic programming, repeatedly strong equivalence of logic programs P and Q has been considered, which holds if the programs P ∪ R and Q∪ R have the same stable models for any other program R. This property strengthens equivalence of P and Q with respect to stable models (which is the particular case for R= ∅), and has an application in program optimization. In this paper, we consider the more liberal notion of uniform equivalence, in which R ranges only over the sets of facts rather than all sets of rules. This notion, which is well-known, is particularly useful for assessing whether programs P and Q are equivalent as components in a logic program which is modularly structured. We provide semantical characterizations of uniform equivalence for disjunctive logic programs and some restricted classes, and analyze the computational cost of uniform equivalence in the propositional (ground) case. Our results, which naturally extend to answer set semantics, complement the results on strong equivalence of logic programs and pave the way for optimizations in answer set solvers as a tool for input-based problem solving.

title: Tight logic programs
abstract: This note is about the relationship between two theories of negation as failure – one based on program completion, the other based on stable models, or answer sets. François Fages showed that if a logic program satisfies a certain syntactic condition, which is now called ‘tightness,’ then its stable models can be characterized as the models of its completion. We extend the definition of tightness and Fages' theorem to programs with nested expressions in the bodies of rules, and study tight logic programs containing the definition of the transitive closure of a predicate.

title: ASSAT: computing answer sets of a logic program by SAT solvers
abstract: We propose a new translation from normal logic programs with constraints under the answer set semantics to propositional logic. Given a logic program, we show that by adding, for each loop in the program, a corresponding loop formula to the program's completion, we obtain a one-to-one correspondence between the answer sets of the program and the models of the resulting propositional theory. Compared with the translation by Ben-Eliyahu and Dechter, ours has the advantage that it does not use any extra variables, and is considerably simpler, thus easier to understand. However, in the worst case, it requires computing exponential number of loop formulas. To address this problem, we propose an approach that adds loop formulas a few at a time, selectively. Based on these results, we implemented a system called ASSAT(X), depending on the SAT solver X used, and tested it on a variety of benchmarks including the graph coloring, the blocks world planning, and Hamiltonian Circuit domains. The results are compared with those by smodels and dlv, and it shows a clear edge of ASSAT(X) over them in these domains.

title: An Extensible SAT-solver
abstract: In this article, we present a small, complete, and efficient SAT-solver in the style of conflict-driven learning, as exemplified by Chaff. We aim to give sufficient details about implementation to enable the reader to construct his or her own solver in a very short time.This will allow users of SAT-solvers to make domain specific extensions or adaptions of current state-of-the-art SAT-techniques, to meet the needs of a particular application area. The presented solver is designed with this in mind, and includes among other things a mechanism for adding arbitrary boolean constraints. It also supports solving a series of related SAT-problems efficiently by an incremental SAT-interface.

title: Consistency of Clark's Completion and Existence of Stable Models 2 Introduction and Notations
abstract: 1 Abstract The most general notion of canonical model for a logic program with negation is the one of stable model 9]. In 7] the stable models of a logic program are characterized by the well-supported Herbrand models of the program, and a new xed point semantics that formalizes the bottom-up truth maintenance procedure of 4] is based on that characterization. Here we focus our attention on the abstract notion of well-supportedness in order to derive suucient conditions for the existence of stable models. We show that if a logic program is positive-order-consistent (i.e. there is no innnite decreasing chain w.r.t. the positive dependencies in the atom dependency graph of) then the Herbrand models of comp(() coincide with the stable models of. From this result and the ones of 10] 17] 2] on the consistency of Clark's completion, we obtain suf-cient conditions for the existence of stable models for positive-order-consistent programs. Then we show that a negative cycle free program can have no stable model if it is not positive-order-consistent, but that order-consistency alone 17] 2] (this condition generalizes call-consistency 10] 18], it is independent of positive-order-consistency) is suucient to ensure the existence of a stable model. The last result is based on a characterization of stable models due to 5] and on a generalization of the result of 17] on the consistency of Clark's completion to innnite logic programs. A logic program is a nite set of rules of the form L 1 A is an atom, called the conclusion and denoted by concl(R), and the L i 's are literals (i.e. atoms or negated atoms), called the premises and denoted by prem(R). We denote the subset of positive atoms in prem(R) by pos(R), and

title: Noise Strategies for Improving Local Search
abstract: It has recently been shown that local search is surprisingly good at finding satisfying assignments for certain computationally hard classes of CNF formulas. The performance of basic local search methods can be further enhanced by introducing mechanisms for escaping from local minima in the search space. We will compare three such mechanisms: simulated annealing, random noise, and a strategy called "mixed random walk". We show that mixed random walk is the superior strategy. We also present results demonstrating the effectiveness of local search with walk for solving circuit synthesis and circuit diagnosis problems. Finally, we demonstrate that mixed random walk improves upon the best known methods for solving MAX-SAT problems.

title: Semantics of Logic Programs with Aggregates
abstract: We investigate the semantics of aggregates (count, sum, : : :) in logic programs with function symbols and negation. In particular we address the meaning of programs with recursion through aggregation. We extend the two most successful semantic approaches to the problem of recursion through negation, well founded models and stable models, to programs with aggregates. We examine previously deened classes of aggregate programs: aggregate stratiied, group stratiied, magical stratiied, monotonic and closed semi-ring programs and relate our semantics to those previously deened. The well-founded model gives a semantics to all programs containing aggregates, and agrees with two-valued models already deened for aggregate and group stratiied programs. Stable models give a meaning to many programs with aggregation, including all of the above classes, and captures all the models that have been previously deened. Further, there are programs not captured in any previously deened class where the unique stable model agrees with their \intuitive" semantics.

title: Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning
abstract: In this paper we develop an algebraic framework for studying semantics of nonmonotonic logics. Our approach is formulated in the language of lattices, bilattices, operati

title: Classical negation in logic programs and disjunctive databases
abstract: An important limitation of traditional logic programming as a knowledge representation tool, in comparison with classical logic, is that logic programming does not allow us to deal directly with incomplete information. In order to overcome this limitation, we extend the class of general logic programs by including classical negation, in addition to negation-as-failure. The semantics of such extended programs is based on the method of stable models. The concept of a disjunctive database can be extended in a similar way. We show that some facts of commonsense knowledge can be represented by logic programs and disjunctive databases more easily when classical negation is available. Computationally, classical negation can be eliminated from extended programs by a simple preprocessor. Extended programs are identical to a special case of default theories in the sense of Reiter.

title: Answer Sets for Propositional Theories
abstract: Equilibrium logic, introduced by David Pearce, extends the concept of an answer set from logic programs to arbitrary sets of formulas. Logic programs correspond to the special case in which every formula is a “rule” — an implication that has no implications in the antecedent (body) and consequent (head). The semantics of equilibrium logic looks very different from the usual definitions of an answer set in logic programming, as it is based on Kripke models. In this paper we propose a new definition of equilibrium logic which uses the concept of a reduct, as in the standard definition of an answer set. Second, we apply the generalized concept of an answer set to the problem of defining the semantics of aggregates in answer set programming. We propose, in particular, a semantics for weight constraints that covers the problematic case of negative weights. Our semantics of aggregates is an extension of the approach due to Faber, Leone, and Pfeifer to a language with choice rules and, more generally, arbitrary rules with nested expressions.