Grup de Recerca en Energia i Intel·ligència Artificial (GREiA) (INSPIRES)

Permanent URI for this collection

https://repositori.udl.cat/handle/10459.1/56941

The GREiA research group (Research group in energy and artificial intelligence) is born from the union of the research group in energy GREA and the research group in artificial intelligence IA. The collaboration of these two groups begins in 2014. The general line of research that defines the activity of the group is to provide answers and solutions related to the fields of energy engineering, industrial and construction design, sustainability and intelligence artificial. [Més informació]

Browse

Now showing 1 - 20 of 505

Restricted
The satisfiability problem in regular CNF-formulas
(Springer Verlag, 1998) Manyà Serres, Felip; Béjar Torres, Ramón; Escalada Imaz, G.
In this paper we deal with the propositional satisfiability (SAT) problem for a kind of multiple-valued clausal forms known as regular CNF-formulas and extend some known results from classical logic to this kind of formulas. We present a DavisÐPutnam-style satisfiability checking procedure for regular CNF-formulas equipped with suitable data structures and prove its completeness. Then, we describe a series of experiments for regular random 3-SAT instances. We observe that, for the regular 3-SAT problem with this procedure, there exists a threshold of the ratio of clauses to variables such that (i) the most computationally difficult instances tend to be found near the threshold, (ii) there is a sharp transition from satisfiable to unsatisfiable instances at the threshold and (iii) the value of the threshold increases as the number of truth values considered increases. Instances in the hard part provide benchmarks for the evaluation of regular satisfiability solvers.
Restricted
Extending the Reach of SAT with Many-Valued Logics
(Elsevier, 2001) Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip; Gomes, Carla
We present Regular-SAT, an extension of Boolean Satisfiability based on a class of many-valued CNFform ulas. Regular-SAT shares many properties with Boolean SAT, which allows us to generalize some of the best known SAT results and apply them to Regular-SAT. In addition, Regular-SAT has a number of advantages over Boolean SAT. Most importantly, it produces more compact encodings that capture problem structure more naturally. Furthermore, its simplicity allows us to develop Regular-SAT solvers that are competitive with SAT and CSP procedures. We present a detailed performance analysis of Regular-SAT on several benchmark domains. These results show a clear computational advantage of using a Regular- SAT approach over a pure Boolean SAT or CSP approach, at least on the domains under consideration. We therefore believe that an approach based on Regular-SAT provides a compelling intermediate approach between SAT and CSPs, bringing together some of the best features of each paradigm.
Restricted
Immersion corrosion tests on metal-salt hydrate pairs used for latent heat storage in the 32 to 36 8C temperature range
(Wiley, 2001) Cabeza, Luisa F.; Illa i Alibés, Josep; Roca Enrich, Joan; Badia Pascual, Ferran; Mehling, Harald; Hiebler, Stefan; Ziegler, F.
During the last decades, energy storage has become more and more important. It is required in order to utilize alternative energy sources, which often are available at times when energy is not needed. The main applications of PCMs (Phase Change Materials) in thermal energy storage are when space restrictions limit larger thermal storage units. But widespread use of latent heat stores has not been realized till today due to two main problems: the low heat flux, and the insufficient long term stability of the storage materials and containers. In the present work, we studied this second problem selecting different common metals (aluminum, brass, copper, steel, and stainless steel) and testing their corrosion resistance in contact with salt hydrates that are used as PCMs (zinc nitrate hexahydrate, sodium hydrogen phosphate dodecahydrate, calcium chloride hexahydrate). The method used was the immersion corrosion test. The tests here presented and evaluated were short term. As a consequence of the results from the experiments several pairs can be ruled out. The combinations of zinc nitrate hexahydrate with stainless steel, sodium hydrogen phosphate dodecahydrate with brass, copper and stainless steel, and calcium chloride hexahydrate with brass and copper shared no significant corrosion in the short term and should be studied further.
Restricted
Capturing Structure with Satisfiability
(Springer Verlag, 2001) Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip; Gomes, Carla
We present Regular-SAT, an extension of Boolean Satisfiability basedon a class of many-valuedCNF formulas. Regular-SAT shares many properties with Boolean SAT, which allows us to generalize some of the best known SAT results and apply them to Regular-SAT. In addition, Regular-SAT has a number of advantages over Boolean SAT. Most importantly, it produces more compact encodings that capture problem structure more naturally. Furthermore, its simplicity allows us to develop Regular-SAT solvers that are competitive with SAT andCSP procedures. We present a detailed performance analysis of Regular-SAT on several benchmark domains. These results show a clear computational advantage of using a Regular-SAT approach over a pure Boolean SAT or CSP approach, at least on the domains under consideration. We therefore believe that an approach basedon Regular-SAT provides a compelling intermediate approach between SAT and CSPs, bringing together some of the best features of each paradigm.
Restricted
Towards an Automated Deduction System for First-Order Possibilistic Logic Programming with Fuzzy Constants
(Wiley, 2002) Alsinet, Teresa; Godo i Lacasa, Lluís
In this article, we present a first-order logic programming language for fuzzy reasoning under possibilistic uncertainty and poorly known information. Formulas are represented by a pair (ϕ, α), in which ϕ is a first-order Horn clause or a query with fuzzy constants and regular predicates, and α ∈ [0, 1] is a lower bound on the belief on ϕ in terms of necessity measures. Since fuzzy constants can occur in the logic component of formulas, the truth value of formulas is many-valued instead of Boolean. Moreover, since we have to reason about the possibilistic uncertainty of formulas with fuzzy constants, belief states are modeled by normalized possibility distributions on a set of many-valued interpretations. In this framework, (1) we define a syntax and a semantics of the underlying logic; (2) we give a sound modus ponens-style calculus by derivation based on a semantic unification pattern of fuzzy constants; (3) we develop a directional fuzzy unification algorithm based on the distinction between general and specific object constants; and (4) we describe a backward first-order proof procedure oriented to queries that is based on the calculus of the language and the computation of the unification degree between fuzzy constants in terms of a necessity measure for fuzzy events.
Restricted
Minimal and Redundant SAT Encodings for the All-Interval-Series Problem
(Springer Verlag, 2002) Alsinet, Teresa; Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip
The SAT encodings defined so far for the all-interval-series (ais) problem are very hard for local search but rather easy for systematic algorithms. We define different SAT encodings for the ais problem and provide experimental evidence that this problem can be efficiently solved with local search methods if one chooses a suitable SAT encoding.
Restricted
Heat transfer enhancement in water when used as PCM in thermal energy storage
(Elsevier Science, 2002) Cabeza, Luisa F.; Mehling, Harald; Hiebler, Stefan; Ziegler, F.
Efficient and reliable storage systems for thermal energy are an important requirement in many applications where heat demand and supply or availability do not coincide. Heat and cold stores can basically be divided in two groups. In sensible heat stores the temperature of the storage material is increased significantly. Latent heat stores, on the contrary, use a storage material that undergoes a phase change (PCM) and a small temperature rise is sufficient to store heat or cold. The major advantages of the phase change stores are their large heat storage capacity and their isothermal behavior during the charging and discharging process. However, while unloading a latent heat storage, the solid–liquid interface moves away from the heat transfer surface and the heat flux decreases due to the increasing thermal resistance of the growing layer of the molten/solidified medium. This effect can be reduced using techniques to increase heat transfer. In this paper, three methods to enhance the heat transfer in a cold storage working with water/ice as PCM are compared: addition of stainless steel pieces, copper pieces (both have been proposed before) and a new PCM-graphite composite material. The PCM-graphite composite material showed an increase in heat flux bigger than with any of the other techniques.
Restricted
Improved Branch and Bound Algorithms for Max-2-SAT and Weighted Max-2-SAT
(Springer Verlag, 2003) Planes Cid, Jordi
We developed novel branch and bound algorithms for solving Max-SAT and weighted Max-SAT, which are variants of the algorithm of Borchers & Furman (BFA) [1]. We improved BFA by (i) defining a lower bound of better quality, and (ii) incorporating a new variable selection heuristic.
Restricted
Review on thermal energy storage with phase change: materials, heat transfer analysis and applications
(Elsevier Science, 2003) Zalba, Belén; Marín, José M.; Cabeza, Luisa F.; Mehling, Harald
Thermal energy storage in general, and phase change materials (PCMs) in particular, have been a main topic in research for the last 20 years, but although the information is quantitatively enormous, it is also spread widely in the literature, and difficult to find. In this work, a review has been carried out of the history of thermal energy storage with solid–liquid phase change. Three aspects have been the focus of this review: materials, heat transfer and applications. The paper contains listed over 150 materials used in research as PCMs, and about 45 commercially available PCMs. The paper lists over 230 references.
Restricted
Thermal performance of sodium acetate trihydrate thickened with different materials as phase change energy storage material
(Elsevier, 2003) Cabeza, Luisa F.; Svensson, Gustav; Hiebler, Stefan; Mehling, Harald
The use of phase change materials (PCMs) in energy storage has the advantage of high energy density and isothermal operation. Although the use of only non-segregating PCMs is a good commercial approach, some desirable PCM melting points do not seem attainable with non-segregating salt hydrates at a reasonable price. The addition of gellants and thickeners can avoid segregation of these materials. In this paper, sodium acetate trihydrate is successfully thickened with bentonite and starch. Cellulose gives an even better thickened PCM, but temperatures higher than 65 C give phase separation. The mixtures would show a similar thermal behavior as the salt hydrate, with the same melting point and an enthalpy decrease between 20% and 35%, depending on the type and amount of thickening material used.
Restricted
A Max-SAT Solver with Lazy Data Structures
(Springer Verlag, 2004) Alsinet, Teresa; Manyà Serres, Felip; Planes Cid, Jordi
We present a new branch and bound algorithm for Max-SAT which incorporates original lazy data structures, a new variable selection heuristics and a lower bound of better quality. We provide experimental evidence that our solver outperforms some of the best performing Max- SAT solvers on a wide range of instances.
Restricted
Argument-Based Expansion Operators in Possibilistic Defeasible Logic Programming: Characterization and Logical Properties
(Springer Verlag, 2005) Chesñevar, Carlos Iván; Simari, Guillermo Ricardo; Godo i Lacasa, Lluís; Alsinet, Teresa
Possibilistic Defeasible Logic Programming (P-DeLP) is a logic programming language which combines features from argumentation theory and logic programming, incorporating as well the treatment of possibilistic uncertainty and fuzzy knowledge at object-language level. Defeasible argumentation in general and P-DeLP in particular provide a way of modelling non-monotonic inference. From a logical viewpoint, capturing defeasible inference relationships for modelling argument and warrant is particularly important, as well as the study of their logical properties. This paper analyzes two non-monotonic operators for P-DeLP which model the expansion of a given program P by adding new weighed facts associated with argument conclusions and warranted literals, resp. Different logical properties for the proposed expansion operators are studied and contrasted with a traditional SLD-based Horn logic. We will show that this analysis provides useful comparison criteria that can be extended and applied to other argumentation frameworks
Open Access
Solving Over-Constrained Problems with SAT Technology
(Springer Verlag, 2005) Argelich Romà, Josep; Manyà Serres, Felip
We present a new generic problem solving approach for overconstrained problems based on Max-SAT. We first define a clausal form formalism that deals with blocks of clauses instead of individual clauses, and that allows one to declare each block either as hard (i.e., must be satisfied by any solution) or soft (i.e., can be violated by some solution). We then present two Max-SAT solvers that find a truth assignment that satisfies all the hard blocks of clauses and the maximum number of soft blocks of clauses. Our solvers are branch and bound algorithms equipped with original lazy data structures; the first one incorporates static variable selection heuristics while the second one incorporates dynamic variable selection heuristics. Finally, we present an experimental investigation to assess the performance of our approach on a representative sample of instances (random 2-SAT, Max-CSP, and graph coloring).
Restricted
Modelling Power and Trust for Knowledge Distribution: An Argumentative Approach
(Springer Verlag, 2005) Chesñevar, Carlos Iván; Brena, Ramón F.; Aguirre, José Luis
Knowledge and Information distribution, which is one of the main processes in Knowledge Management, is greatly affected by power explicit relations, as well as by implicit relations like trust. Making decisions about whether to deliver or not a specific piece of information to users on the basis of a rationally justified procedure under potentially conflicting policies for power and trust relations is indeed a challenging problem. In this paper we model power relations, as well as delegation and trust, in terms of an argumentation formalism, in such a way that a dialectical process works as a decision core, which is used in combination with the existing knowledge and an information distribution system. A detailed example is presented and an implementation reported.
Restricted
Improved Exact Solvers for Weighted Max-SAT
(Springer Verlag, 2005) Alsinet, Teresa; Manyà Serres, Felip; Planes Cid, Jordi
We present two new branch and bound weighted Max-SAT solvers (Lazy and Lazy ) which incorporate original data structures and inference rules, and a lower bound of better quality
Restricted
An Argument-Based Framework to Model an Agent’s Beliefs in a Dynamic Environment
(Springer Verlag, 2005) Capobianco, Marcela; Chesñevar, Carlos Iván; Simari, Guillermo Ricardo
One of the most difficult problems in multiagent systems involves representing knowledge and beliefs of agents in dynamic environments. New perceptions modify an agent’s current knowledge about the world, and consequently its beliefs. Such revision and updating process should be performed efficiently by the agent, particularly in the context of real time constraints. This paper introduces an argument-based logic programming language called Observation-based Defeasible Logic Programming (ODeLP). An ODeLP program is used to represent an agent’s knowledge in the context of a multiagent system. The beliefs of the agent are modeled with warranted goals computed on the basis of the agent’s program. New perceptions from the environment result in changes in the agent’s knowledge handled by a simple but effective updating strategy. The process of computing beliefs in a changing environment is made computationally attractive by integrating a “dialectical database” with the agent’s program, providing precompiled information about inferences. We present algorithms for creation and use of dialectical databases.
Restricted
Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers
(Springer Verlag, 2005) Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi
One of the main differences between complete SAT solvers and exact Max-SAT solvers is that the former make an intensive use of unit propagation at each node of the proof tree while the latter, in order to ensure optimality, can only apply unit propagation to a restricted number of nodes. In this paper, we describe a branch and bound MaxSAT solver that applies unit propagation at each node of the proof tree to compute the lower bound instead of applying unit propagation to simplify the formula. The new lower bound captures the lower bound based on inconsistency counts that apply most of the state-of-the-art Max-SAT solvers as well as other improvements, like the start rule, that have been defined to get a lower bound of better quality. Moreover, our solver incorporates the Jeroslow-Wang variable selection heuristic, the pure literal and dominating unit clause rules, and novel preprocessing techniques. The experimental investigation we conducted to compare our solver with the most modern Max-SAT solvers provides experimental evidence that our solver is very competitive.
Open Access
Communication and Computation in Distributed CSP Algorithms
(Springer Verlag, 2005) Fernàndez Camon, César; Béjar Torres, Ramón; Krishnamachari, Bhaskar; Gomes, Carla
We introduce SensorDCSP, a naturally distributed benchmark based on a real-world application that arises in the context of networked distributed systems. In order to study the performance of Distributed CSP (DisCSP) algorithms in a truly distributed setting, we use a discrete-event network simulator, which allows us to model the impact of different network traffic conditions on the performance of the algorithms. We consider two complete DisCSP algorithms: asynchronous backtracking (ABT) and asynchronous weak commitment search (AWC). In our study of different network traffic distributions, we found that, random delays, in some cases combined with a dynamic decentralized restart strategy, can improve the performance of DisCSP algorithms. More interestingly, we also found that the active introduction of message delays by agents can improve performance and robustness, while reducing the overall network load. Finally, our work confirms that AWC performs better than ABT on satisfiable instances. However, on unsatisfiable instances, the performance of AWC is considerably worse than ABT.
Open Access
Statistical Regimes Across Constrainedness Regions
(Springer Verlag, 2005) Gomes, Carla; Fernàndez Camon, César; Selman, Bart; Bessière, Christian
Much progress has been made in terms of boosting the effectiveness of backtrack style search methods. In addition, during the last decade, a much better understanding of problem hardness, typical case complexity, and backtrack search behavior has been obtained. One example of a recent insight into backtrack search concerns so-called heavy-tailed behavior in randomized versions of backtrack search. Such heavy-tails explain the large variance in runtime often observed in practice. However, heavy-tailed behavior does certainly not occur on all instances. This has led to a need for a more precise characterization of when heavy-tailedness does and when it does not occur in backtrack search. In this paper, we provide such a characterization. We identify different statistical regimes of the tail of the runtime distributions of randomized backtrack search methods and show how they are correlated with the Bsophistication^ of the search procedure combined with the inherent hardness of the instances. We also show that the runtime distribution regime is highly correlated with the distribution of the depth of inconsistent subtrees discovered during the search. In particular, we show that an exponential distribution of the depth of inconsistent subtrees combined with a search space that grows exponentially with the depth of the inconsistent subtrees implies heavy-tailed behavior.
Restricted
Computing Dialectical Trees Efficiently in Possibilistic Defeasible Logic Programming
(Springer Verlag, 2005) Chesñevar, Carlos Iván; Simari, Guillermo Ricardo; Godo i Lacasa, Lluís
Possibilistic Defeasible Logic Programming (P-DeLP) is a logic programming language which combines features from argumentation theory and logic programming, incorporating as well the treatment of possibilistic uncertainty and fuzzy knowledge at object-language level. Solving a P-DeLP query Q accounts for performing an exhaustive analysis of arguments and defeaters for Q, resulting in a so-called dialectical tree, usually computed in a depth-first fashion. Computing dialectical trees efficiently in P-DeLP is an important issue, as some dialectical trees may be computationally more expensive than others which lead to equivalent results. In this paper we explore different aspects concerning how to speed up dialectical inference in P-DeLP. We introduce definitions which allow to characterize dialectical trees constructively rather than declaratively, identifying relevant features for pruning the associated search space. The resulting approach can be easily generalized to be applied in other argumentation frameworks based in logic programming.