Now showing items 1-19 of 19

    • Automated monitoring of medical protocols: a secure and distributed architecture 

      Alsinet, Teresa; Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Manyà Serres, Felip (Elsevier, 2003)
      The control of the right application of medical protocols is a key issue in hospital environments. For the automated monitoring of medical protocols, we need a domain-independent language for their representation and a ...
    • Boosting Open CSPs 

      Macho González, Santiago; Ansótegui Gil, Carlos José; Meseguer, Pedro (Springer Verlag, 2006)
      In previous work, a new approach called Open CSP (OCSP) was defined as a way of integrate information gathering and problem solving. Instead of collecting all variable values before CSP resolution starts, OCSP asks for ...
    • Edge matching puzzles as hard SAT/CSP benchmarks 

      Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (Springer, 2008)
      Recently, edge matching puzzles, an NP-complete problem, have rececived, thanks to money-prized contests, considerable attention from wide audiences. We consider these competitions not only a challenge for SAT/CSP solving ...
    • 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 ...
    • From High Girth Graphs to Hard Instances 

      Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (Springer Verlag, 2008)
      In this paper we provide a new method to generate hard k-SAT instances. Basically, we construct the bipartite incidence graph of a k-SAT instance where the left side represents the clauses and the right side represents ...
    • Generating hard SAT/CSP instances using expander graphs 

      Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (Association for the Advancement of Artificial Intelligence, 2008)
      In this paper we provide a new method to generate hard k-SAT instances. We incrementally construct a high girth bipartite incidence graph of the k-SAT instance. Having high girth assures high expansion for the graph, and ...
    • Generating highly balanced sudoku problems as hard problems 

      Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Gomes, Carla; Mateu Piñol, Carles (Springer, 2011)
      Sudoku problems are some of the most known and enjoyed pastimes, with a never diminishing popularity, but, for the last few years those problems have gone from an entertainment to an interesting research area, a twofold ...
    • How hard is a commercial puzzle: the eternity II challenge 

      Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (IOS Press, 2008)
      Recently, edge matching puzzles, an NP-complete problem, have received, thanks to money-prized contests, considerable attention from wide audiences. We consider these competitions not only a challenge for SAT/CSP solving ...
    • Incomplete MaxSAT approaches for combinatorial testing 

      Ansótegui Gil, Carlos José; Manyà Serres, Felip; Ojeda Contreras, Jesús; Salvia, Josep M.; Torres, Eduard (Springer, 2022)
      We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length, referred to as the Covering Array Number problem. This problem is central in Combinatorial Testing for ...
    • Una introducción a los algoritmos de satisfactibilidad 

      Ansótegui Gil, Carlos José; Manyà Serres, Felip (Asociación Española para la Inteligencia Artificial (AEPIA), 2003)
      En este artículo se presenta una introducción a los algoritmos de satisfactibilidad. Primero, se describe el procedimiento de Davis-Putnam, que constituye la base de la mayoría de algoritmos completos (por ejemplo: Satz, ...
    • On balanced CSPs with high treewidth 

      Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (Association for the Advancement of Artificial Intelligence, 2007)
      Tractable cases of the binary CSP are mainly divided in two classes: constraint language restrictions and constraint graph restrictions. To better understand and identify the hardest binary CSPs, in this work we propose ...
    • On the hardness of solving edge matching puzzles as SAT or CSP problems 

      Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles (Springer Verlag, 2013)
      Edge matching puzzles have been amongst us for a long time now and traditionally they have been considered, both, a children’s game and an interesting mathematical divertimento. Their main characteristics have already been ...
    • QBF modeling: exploiting player symmetry for simplicity and efficiency 

      Sabharwal, Ashish; Ansótegui Gil, Carlos José; Gomes, Carla; Hart, Justin W.; Selman, Bart (Springer Verlag, 2006)
      Quantified Boolean Formulas (QBFs) present the next big challenge for automated propositional reasoning. Not surprisingly, most of the present day QBF solvers are extensions of successful propositional satisfiability ...
    • Resolución de Problemas en Ingeniería Utilizando Técnicas de Inteligencia Artificial 

      Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Manyà Serres, Felip (AEIM, 2002)
      En este artículo presentamos el temario para una asignatura sobre resolución de problemas en ingeniería utilizando técnicas de inteligencia artificial. Por un lado, el temario cubre diferentes métodos automáticos (algoritmos) ...
    • SAT-based MaxSAT algorithms 

      Ansótegui Gil, Carlos José; Bonet, Maria Luisa; Levy, Jordi (Elsevier, 2013)
      Many industrial optimization problems can be translated to MaxSAT. Although the general problem is NP hard, like SAT, many practical problems may be solved using modern MaxSAT solvers. In this paper we present several ...
    • Scale-Free Random SAT Instances 

      Ansótegui Gil, Carlos José; Bonet, Maria Luisa; Levy, Jordi (MDPI, 2022)
      We focus on the random generation of SAT instances that have properties similar to real-world instances. It is known that many industrial instances, even with a great number of variables, can be solved by a clever solver ...
    • Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories 

      Ansótegui Gil, Carlos José; Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu (Springer Verlag, 2013)
      We introduce WSimply, a new framework for modelling and solving Weighted Constraint Satisfaction Problems (WCSP) using Satisfiability Modulo Theories (SMT) technology. In contrast to other well-known approaches designed ...
    • The Fractal Dimension of SAT Formulas 

      Ansótegui Gil, Carlos José; Bonet, Maria Luisa; Giráldez-Cru, Jesús; Levy, Jordi (Springer Verlag, 2014)
      Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is believed that these techniques exploit ...
    • The impact of balancing on problem hardness in a highly structured domain 

      Ansótegui Gil, Carlos José; Béjar Torres, Ramón; Fernàndez Camon, César; Gomes, Carla; Mateu Piñol, Carles (Association for the Advancement of Artificial Intelligence, 2006)
      Random problem distributions have played a key role in the study and design of algorithms for constraint satisfaction and Boolean satisfiability, as well as in ourunderstanding of problem hardness, beyond standard worst-case ...