The Artificial Intelligence Research Group of the University of Lleida is formed by members of the Department of Computer Science. The current research of the group focus on the following areas: Argumentation: logical formalizations, technological applications, and integration with fuzzy logic programming languages. Constraint Programming: modelling, practical complexity, distributed CSP, weighted CSP, and connections with satisfiability. Fuzzy logic programming: integration of logic propramming languages and fuzzy logics and formalisms for treatment of uncertainty, such as possibilistic logic. Many-valued logics: logical calculi for signed CNF formula, complexity, automated theorem proving. Satisfiability: design, analysis, implementation and evaluation of algorithms for solving SAT, Max-SAT and QBF for both Boolean and Many-Valued CNF formulas, efficient encodings, logical calculi, tractable problems, phase transitions, local search, learning. [Més informació]

Recent Submissions

  • Argument-Based Expansion Operators in Possibilistic Defeasible Logic Programming: Characterization and Logical Properties 

    Chesñevar, Carlos Iván; Simari, Guillermo Ricardo; Godo i Lacasa, Lluís; Alsinet, Teresa (Springer Verlag, 2005)
    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 ...
  • Modelling Power and Trust for Knowledge Distribution: An Argumentative Approach 

    Chesñevar, Carlos Iván; Brena, Ramón F.; Aguirre, José Luis (Springer Verlag, 2005)
    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 ...
  • Computing Dialectical Trees Efficiently in Possibilistic Defeasible Logic Programming 

    Chesñevar, Carlos Iván; Simari, Guillermo Ricardo; Godo i Lacasa, Lluís (Springer Verlag, 2005)
    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 ...
  • Statistical Regimes Across Constrainedness Regions 

    Gomes, Carla; Fernàndez Camon, César; Selman, Bart; Bessière, Christian (Springer Verlag, 2005)
    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 ...
  • Knowledge Distribution in Large Organizations Using Defeasible Logic Programming 

    Chesñevar, Carlos Iván; Brena, Ramón F.; Aguirre, José L. (Springer Verlag, 2005)
    Distributing pieces of knowledge in large, usually distributed organizations is a central problem in Knowledge and Organization Management. Policies for distributing knowledge and information are very often incomplete, ...
  • An Argument-Based Framework to Model an Agent’s Beliefs in a Dynamic Environment 

    Capobianco, Marcela; Chesñevar, Carlos Iván; Simari, Guillermo Ricardo (Springer Verlag, 2005)
    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 ...
  • Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers 

    Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Springer Verlag, 2005)
    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, ...
  • Improved Exact Solvers for Weighted Max-SAT 

    Alsinet, Teresa; Manyà Serres, Felip; Planes Cid, Jordi (Springer Verlag, 2005)
    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
  • Communication and Computation in Distributed CSP Algorithms 

    Fernàndez Camon, César; Béjar Torres, Ramón; Krishnamachari, Bhaskar; Gomes, Carla (Springer Verlag, 2005)
    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) ...
  • Sensor networks and distributed CSP: communication, computation and complexity 

    Béjar Torres, Ramon; Domshlak, Carmel; Fernàndez Camon, César; Gomes, Carla; Krishnamachari, Bhaskar; Selman, Bart; Valls Marsal, Magda (Elsevier, 2005)
    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) ...
  • A Max-SAT Solver with Lazy Data Structures 

    Alsinet, Teresa; Manyà Serres, Felip; Planes Cid, Jordi (Springer Verlag, 2004)
    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 ...
  • New Inference Rules for Max-SAT 

    Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Association for the Advancement of Artificial Intelligence, 2007)
    Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability ...
  • Argument-based critics and recommenders: A qualitative perspective on user support systems 

    Chesñevar, Carlos Iván; Maguitman, Ana Gabriela; Simari, Guillermo Ricardo (Elsevier, 2006)
    In recent years we have witnessed the wide-spread evolution of support tools that operate in association with the user to accomplish a range of computer-mediated tasks. Two examples of these tools are critics and recommenders. ...
  • Exact Max-SAT solvers for over-constrained problems 

    Argelich Romà, Josep; Manyà Serres, Felip (Springer Verlag, 2006)
    We present a new generic problem solving approach for over-constrained problems based on Max-SAT. We first define a Boolean clausal form formalism, called soft CNF formulas, that deals with blocks of clauses instead of ...
  • Argumentation and the Dynamics of Warranted Beliefs in Changing Environments 

    Capobianco, Marcela; Chesñevar, Carlos Iván; Simari, Guillermo Ricardo (Springer Verlag, 2005)
    One of the most difficult problems in Multi-Agent Systems (MAS) involves representing the knowledge and beliefs of an agent which performs its tasks in a dynamic environment. New perceptions modify this agent’s current ...
  • Exploiting multivalued knowledge in variable selection heuristics for SAT solvers 

    Ansótegui Gil, Carlos José; Larrubia, Jose; Li, Chu-Min; Manyà Serres, Felip (Springer Verlag, 2007)
    We show that we can design and implement extremely efficient variable selection heuristics for SAT solvers by identifying, in Boolean clause databases, sets of Boolean variables that model the same multivalued variable ...
  • Improved Branch and Bound Algorithms for Max-2-SAT and Weighted Max-2-SAT 

    Planes Cid, Jordi (Springer Verlag, 2003)
    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, ...
  • Adding truth-constants to logics of continuous t-norms: Axiomatization and completeness results 

    Noguera, Carles; Esteva, Francesc; Gispert, Joan; Godó, Lluís (Elsevier, 2007)
    In this paper we study generic expansions of logics of continuous t-norms with truth-constants, taking advantage of previous results for Łukasiewicz logic and more recent results for Gödel and Product logics. Indeed, we ...
  • Minimal and Redundant SAT Encodings for the All-Interval-Series Problem 

    Alsinet, Teresa; Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip (Springer Verlag, 2002)
    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 ...
  • Regular-SAT: A many-valued approach to solving combinatorial problems 

    Béjar Torres, Ramón; Manyà Serres, Felip; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Gomes, Carla (Elsevier, 2007)
    Regular-SAT is a constraint programming language between CSP and SAT that—by combining many of the good properties of each paradigm—offers a good compromise between performance and expressive power. Its similarity to SAT ...

View more