Search

Propositional satisfiability solving (SAT) has been one of the most successful automated reasoning methods in the last decade in computer science by solving a wide range of both industrial and academic problems. One of the most widely used constraint during the process of translating a practical problem into a SAT instance is the at-most-one (AMO) constraint. Many studies on SAT encodings of the AMO constraint have been reported in the literature, however thorough comparisons of these encodings are largely missing. This paper not only provide such comparisons, but also discusses the similarity of the SAT encodings of the AMO constraint and SAT encodings of more general CSPs. More specifically, the paper empirically evaluates the most well-known AMO encodings on three state-of-the-art SAT solvers of a number of benchmarks and provides some guidelines for efficient SAT encodings of the AMO constraint leading.

The probabilistic continuous constraint framework complements the representation of uncertainty by means of intervals with a probabilistic distribution of values within such intervals. This paper describes how nonlinear inverse problems can be cast into this framework, highlighting its ability to deal with all the uncertainty aspects of such problems. In previous work we have formalized the framework, relying on simplified integration methods to characterize the uncertainty distributions. In this paper we (1) provide validated constraint-based algorithms to compute these distributions, (2) discuss approximations obtained by their hybridization with Monte-Carlo methods, and (3) obtain a better uncertainty characterization, by including methods to compute expected values and standard deviations. The paper illustrates this new methodology in Ocean Color (OC), a research area which is widely used in climate change studies and has potential applications in water quality monitoring. OC semi-analytical approaches rely on forward models that relate optically active seawater compounds (OC products) to remote sensing measurements of the sea-surface reflectance. OC products are derived by inverting the forward model on a spectral-reflectance basis. Based on a set of preliminary experiments we show that the probabilistic constraint framework is able to provide a valuable characterization of the uncertainty of all scenarios consistent with the model and the measurements. Moreover, the framework can be used to derive how measurements accuracy affects the uncertainty distribution of the retrieved OC products, which may constitute an important contribution to the OC community.

In this paper we propose PSICO (Processing Structural Information with Constraint programming and Optimisation) as a constraint-based approach to determining protein structures compatible with distance constraints obtained from Nuclear Magnetic Resonance (NMR) data. We compare the performance of our proposed algorithm with DYANA (“Dynamics algorithm for NMR applications”) an existing commercial application based on simulated annealing. On a test case with experimental data on the dimeric protein Desulforedoxin, the method proposed here supplied similar results in less than 10 minutes compared to approximately 10 hours of computation time for DYANA. Although the quality of results can still be improved, this shows that CP technology can greatly reduce computation time, a major advantage because structural NMR technique generally demands multiple runs of structural computation.

The probabilistic continuous constraint (PC) framework complements the representation of uncertainty by means of intervals with a probabilistic distribution of values within such intervals. This paper, published in Constraints [8], describes how nonlinear inverse problems can be cast into this framework, highlighting its ability to deal with all the uncertainty aspects of such problems, and illustrates this new methodology in Ocean Color (OC), a research area widely used in climate change studies with significant applications in water quality monitoring.

Constraints that may be obtained by composition from simpler constraints are present, in some way or another, in almost every constraint program. The decomposition of such constraints is a standard technique for obtaining an adequate propagation algorithm from a combination of propagators designed for simpler constraints. The decomposition approach is appealing in several ways. Firstly because creating a specific propagator for every constraint is clearly infeasible since the number of constraints is infinite. Secondly, because designing a propagation algorithm for complex constraints can be very challenging. Finally, reusing existing propagators allows to reduce the size of code to be developed and maintained. Traditionally, constraint solvers automatically decompose constraints into simpler ones using additional auxiliary variables and propagators, or expect the users to perform such decomposition themselves, eventually leading to the same propagation model. In this paper we explore views, an alternative way to create efficient propagators for such constraints in a modular, simple and correct way, which avoids the introduction of auxiliary variables and propagators., The final publication is available at link.springer.com

Continuous constraint programming has been widely used to model safe reasoning in applications where uncertainty arises. Constraint propagation propagates intervals of uncertainty among the variables of the problem, eliminating values that do not belong to any solution. However, to play safe, these intervals may be very wide and lead to poor propagation. We proposed a probabilistic continuous constraint framework that associates a probabilistic space to the variables of the problem, allowing to distinguish between different scenarios, based on their likelihoods. In this paper we discuss the capabilities of the framework for decision support in nonlinear continuous problems with uncertain information. Its applicability is illustrated in inverse and reliability problems, which are two different types of problems representative of the kind of reasoning required by the decision makers.

RNA secondary structure prediction depends on context. When only a few (sometimes putative) RNA homologs are available, one of the most famous approach is based on a set of recursions proposed by Sankoff in 1985. Although this modus operandi insures an algorithmically optimal result, the main drawback lies in its prohibitive time and space complexities. A series of heuristics were developed to face that difficulty and turn the recursions usable. In front of the inescapable intricacy of the question when handling the full thermodynamic model, we come back in the present paper to a biologically simplified model that helps focusing on the algorithmic issues we want to overcome. We expose our ongoing developments by using the constraints framework which we believe is a powerful paradigm for heuristic design. We give evidence that the main heuristics proposed by others (structural and alignment banding, multi-loop restriction) can be refined in order to produce a substantial gain both in time computation and space requirements. A beta implementation of our approach, that we named ARNICA, exemplify that gain on a sample set that remains unaffordable to other methods. The sources and sample tests of ARNICA are available at http://centria.di.fct.unl.pt/~op/arnica.tar.gz

Constraint programming has been used in many applications where uncertainty arises to model safe reasoning. The goal of constraint propagation is to propagate intervals of uncertainty among the variables of the problem, thus only eliminating values that assuredly do not belong to any solution. However, to play safe, these intervals may be very wide and lead to poor propagation. In this paper we present a framework for probabilistic constraint solving that assumes that uncertain values are not all equally likely. Hence, in addition to initial intervals, a priori probability distributions (within these intervals) are defined and propagated through the constraints. This provides a posteriori conditional probabilities for the variables values, thus enabling the user to select the most likely scenarios.

Recently proposed impact based heuristics have been shown to outperform other instances of the first-fail policy such as the common dom and dom/deg heuristics. This paper compares the behaviour of a constraint and a variable centered impact based heuristic and relates it to the amount of constraint propagation inherent to the model of the problem. Additionally, it presents results which suggest that a lookahead impact heuristic we recently proposed might be the best choice for problems with low locality and where constraint propagation plays an important role.

The authors previous work on probabilistic constraint reasoning assumes the uncertainty of numerical variables within given bounds, characterized by a priori probability distributions. It propagates such knowledge through a network of constraints, reducing the uncertainty and providing a posteriori probability distributions. An inverse problem aims at estimating parameters from observed data, based on some underlying theory about a system behavior. This paper describes how nonlinear inverse problems can be cast into the probabilistic constraint framework, highlighting its ability to deal with all the uncertainty aspects of such problems.

The efficiency of complete solvers depends both on constraint propagation to narrow the domains and some form of complete search. Whereas constraint propagators should achieve a good trade-off between their complexity and the pruning that is obtained, search heuristics take decisions based on information about the state of the problem being solved. In general, these two components are independent and are indeed considered separately. A recent family of algorithms have been proposed to achieve a strong form of consistency called Singleton Consistency (SC). These algorithms perform a limited amount of search and propagation (lookahead) to remove inconsistent values from the variables domains, making SC costly to maintain. This paper follows from the observation that search states being explored while enforcing SC are an important source of information about the future search space which is being ignored. In this paper we discuss the integration of this look-ahead information into variable and value selection heuristics, and show that significant speedups are obtained in a number of standard benchmark problems.

Although propagation techniques are very important to solve constraint solving problems, heuristics are still necessary to handle non trivial problems efficiently. General principles may be defined for such heuristics (e.g. first-fail and best-promise), but problems arise in their implementation except for some limited sources of information (e.g. cardinality of variables domain). Other possibly relevant features are ignored due to the difficulty in understanding their interaction and a convenient way of integrating them. In this paper we illustrate such difficulties in a specific problem, determination of protein structure from Nuclear Magnetic Resonance (NMR) data. We show that machine learning techniques can be used to define better heuristics than the use of heuristics based on single features, or even than their combination in simple form (e.g majority vote). The technique is quite general and, with the necessary adaptations, may be applied to many other constraint satisfaction problems.

This paper addresses constraint solving over continuous domains in the context of decision making, and discusses the trade-off between precision in the definition of the solution space and the computational efforts required. In alternative to local consistency, we propose maintaining global hull-consistency and present experimental results that show that this may be an appropriate alternative to other higher order consistencies. We tested various global hull enforcing algorithms and the best results were obtained with the integration of a local search procedure within interval constraint propagation.

System dynamics is often modeled by means of parametric differential equations. Despite their expressive power, they are difficult to reason about and make safe decisions, given their non-linearity and the important effects that the uncertainty on data may cause. Either by traditional numerical simulation or relying on constraint based methods, it is difficult to express a number of constraints on the solution functions (for which there are usually no analytical solutions) and these constraints may only be handled passively, with generate and test techniques. In contrast, the framework we propose not only extends the declarativeness of the constraint based approach but also makes an active use of constraints on the solution functions, which makes it particularly suited for a number of decision making problems, such as those arising in the biomedical applications presented in the paper.

Knowledge representation has always been a major problem in the design of medical decision support systems. In this paper we present a new methodology to represent and reason about medical knowledge, based on the declarative specification of interval constraints over the medical concepts. This allows the integration of deep medical models involving differential equations developed in biomedical research (typical in several medical domains) which, due to their complexity, have not been incorporated into medical decision support systems. The methodology which enables reasoning both forward and backward in time, is applied to a specific domain, electromyography. The promising results obtained are discussed to justify our future work.

Model-based decision support systems rely on an explicit representation of some system whose dynamics is often qualitatively described by specifying the rates at which the system variables change. Such models are naturally represented as a set of ordinary differential equations (ODEs) which are parametric (they include parameters whose value is not known exactly). If safe decisions are to be made based on the values of these parameters, it is important to know them with sufficient precision.

In this paper, we propose a constraint-based approach to determining protein structures compatible with distance constraints obtained from Nuclear Magnetic Resonance (NMR) data. We compare the performance of our proposed algorithm with DYANA (“Dynamics algorithm for NMR applications” [1]) an existing commercial application based on simulated annealing. For our test case, computation time for DYANA was more than six hours, whereas the method we propose produced similar results in 8 minutes, so we show that the application of Constraint Programming (CP) technology can greatly reduce computation time. This is a major advantage because this NMR technique generally demands multiple runs of structural computation.

This paper extends a constraint solver over the booleans to make it defeasible, and embeddable in a general architecture for defeasible constraint solving. This complements previous work on defeasible solvers over finite domains and rational numbers. Similar to the latter, one approach uses witness variables to detect minimal conflict sets of constraints, but adds important overhead. Other approaches use data dependencies, as in finite domains, to detect conflict sets. Although these are not minimal, such approaches seem more promising due to their less complexity.

Objective. In a faulty digital circuit, many (single) faulty gates may explain the observed findings. It may be not practical (e.g. in VLSI chips) to test points in the circuit other than their input and output bits, so constraint technology was used to obtain input patterns that identify single faulty gates. However, two alternative faulty gates often have a large number of test patterns, but only a few, if any, differentiate them. We focus on obtaining test patterns that discriminate alternative faulty gates. Technique. The technique of [2] to generate a test pattern for a faulty gate introduces new values, d and notd, and assigns d to the gate output. New truth tables cope with the new values, and the patterns generated force a d (or notd) to reach an output bit

This paper presents a defeasible constraint solver for the domain of linear equations, disequations and inequalities over the body of rational/real numbers. As extra requirements resulting from the incorporation of the solver into an Incremental Hierarchical Constraint Solver (IHCS) scenario we identified: a)the ability to refer to individual constraints by a label, b) the ability to report the (minimal) cause for the unsatisfiability of a set of constraints, and c) the ability to undo the effects of a formerly activated constraint. We develop the new functionalities after starting the presentation with a general architecture for defeasible constraint solving, through a solved form algorithm that utilizes a generalized, incremental variant of the Simplex algorithm, where the domain of a variable can be restricted to an arbitrary interval. We demonstrate how generalized slacks form the basis for the computation of explanations regarding the cause of unsatisfiability and/or entailment in terms of the constraints told, and the possible deactivation of constraints as demanded by the hierarchy handler.