Now showing items 21-33 of 33

    • 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 ...
    • Boolean lexicographic optimization: algorithms & applications 

      Marques-Silva, Joao; Argelich Romà, Josep; Graça, Ana; Lynce, Inês (Springer Verlag, 2011)
      Multi-Objective Combinatorial Optimization (MOCO) problems find a wide range of practical application problems, some of which involving Boolean variables and constraints. This paper develops and evaluates algorithms for ...
    • Extending the Reach of SAT with Many-Valued Logics 

      Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip; Gomes, Carla (Elsevier, 2001)
      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 ...
    • Solving Over-Constrained Problems with SAT Technology 

      Argelich Romà, Josep; Manyà Serres, Felip (Springer Verlag, 2005)
      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 ...
    • The Sudoku completion problem with rectangular hole pattern is NP-complete 

      Béjar Torres, Ramón; Fernàndez Camon, César; Mateu Piñol, Carles; Valls Marsal, Magda (Elsevier, 2012)
      The sudoku completion problem is a special case of the latin square completion problem and both problems are known to be NP-complete. However, in the case of a rectangular hole pattern – i.e. each column (or row) is ...
    • 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 ...
    • 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 ...
    • Towards an Automated Deduction System for First-Order Possibilistic Logic Programming with Fuzzy Constants 

      Alsinet, Teresa; Godo i Lacasa, Lluís (Wiley, 2002)
      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 ...
    • Capturing Structure with Satisfiability 

      Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip; Gomes, Carla (Springer Verlag, 2001)
      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 ...
    • 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 ...
    • Iterative and core-guided MaxSAT solving: A survey and assessment 

      Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes Cid, Jordi; Marques-Silva, Joao (Springer Verlag, 2013)
      Maximum Satisfiability (MaxSAT) is an optimization version of SAT, and many real world applications can be naturally encoded as such. Solving MaxSAT is an important problem from both a theoretical and a practical point of ...
    • Modeling energy consumption in automated vacuum waste collection systems 

      Fernàndez Camon, César; Manyà Serres, Felip; Mateu Piñol, Carles; Solé Mauri, Francina (Elsevier, 2014)
      In a world where resources are scarce and urban areas consume the vast majority of these resources, it is vital to make cities greener and more sustainable. A smart city is a city in which information and communications ...
    • The satisfiability problem in regular CNF-formulas 

      Manyà Serres, Felip; Béjar Torres, Ramón; Escalada Imaz, G. (Springer Verlag, 1998)
      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 ...