Explaining the <Literal>cumulative</Literal> propagator

The global cumulative constraint was proposed for modelling cumulative resources in scheduling problems for finite domain (FD) propagation. Since that time a great deal of research has investigated new stronger and faster filtering techniques for cumulative, but still most of these techniques only pay off in limited cases or are not scalable. Recently, the “lazy clause generation” hybrid solving approach has been devised which allows a finite domain propagation engine possible to take advantage of advanced SAT technology, by “lazily” creating a SAT model of an FD problem as computation progresses. This allows the solver to make use of SAT explanation and autonomous search capabilities. In this article we show how, once we use lazy clause generation, modelling the cumulative constraint by decomposition creates a highly competitive version of cumulative. Using decomposition into component parts automatically makes the propagator incremental and able to explain itself. We then show how, using the insights from the behaviour of the decomposition, we can create global cumulative constraints that explain their propagation. We compare these approaches to explaining the cumulative constraint on resource constrained project scheduling problems. All our methods are able to close a substantial number of open problems from the well-established PSPlib benchmark library of resource-constrained project scheduling problems.     

Extending Sledgehammer with SMT Solvers

Sledgehammer is a component of Isabelle/HOL that employs resolution-based first-order automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically selects relevant facts and, if an ATP is successful, produces a snippet that replays the proof in Isabelle. We extended Sledgehammer to invoke satisfiability modulo theories (SMT) solvers as well, exploiting its relevance filter and parallel architecture. The ATPs and SMT solvers nicely complement each other, and Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs’ reach.     

Improved usability and performance of SMT solvers for debugging specifications

It is now common to construct an extended static checker or software verification system using an SMT theorem prover as the underlying logical verifier. SMT provers have improved significantly in performance over the last several years. However, their usability as a component of software checking and verification systems still has gaps. This paper describes investigations in two areas: the reporting of counterexample information and the testing of vacuity, both of which are important to realistic use of such tools for typical software development. The use of solvers in verification is more effective if the solvers support minimal unsatisfiable cores and incremental construction, evolution and querying of satisfying assignments; current solvers only partially support these capabilities.     

Linear constraint equations for continuous support conditions in finite element analysis

Discretised structural models such as by finite elements imply discretised support conditions. In some cases such as plates on elastic foundation or slabs on large interacting columns an improved formulation of the continuous support conditions is desirable. This can be achieved by means of linear constraint equations. The numerical treatment of linear constraints is discussed for the method of elimination of variables as well as for the method of Lagrange multipliers. Then specific constraint equations for different accuracy requirements are derived, which can be used to constrain rectangular flat shell elements of arbitrary shape functions. These constraints introduce six generalized displacements according to the rigid body motions of the element and transmit the corresponding generalized reactions on the nodal degrees of freedom in a way consistent with distributed reactions. The effect on the strain energy of a square shell element is shown for the different constraint equations. As an application, the linear constraints are used to represent the continuous interaction of columns with the plate in a flat slab structure. Comparison of the finite element solutions with analytical results shows that the derived constraint equations allow a considerably improved formulation of continuous support conditions.     

Extending constraint logic programming for temporal reasoning

In recent years, several constraint‐based temporal reasoning frameworks have been proposed. They consider temporal points or intervals as domain elements linked by temporal constraints. Temporal reasoning in these systems is based on constraint propagation. In this paper, we argue that a language based on constraint propagation can be a suitable tool for expressing and reasoning about temporal problems. We concentrate on Constraint Logic Programming (CLP) which is a powerful programming paradigm combining the advantages of Logic Programming and the efficiency of constraint solving. However, CLP presents some limitations in dealing with temporal reasoning. First, it uses an “arc consistency” propagation algorithm which is embedded in the inference engine, cannot be changed by the user, and is too weak in many temporal frameworks. Second, CLP is not able to deal with qualitative temporal constraints. We present a general meta CLP architecture which maintains the advantages of CLP, but overcomes these two main limitations. Each architectural level is a finite domain constraint solver(CLP(FD)) that reasons about constraints of the underlying level. Based on this conceptual architecture, we extend the CLP(FD)language and we specialize the extension proposed on Vilain and Kautz’sPoint Algebra, on Allen’s Interval Algebra and on the STP framework by Dechter, Meiri and Pearl. In particular, we show that we can cope effectively with disjunctive constraints even in an interval‐based framework. This revised version was published online in June 2006 with corrections to the Cover Date.     

Engineering constraint solvers for automatic analysis of probabilistic hybrid automata

In this article, we recall different approaches to the constraint-based, symbolic analysis of hybrid discrete-continuous systems and combine them to a technology able to address hybrid systems exhibiting both non-deterministic and probabilistic behavior akin to infinite-state Markov decision processes. To enable mechanized analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theories (SMT) solving by, first, reasoning over ordinary differential equations (ODEs) and, second, a comprehensive treatment of randomized (also known as stochastic) quantification over discrete variables as well as existential quantification over both discrete and continuous variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a constraint-based analysis of dense-time probabilistic hybrid automata, extending previous results addressing discrete-time automata [33]. Generalizing SMT-based bounded model-checking of hybrid automata [5], [31], stochastic SMT including ODEs permits the direct analysis of probabilistic bounded reachability problems of dense-time probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.     

Studies on two concurrent solvers for finite element analysis

This paper describes a study carried out on the development and implementation of two parallel equation solvers for static finite element analysis. The two direct solvers, one for banded storage and the other for skyline profile storage, are implemented on a tightly coupled shared memory system. Certain key issues like (algorithmic) portability across different parallel architectures, matrix sparsity and vectorisation have been kept in mind while designing the algorithms. Performance studies have been conducted by varying the number of processors and the size of the problem. The results indicate that higher efficiencies can be obtained with both the algorithms described in this paper. However, one has to obtained with both the algorithms described in this paper. However, one has to choose the appropriate solver based on the concurrent approach chosen for paralleling the finite element code. The pseudo-codes, the concurrent implementation of the two solvers, both for shared and message passing systems are presented.     

Neural networks for finite constraint satisfaction

Constraint Satisfaction Problems (CSPs) are in general NP-hard, and a general deterministic polynomial time algorithm is not known. They play a central role in real-life problems. The satisfaction of a Conjunctive Normal Form (CNF-SAT)is the core of any CSP. We present a new modelisation technique for any CSP with finite variable domains, and, in particular, for solving CNF-SAT. The knowledge representation is based on two fundamental types of constraint: the choice constraint, and the exclusion constraint. These models are then implemented by means of several different neural networks, some based on backpropagation learning and others on different procedures. All these networks are trained through a supervised procedure, and learn to efficiently solve CNF-SAT. The results of significant tests are described: they show that some networks can effectively solve the proposed problems.     

Three generalizations of the <Emphasis Type="SmallCaps">FOCUS</Emphasis> constraint

The FOCUS constraint expresses the notion that solutions are concentrated. In practice, this constraint suffers from the rigidity of its semantics. To tackle this issue, we propose three generalizations of the FOCUS constraint. We provide for each one a complete filtering algorithm. Moreover, we propose ILP and CSP decompositions.     

On Supersymmetric M-brane configurations with an R<Stack><Subscript>*</Subscript><Superscript>1,1</Superscript></Stack> /Z<Subscript>2</Subscript> submanifold

We obtain new examples of partly supersymmetric M-brane solutions defined on products of Ricci-flat manifolds, which contain a two-dimensional Lorentzian submanifold R _* ^1,1 /Z ₂ with one parallel spinor. The examples belong to the following configurations: M2, M5, M2 ∩M5 and M5 ∩M5. Among them, an M2 solution with N = 1/32 fractional number of preserved supersymmetries is presented.     

Stability in the domain of nonlinear difference inclusions<Superscript>1</Superscript>

The problem of establishing the sufficient conditions for robust stability in a given domain is considered for the class of nonlinear discrete systems described by a difference inclusion. The nonlinear function of the system cannot be represented in a quasilinear form, and only nonlinear constraints are specified for its values. Examples of constructive testing of the sufficient stability conditions are presented.     

An Augmented Lagrangian Method for <Emphasis Type=Italic>TV</Emphasis><Subscript><Emphasis Type=Italic>g</Emphasis></Subscript>+<Emphasis Type=Italic>L</Emphasis><Superscript>1</Superscript>-norm Minimization

In this paper, the minimization of a weighted total variation regularization term (denoted TV _g ) with L ¹ norm as the data fidelity term is addressed using the Uzawa block relaxation method. The unconstrained minimization problem is transformed into a saddle-point problem by introducing a suitable auxiliary unknown. Applying a Uzawa block relaxation method to the corresponding augmented Lagrangian functional, we obtain a new numerical algorithm in which the main unknown is computed using Chambolle projection algorithm. The auxiliary unknown is computed explicitly. Numerical experiments show the availability of our algorithm for salt and pepper noise removal or shape retrieval and also its robustness against the choice of the penalty parameter. This last property is useful to attain the convergence in a reduced number of iterations leading to efficient numerical schemes. The specific role of the function g in TV _g is also investigated and we highlight the fact that an appropriate choice leads to a significant improvement of the denoising results. Using this property, we propose a whole algorithm for salt and pepper noise removal (denoted UBR-EDGE) that is able to handle high noise levels at a low computational cost. Shape retrieval and geometric filtering are also investigated by taking into account the geometric properties of the model.     

Iterative solvers by substructuring for the p-version finite element method

We study a class of substructuring methods well-suited for iterative solution of large systems of linear equations arising from the p-version finite element method. The p-version offers a natural decomposition with every element treated as a substructure. We use the preconditioned conjugate gradient method with preconditioning constructed by a decomposition of the local function space on each element. We develop an elementary theory giving bounds on the condition numbers which do not depend on the number of elements if a sparse system with only few variables per element is solved in each iteration. This bound can be evaluated considering one element at a time and we compute such condition numbers numerically for various elements.     

The finite horizon investor problem with a budget constraint

We study a model that incorporates a budget constraint in a decision making problem. Our goal is to maximize the expected wealth, where in each time period we can either stop the business getting our current wealth or to continue one additional time period and getting a random revenue. We show that when the wealth is scalar, the problem is NP-hard and we provide an FPTAS. However, when the wealth is vector with at least two components the problem cannot be approximated.     

Mining <Emphasis Type=Italic>top-k</Emphasis> frequent patterns in the presence of the memory constraint

We explore in this paper a practicably interesting mining task to retrieve top-k (closed) itemsets in the presence of the memory constraint. Specifically, as opposed to most previous works that concentrate on improving the mining efficiency or on reducing the memory size by best effort, we first attempt to specify the available upper memory size that can be utilized by mining frequent itemsets. To comply with the upper bound of the memory consumption, two efficient algorithms, called MTK and MTK_Close, are devised for mining frequent itemsets and closed itemsets, respectively, without specifying the subtle minimum support. Instead, users only need to give a more human-understandable parameter, namely the desired number of frequent (closed) itemsets k. In practice, it is quite challenging to constrain the memory consumption while also efficiently retrieving top-k itemsets. To effectively achieve this, MTK and MTK_Close are devised as level-wise search algorithms, where the number of candidates being generated-and-tested in each database scan will be limited. A novel search approach, called δ-stair search, is utilized in MTK and MTK_Close to effectively assign the available memory for testing candidate itemsets with various itemset-lengths, which leads to a small number of required database scans. As demonstrated in the empirical study on real data and synthetic data, instead of only providing the flexibility of striking a compromise between the execution efficiency and the memory consumption, MTK and MTK_Close can both achieve high efficiency and have a constrained memory bound, showing the prominent advantage to be practical algorithms of mining frequent patterns.     

Sparse Support Vector Machine with <Emphasis Type="Italic">L</Emphasis><Subscript><Emphasis Type="Italic">p</Emphasis></Subscript> Penalty for Feature Selection

We study the strategies in feature selection with sparse support vector machine (SVM). Recently, the socalled L _p -SVM (0 < p < 1) has attracted much attention because it can encourage better sparsity than the widely used L ₁-SVM. However, L _p -SVM is a non-convex and non-Lipschitz optimization problem. Solving this problem numerically is challenging. In this paper, we reformulate the L _p -SVM into an optimization model with linear objective function and smooth constraints (LOSC-SVM) so that it can be solved by numerical methods for smooth constrained optimization. Our numerical experiments on artificial datasets show that LOSC-SVM (0 < p < 1) can improve the classification performance in both feature selection and classification by choosing a suitable parameter p. We also apply it to some real-life datasets and experimental results show that it is superior to L ₁-SVM.     

Efficient Algorithms for Integer Programs with Two Variables per Constraint<Superscript><Emphasis Type="Italic">1</Emphasis></Superscript>

Given a bounded integer program with n variables and m constraints, each with two variables, we present an O(mU) time and O(m) space feasibility algorithm, where U is the maximal variable range size. We show that with the same complexity we can find an optimal solution for the positively weighted minimization problem for monotone systems. Using the local-ratio technique we develop an O(nmU) time and O(m) space 2 -approximation algorithm for the positively weighted minimization problem for the general case. We further generalize all results to nonlinear constraints (called axis-convex constraints ) and to nonlinear (but monotone) weight functions. Our algorithms are not only better in complexity than other known algorithms, but also considerably simpler, and they contribute to the understanding of these very fundamental problems. Received June 21, 1996; revised December 5, 1997.     

Extending object-oriented languages with backward error recovery integrated support

One of the requirements of software robustness is controlling and managing runtime errors that might arise at certain points of application execution. In most object-oriented programming languages, this requirement is commonly implemented by means of exception handling. Although exception handling is a powerful tool to avoid system failure arising, there are still many situations where it is not sufficient to restore the system to a consistent state. Exception handling allows the developer to detect and locate errors, but it gives no information or tools to cover the error recovering task. Therefore, we propose an extension of the semantics of common object-oriented languages to restore the previous consistent state of the system in the presence of runtime errors, avoiding some of the tasks that exception-handling mechanisms delegate to developers. Our proposed solution is centered in the concept of “reconstructor”, a declarative component oriented to automatically return the system to its last stable state. Based on this concept, we develop a non-intrusive code enrichment tool for Java, and we apply it to a real application in order to check the feasibility of the proposal. We evaluated the performance of the resulting code, obtaining reasonable and viable rates and overload.     

Localized tensor-based solvers for interactive finite element applications using C++ and Java

This paper presents techniques for solving systems of equations arising in finite element applications using a localized, tensor-based approach. The approach is localized in that a major part of the solution responsibility is delegated to vector degree-of-freedom objects, rather than residing solely in a global solver working on a monolithic data structure. The approach is tensor-based in that the fundamental quantities used for computation are considered to be second-order tensors. The localized data structure strategy provides the benefits of an efficient sparse and symmetric storage scheme without requiring complex implementation code. The tensor-based aspect of the approach can bring substantial performance benefits by increasing the granularity at which solution algorithms deal with their data. Java and C++ implementations of interactive finite element programs are used to demonstrate performance that is competitive with other available solvers, especially in the case of problems for which interactive analysis is feasible on commonly available hardware.