Anytime clausal reasoning

Given any incomplete clausal propositional reasoner satisfying certain properties, we extend it to a family of increasingly‐complete, sound, and tractable reasoners. Our technique for generating these reasoners is based on restricting the length of the clauses used in chaining (Modus Ponens). Such a family of reasoners constitutes an anytime reasoner, since each propositional theory has a complete reasoner in the family. We provide an alternative characterization, based on a fixed‐point construction, of the reasoners in our anytime families. This fixed‐point characterization is then used to define a transformation of propositional theories into logically equivalent theories for which the base reasoner is complete; such theories are called “vivid”. Developing appropriate notions of vividness and techniques for compiling theories into vivid theories has already generated considerable interest in the KR community. We illustrate our approach by developing an anytime family based on Boolean constraint propagation. This revised version was published online in June 2006 with corrections to the Cover Date.     

Cardinal: A Finite Sets Constraint Solver

In this paper we present Cardinal, a general finite sets constraint solver just made publicly available in ECLiPSe Constraint System, suitable for combinatorial problem solving by exploiting inferences over sets cardinality. In fact, to deal with set variables and set constraints, existing set constraint solvers are not adequate to handle a number of problems, as they do not actively use important information about the cardinality of the sets, a key feature in such problems. Cardinal is formally presented as a set of rewriting rules on a constraint store and we illustrate its efficiency with experimental results. We show the importance of propagating constraints on sets cardinality, by comparing Cardinal with other solvers. Another contribution of this paper is on modelling: we focus essentially on digital circuits problems, for which we present new modelling approaches and prove that sets alone can be used to model these problems in a clean manner and solve them efficiently using Cardinal. Results on a set of diagnostic problems show that Cardinal obtains a speed up of about two orders of magnitude over Conjunto, a previous available set constraint solver, which uses a more limited amount of constraint propagation on cardinalities. Additionally, to further extend modelling capabilities and efficiency, we generalized Cardinal to actively consider constraints over set functions other than cardinality. The Cardinal version just released allows declaring union, minimum and maximum functions on set variables, and easily constraining those functions, letting Cardinal especial inferences efficiently take care of different problems. We describe such extensions and discuss its potentialities, which promise interesting research directions.     

Reference,Synthesis and Constraint Satisfaction*

In this paper we discuss two kinds of constraint satisfaction problems that arise in the context of geometric modelling, In particular in the modification of 2-D wire-frame diagrams that are subject to an arbitrary number of geometrical and topological constraints. We argue that problems in this domain can be classified in two categories that we shall call problems of reference and problems of synthesis. Since Sutherland's Sketchpad program [16], a large number of systems have addressed constraint satisfaction in terms of the representation of constraints sets as equation systems, which in turn are solved by numerical methods like local propagation, relaxation and Gaussian elimination. Here, we present an alternative framework. We argue that conceptualising constraint satisfaction as symbolic rather than “numerical” problems helps to clarify the notion of “constraint”, simplify solution methods, and to explain the intuitive inferential processes underlying the modification of drawings in the course of interactive drafting sessions. The theory presented in this paper has been tested with an experimental computer program called Graflog [5, 8, 9, 10, 11, 12]. The program has been implemented during the last four years, and has evolved through several stages. The current version is implemented in terms of two Unix-processes connected by Unix-pipes. The first is a “C” program running X windows, and handles the external aspects of the interaction. The second is a Prolog program supporting the representational structures and interpreters of the system.     

Compile-time analysis of nonlinear constraints in CLPR

Solving nonlinear constraints over real numbers is a complex problem. Hence constraint logic programming languages like CLPR or Prolog III solve only linear constraints and delay nonlinear constraints until they become linear. This efficient implementation method has the disadvantage that sometimes computed answers are unsatisfiable or infinite loops occur due to the unsatisfiability of delayed nonlinear constraint These problems could be solved by using a more powerful constraint solver which can deal with nonlinear constraints like in RISC-CLP(Real). Since such powerful constraint solvers are not very efficient, we propose a compromise between these two extremes. We characterize a class of CLPR programs for which all delayed nonlinear constraints become linear at run time. Programs belonging to this class can be safely executed with the efficient CLPR method while the remaining programs need a more powerful constraint solver. This paper is an extended and revised version of Ref. 12). The research described in this paper was made during the author’s stay at the Max-planck-Institut für Informatik in Saarbrücken, Germany. It was supported in part by the German Ministry for Research and Technology (BMFT) under grant ITS 9103 and by the ESPRIT Basic Research Working Group 6028 (Construction of Computational Logics). The responsibility for the contents of this publication lies with the author.     

Fast algebraic methods for interval constraint problems

We describe an effective generic method for solving constraint problems, based on Tarski’s relation algebra, using path-consistency as a pruning technique. We investigate the performance of this method on interval constraint problems. Time performance is affected strongly by the path-consistency calculations, which involve the calculation of compositions of relations. We investigate various methods of tuning composition calculations, and also path-consistency computations. Space performance is affected by the branching factor during search. Reducing this branching factor depends on the existence of ‘nice’ subclasses of the constraint domain. Finally, we survey the statistics of consistency properties of interval constraint problems. Problems of up to 500 variables may be solved in expected cubic time. Evidence is presented that the ‘phase transition’ occurs in the range 6 ≤ n.c ≤15, where n is the number of variables, and c is the ratio of non-trivial constraints to possible constraints. This revised version was published online in June 2006 with corrections to the Cover Date.     

High-Order Consistency in Valued Constraint Satisfaction

k-consistency operations in constraint satisfaction problems (CSPs) render constraints more explicit by solving size-k subproblems and projecting the information thus obtained down to low-order constraints. We generalise this notion of k-consistency to valued constraint satisfaction problems (VCSPs) and show that it can be established in polynomial time when penalties lie in a discrete valuation structure.A generic definition of consistency is given which can be tailored to particular applications. As an example, a version of high-order consistency (face consistency) is presented which can be established in low-order polynomial time given certain restrictions on the valuation structure and the form of the constraint graph.     

Capacitated Domination Problem

We consider a generalization of the well-known domination problem on graphs. The (soft) capacitated domination problem with demand constraints is to find a dominating set D of minimum cardinality satisfying both the capacity and demand constraints. The capacity constraint specifies that each vertex has a capacity that it can use to meet the demands of dominated vertices in its closed neighborhood, and the number of copies of each vertex allowed in D is unbounded. The demand constraint specifies the demand of each vertex in V to be met by the capacities of vertices in D dominating it. In this paper, we study the capacitated domination problem on trees from an algorithmic point of view. We present a linear time algorithm for the unsplittable demand model, and a pseudo-polynomial time algorithm for the splittable demand model. In addition, we show that the capacitated domination problem on trees with splittable demand constraints is NP-complete (even for its integer version) and provide a polynomial time approximation scheme (PTAS). We also give a primal-dual approximation algorithm for the weighted capacitated domination problem with splittable demand constraints on general graphs.     

A ρ-calculus of explicit constraint application

Theoretical presentations of the rewriting or ρ-calculus often treat the matching constraint computations as an atomic operation although matching constraints are explicitly expressed. Actual implementations have to take a more realistic view: computations needed in order to find the solutions of a matching equation can have an important impact on the (efficiency of the) calculus for some matching theories and the substitution application usually involves a term traversal. Following the works on explicit substitutions in the λ-calculus, we present two versions of the ρ-calculus, one with explicit matching and one with explicit substitutions, together with a version that combines the two and considers efficiency issues and more precisely the composition of substitutions. The approach is general, allowing for potential extensions to various matching theories. We establish the confluence of the calculus and the termination of the explicit constraint handling and application sub-calculus.     

A Rigorous Global Filtering Algorithm for Quadratic Constraints*

This article introduces a new filtering algorithm for handling systems of quadratic equations and inequations. Such constraints are widely used to model distance relations in numerous application areas ranging from robotics to chemistry. Classical filtering algorithms are based upon local consistencies and thus, are often unable to achieve a significant pruning of the domains of the variables occurring in quadratic constraint systems. The drawback of these approaches comes from the fact that the constraints are handled independently. We introduce here a global filtering algorithm that works on a tight linear relaxation of the quadratic constraints. The Simplex algorithm is then used to narrow the domains. Since most implementations of the Simplex work with floating point numbers and thus, are unsafe, we provide a procedure to generate safe linearizations. We also exploit a procedure provided by Neumaier and Shcherbina to get a safe objective value when calling the Simplex algorithm. With these two procedures, we prevent the Simplex algorithm from removing any solution while filtering linear constraint systems. Experimental results on classical benchmarks show that this new algorithm yields a much more effective pruning of the domains than local consistency filtering algorithms.*This article is an extended version of [23].     

Combinations of <Emphasis Type="Italic">Stit</Emphasis> and Actions

We present a simple theory of actions against the background of branching time, based on which we propose two versions of an extended stit theory, one equipped with particular actions and the other with sets of such actions. After reporting some basic results of a formal development of such a theory, we briefly explore its connection to a version of branching ETL.     

ComR: a combined OWL reasoner for ontology classification

Ontology classification, the problem of computing the subsumption hierarchies for classes (atomic concepts), is a core reasoning service provided by Web Ontology Language (OWL) reasoners. Although general-purpose OWL 2 reasoners employ sophisticated optimizations for classification, they are still not efficient owing to the high complexity of tableau algorithms for expressive ontologies. Profile-specific OWL 2 EL reasoners are efficient; however, they become incomplete even if the ontology contains only a small number of axioms that are outside the OWL 2 EL fragment. In this paper, we present a technique that combines an OWL 2 EL reasoner with an OWL 2 reasoner for ontology classification of expressive SROIQ. To optimize the workload, we propose a task decomposition strategy for identifying the minimal non-EL subontology that contains only necessary axioms to ensure completeness. During the ontology classification, the bulk of the workload is delegated to an efficient OWL 2 EL reasoner and only the minimal non- EL subontology is handled by a less efficient OWL 2 reasoner. The proposed approach is implemented in a prototype ComR and experimental results show that our approach offers a substantial speedup in ontology classification. For the wellknown ontology NCI, the classification time is reduced by 96.9% (resp. 83.7%) compared against the standard reasoner Pellet (resp. the modular reasoner MORe).     

An Efficient Bounds Consistency Algorithm for the Global Cardinality Constraint

Previous studies have demonstrated that designing special purpose constraint propagators can significantly improve the efficiency of a constraint programming approach. In this paper we present an efficient algorithm for bounds consistency propagation of the generalized cardinality constraint (gcc). Using a variety of benchmark and random problems, we show that on some problems our bounds consistency algorithm can dramatically outperform existing state-of-the-art commercial implementations of constraint propagators for the gcc. We also present a new algorithm for domain consistency propagation of the gcc which improves on the worst-case performance of the best previous algorithm for problems that occur often in applications.     

用于离散数学知识检索的本体推理机的获取

通过对当前一些主流本体推理机详细的分析和比较,从系统功能,用户和开发者三个不同角度设计一整套本体推理机测试对比方案,实验证明测试方案是可行和有效的,根据研究结果推荐适用于教学的离散数学知识获取的本体推理机。     

Abstracting soft constraints: Framework, properties, examples

Soft constraints are very flexible and expressive. However, they are also very complex to handle. For this reason, it may be reasonable in several cases to pass to an abstract version of a given soft constraint problem, and then to bring some useful information from the abstract problem to the concrete one. This will hopefully make the search for a solution, or for an optimal solution, of the concrete problem, faster.In this paper we propose an abstraction scheme for soft constraint problems and we study its main properties. We show that processing the abstracted version of a soft constraint problem can help us in finding good approximations of the optimal solutions, or also in obtaining information that can make the subsequent search for the best solution easier.We also show how the abstraction scheme can be used to devise new hybrid algorithms for solving soft constraint problems, and also to import constraint propagation algorithms from the abstract scenario to the concrete one. This may be useful when we don't have any (or any efficient) propagation algorithm in the concrete setting.     

Fast adaptive algorithms for minor component analysis using Householder transformation

In this paper, we propose new adaptive algorithms for the extraction and tracking of the least (minor) or eventually, principal eigenvectors of a positive Hermitian covariance matrix. The main advantage of our proposed algorithms is their low computational complexity and numerical stability even in the minor component analysis case. The proposed algorithms are considered fast in the sense that their computational cost is O(np) flops per iteration where n is the size of the observation vector and p<n is the number of eigenvectors to estimate.We consider OJA-type minor component algorithms based on the constraint and non-constraint stochastic gradient technique. Using appropriate fast orthogonalization procedures, we introduce new fast algorithms that extract the minor (or principal) eigenvectors and guarantee good numerical stability as well as the orthogonality of their weight matrix at each iteration. In order to have a faster convergence rate, we propose a normalized version of these algorithms by seeking the optimal step-size. Our algorithms behave similarly or even better than other existing algorithms of higher complexity as illustrated by our simulation results.     

An MDD-based generalized arc consistency algorithm for positive and negative table constraints and some global constraints

A table constraint is explicitly represented as its set of solutions or non-solutions. This ad hoc (or extensional) representation may require space exponential to the arity of the constraint, making enforcing GAC expensive. In this paper, we address the space and time inefficiencies simultaneously by presenting the mddc constraint. mddc is a global constraint that represents its (non-)solutions with a multi-valued decision diagram (MDD). The MDD-based representation has the advantage that it can be exponentially smaller than a table. The associated GAC algorithm (called mddc) has time complexity linear to the size of the MDD, and achieves full incrementality in constant time. In addition, we show how to convert a positive or negative table constraint into an mddc constraint in time linear to the size of the table. Our experiments on structured problems, car sequencing and still-life, show that mddc is also a fast GAC algorithm for some global constraints such as sequence and regular. We also show that mddc is faster than the state-of-the-art generic GAC algorithms in Gent et al. (2007), Lecoutre and Szymanek (2006), Lhomme and Régin (2005) for table constraint.     

Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers

This paper describes a method for combining “off-the-shelf” SAT and constraint solvers for building an efficient Satisfiability Modulo Theories (SMT) solver for a wide range of theories. Our method follows the abstraction/refinement approach to simplify the implementation of custom SMT solvers. The expected performance penalty by not using an interweaved combination of SAT and theory solvers is reduced by generalising a Boolean solution of an SMT problem first via assigning don’t care to as many variables as possible. We then use the generalised solution to determine a thereby smaller constraint set to be handed over to the constraint solver for a background theory. We show that for many benchmarks and real-world problems, this optimisation results in considerably smaller and less complex constraint problems. The presented approach is particularly useful for assembling a practically viable SMT solver quickly, when neither a suitable SMT solver nor a corresponding incremental theory solver is available. We have implemented our approach in the ABsolver framework and applied the resulting solver successfully to an industrial case-study: the verification problems arising in verifying an electronic car steering control system impose non-linear arithmetic constraints, which do not fall into the domain of any other available solver.