Search

Finite model reasoning in UML class diagrams is an important task for assessing the quality of the analysis phase in the development of software applications in which it is assumed that the number of objects of the domain is finite. In this paper, we show how to encode finite model reasoning in UML class diagrams as a constraint satisfaction problem (CSP), exploiting techniques developed in description logics. In doing so we set up and solve an intermediate CSP problem to deal with the explosion of 'class combinations' arising in the encoding. To solve the resulting CSP problems we rely on the use of off-the-shelf tools for constraint modeling and programming. As a result, we obtain, to the best of our knowledge, the first implemented system that performs finite model reasoning on UML class diagrams. [ABSTRACT FROM AUTHOR]

Benders decomposition is a well-known procedure for solving a combinatorial optimization problem by defining it in terms of a master problem and a slave problem. Its effectiveness relies, among other factors, on the possibility of synthesizing Benders cuts that rule out not only one, but a large class of trial values for the master problem. In turn, for the class of problems we consider (i.e., optimization plus constraint satisfaction) the possibility of separating the slave problem into several subproblems—i.e., problems exhibiting strong intra-relationships and weak inter-relationships—can be exploited for improving searching procedures efficiency. The notion of separation is typically given informally, or relying on syntactical aspects. This paper formally addresses the notion of slave problem separability by giving a semantic definition and exploring it from the computational point of view. Several examples of separable problems are provided, including some proving that a semantic notion of separability is much more helpful than a syntactic one. We show that separability can be formally characterized as equivalence of logical formulae, and prove the undecidability of the separability check problem. Finally, we show how there are cases where automated tools can still be used for checking subproblem separability. [ABSTRACT FROM AUTHOR]

Quantified constraints and Quantified Boolean Formulae are typically much more difficult to reason with than classical constraints, because quantifier alternation makes the usual notion of solution inappropriate. As a consequence, basic properties of Constraint Satisfaction Problems (CSPs), such as consistency or substitutability, are not completely understood in the quantified case. These properties are important because they are the basis of most of the reasoning methods used to solve classical (existentially quantified) constraints, and it is desirable to benefit from similar reasoning methods in the resolution of quantified constraints. In this article, we show that most of the properties that are used by solvers for CSP can be generalized to quantified CSP. This requires a rethinking of a number of basic concepts; in particular, we propose a notion of outcome that generalizes the classical notion of solution and on which all definitions are based. We propose a systematic study of the relations which hold between these properties, as well as complexity results regarding the decision of these properties. Finally, and since these problems are typically intractable, we generalize the approach used in CSP and propose weaker, easier to check notions based on locality, which allow to detect these properties incompletely but in polynomial time. [ABSTRACT FROM AUTHOR]

Literature on Constraint Satisfaction exhibits the definition of several "structural" properties that can be possessed by CSPs, like (in)consistency, substitutability or interchangeability. Current tools for constraint solving typically detect such properties efficiently by means of incomplete yet effective algorithms, and use them to reduce the search space and boost search. In this paper, we provide a unifying framework encompassing most of the properties known so far, both in CSP and other fields' literature, and shed light on the semantical relationships among them. This gives a unified and comprehensive view of the topic, allows new, unknown, properties to emerge, and clarifies the computational complexity of the various detection problems. In particular, among the others, two new concepts, fixability and removability emerge, that come out to be the ideal characterisations of values that may be safely assigned or removed from a variable's domain, while preserving problem satisfiability. These two notions subsume a large number of known properties, including inconsistency, substitutability and others. Because of the computational intractability of all the property-detection problems, by following the CSP approach we then determine a number of relaxations which provide sufficient conditions for their tractability. In particular, we exploit forms of language restrictions and local reasoning. [ABSTRACT FROM AUTHOR]

The efficiency of systems for constraint programming (CP) is currently highly affected by the actual formulation of the input problem. To this end, several choices have to be made by modelers in order to write efficient specifications and handle instances of realistic size, and this, of course, represents a major obstacle to reach full declarativeness. Several structural properties of problem specifications have been investigated in order to provide techniques that reformulate a constraint program into one which is more efficiently evaluable by the solver at hand. In this paper we consider two such properties, symmetries and functional dependencies among variables, and show that, by characterizing problem specifications as logical formulae, the task of deciding whether such properties hold, and consequently that of performing the relevant reformulations, can be practically mechanized by means of automated theorem proving (ATP) technology. In particular, we report the results on using ATP technology for checking the existence of symmetries, checking whether a given constraint is symmetry-breaking, and checking the existence of functional dependencies in a specification. The output of the reasoning phase is a transformed constraint program, consisting in a reformulated specification and, possibly, a search strategy. We show our techniques on problems such as graph coloring, Sailco inventory, and protein folding. [ABSTRACT FROM AUTHOR]

In this paper, we define and study the k-approximating circuits. A circuit accepting a given set of inputs A is k-approximated by accepting inputs that differ from one of A by at most k bits. We show that the existence of polynomial- size k-approximating circuits depends on the relation between k and the number of inputs. [ABSTRACT FROM AUTHOR]

Examines the complexity of propositional nested circumscription and nested abnormality theories. Significance of circumscription as an important principle for knowledge representation and common-sense reasoning. Necessity of circumscriptive formalism that allows for simple yet elegant modular problem representation which led to the introduction of nested abnormality theories (NAT); Proposition of Lcirc, an extension of generic propositional circumscription by allowing propositional combinations and nesting of circumscriptive theories; Analysis of the complexity of Lcirc and NAT and the effect of nesting; Identification of meaningful syntactic fragments of NAT which have lower complexity; Generalization of the Horn circumscription in NAT framework; Importance of the results in giving insights into the cost of using Lcirc as a host language for expressing formalisms such as action theories, narratives, or spatial theories.

The high computational complexity of advanced reasoning tasks such as reasoning about knowledge and planning calls for efficient and reliable algorithms for reasoning problems harder than NP. In this paper we propose Evaluate, an algorithm for evaluating quantified Boolean formulae (QBFs). Algorithms for evaluation of QBFs are suitable for experimental analysis of problems that belong to a wide range of complexity classes, a property not easily found in other formalisms. Evaluate is a generalization of the Davis–Putnam procedure for SAT and is guaranteed to work in polynomial space. Before presenting the algorithm, we discuss several abstract properties of QBFs that we singled out to make it more efficient. We also discuss various options that were investigated about heuristics and data structures and report the main results of the experimental analysis. In particular, Evaluate is orders of magnitude more efficient than a nested backtracking procedure that resorts to a Davis–Putnam algorithm for handling the innermost set of quantifiers. Moreover, experiments show that randomly generated QBFs exhibit regular patterns such as phase transition and easy-hard-easy distribution. [ABSTRACT FROM AUTHOR]

Propositional greatest lower bounds (GLBs) are logically defined approximations of a knowledge base. They were defined in the context of Knowledge Compilation, a technique developed for addressing high computational cost of logical inference. A GLB allows for polynomial time complete on line reasoning, although soundness is not guaranteed. In this paper we propose new algorithms for the generation of a GLB. Furthermore, we give precise characterization of the computational complexity of the problem of generating such lower bounds, thus addressing in a formal way the question “how many queries are needed to amortize the overhead of compilation?” [ABSTRACT FROM AUTHOR]

Proposes a novel application of Reiter's default logic by introducing a default query language (DQL) for finite relational databases. What application is based on; Effectiveness of DQL for diagnostic reasoning.

Many formalisms for reasoning about knowing commit an agent to be logically omniscient. Logical omniscience is an unrealistic principle for us to use to build a real-world agent, since it commits the agent to knowing infinitely many things. A number of formalizations of knowledge have been developed that do not ascribe logical omniscience to agents. With few exceptions, these approaches are modifications of the “possible-worlds” semantics. In this paper we use a combination of several general techniques for building non-omniscient reasoners. First we provide for the explicit representation of notions such as problems, solutions, and problem solving activities, notions which are usually left implicit in the discussions of autonomous agents. A second technique is to take explicitly into account the notion of resource when we formalize reasoning principles. We use the notion of resource to describe interesting principles of reasoning that are used for ascribing knowledge to agents. For us, resources are abstract objects. We make extensive use of ordering and inaccessibility relations on resources, but we do not find it necessary to define a metric. Using principles about resources without using a metric is one of the strengths of our approach. We describe the architecture of a reasoner, built from a finite number of components, who solves a puzzle, involving reasoning about knowing, by explicitly using the notion of resource. Our approach allows the use of axioms about belief ordinarily used in problem solving – such as axiom K of modal logic – without being forced to attribute logical omniscience to any agent. In particular we address the issue of how we can use resource-unbounded (e.g., logically omniscient) reasoning to attribute knowledge to others without introducing contradictions. We do this by showing how omniscient reasoning can be introduced as a conservative extension over resource-bounded reasoning. [ABSTRACT FROM AUTHOR]

Presents the results of the survey on knowledge compilation of propositional knowledge bases. Discussions on non-monotonic knowledge bases compilation; Approximation of knowledge compilation methods; Difference between the intractable query answering of language restriction and theory approximation.