Carregant...
Carregant...

Vés al contingut (premeu Retorn)

LOGPROG - Lògica i Programació

Total activitats: 509
Tipus
Grup de recerca
Tipus de grup
Grup de recerca UPC
Acrònim
LOGPROG
URL
http://www.lsi.upc.es/~roberto/ Obrir en finestra nova
Objectius
La recerca del nostre grup "Lògica i Programació" s'emmarca en el desenvolupament de tècniques i eines per a l'aplicació de la lògica a la resolució de sistemes de restriccions. Més concretament, les principals línies de la nostra investigació es basen per una banda en (a) l'estudi de mètodes de resolució de problemes mitjançant resolvedors de satisfactibilitat proposicional (SAT), de satisfactibilitat mòdul teories (SMT), de programació amb restriccions (CP), i d'extensions d'aquests a optimització (Max-SAT, Max-SMT); i (b) per una altra en l'aplicació d'aquests mètodes per atacar problemes complexos d'interès pràctic, com ara de planificació industrial o d'anàlisis de programes. Mentre que la recerca de tipus més teòric és presentada a les conferències i revistes internacionals de més prestigi de les respectives àrees, els resultats en la vessant més pràctica es materialitzen en transferència de tecnologia en empreses tant de dins com de fora de Catalunya.
Paraules clau
Satisfactibilitat Proposicional, Satisfactibilitat Mòdul Teories, Constraint Programming, Anàlisi de Programes, Lògica Informàtica
Completa aquestes dades (només responsables)

Producció científica

1 a 50 de 509 resultats
 
  • Residual-guided look-ahead in AND/OR search for graphical models

     Lam, W.; Kask, K.; Larrosa, J.; Dechter, R.
    Journal of artificial intelligence research
    Vol. 60, p. 287-346
    DOI: 10.1613/jair.5475
    Data de publicació: 2017-10-01
    Article en revista
  • Jutge.org: characteristics and experiences  Accés obert

     Petit, J.; Roura, S.; Carmona, J.; Cortadella, J.; Duch, A.; Giménez, O.; Mani, A.; Mas, J.; Rodriguez, E.; Rubio, A.; San Pedro, J. de; Venkataramani, D.
    IEEE transactions on learning technologies
    DOI: 10.1109/TLT.2017.2723389
    Data de publicació: 2017-07-04
    Article en revista
    Accés al text complet
  • A correction on Shiloach's algorithm for minimum linear arrangement of trees  Accés obert

     Esteban, J. L.; Ferrer-i-Cancho, R.
    SIAM journal on computing
    Vol. 46, num. 3, p. 1146-1151
    DOI: 10.1137/15M1046289
    Data de publicació: 2017-06-29
    Article en revista
    Accés al text complet
  • On the impact of subproblem orderings on anytime AND/OR best-first search for lower bounds

     Lam, W.; Kask, K.; Dechter, R.; Larrosa, J.
    European Conference on Artificial Intelligence
    p. 1567-1568
    DOI: 10.3233/978-1-61499-672-9-1567
    Data de presentació: 2016-08-29
    Presentació treball a congrés
  • Limited discrepancy AND/OR search and its application to optimization tasks in graphical models  Accés obert

     Larrosa, J.; Rollon, E.; Dechter, R.
    International Joint Conference on Artificial Intelligence
    p. 617-623
    Data de presentació: 2016-07-15
    Presentació treball a congrés
    Accés al text complet
  • Speeding up the constraint-based method in difference logic  Accés obert

     Candeago, L.; Larraz, D.; Oliveras, A.; Rodriguez, E.; Rubio, A.
    International Conference on Theory and Applications of Satisfiability Testing
    p. 284-301
    DOI: 10.1007/978-3-319-40970-2_18
    Data de presentació: 2016-07
    Presentació treball a congrés
    Accés al text complet
  • The scaling of the minimum sum of edge lengths in uniformly random trees  Accés obert

     Esteban, J. L.; Ferrer-i-Cancho, R.; Gómez-Rodríguez, C.
    Journal of statistical mechanics: Theory and experiment
    Vol. 2016, num. 6, p. 063401-
    DOI: 10.1088/1742-5468/2016/06/063401
    Data de publicació: 2016-06-21
    Article en revista
    Accés al text complet
  • Quasipolynomial size frege proofs of Frankl's Theorem on the trace of sets  Accés obert

     Aisenberg, J.; Bonet, M.; Buss, S.
    Journal of symbolic logic
    Vol. 81, num. 2, p. 687-710
    DOI: 10.1017/jsl.2015.17
    Data de publicació: 2016-06-01
    Article en revista
    Accés al text complet
  • Look-ahead with mini-bucket heuristics for MPE  Accés obert

     Dechter, R.; Kask, K.; Lam, W.; Larrosa, J.
    AAAI Conference on Artificial Intelligence
    p. 694-701
    Data de presentació: 2016-02-12
    Presentació treball a congrés
    Accés al text complet
  • Soluciones Efectivas basadas en la Lógica

     Rubio, A.; Larrosa, J.; Nieuwenhuis, R.; Messeguer, X.; Rivero, J.; Rollon, E.; Rodriguez, E.; Oliveras, A.; Borralleras, C.; Aloysisus, M.
    Projecte R+D+I competitiu
  • Improving IntSat by expressing disjunctions of bounds as linear constraints

     Asín, R.J.; Aloysius, M.; Nieuwenhuis, R.
    AI communications: the european journal of artificial intelligence
    Vol. 29, num. 1, p. 205-209
    DOI: 10.3233/AIC-150684
    Data de publicació: 2016
    Article en revista
  • The computability path ordering  Accés obert

     Blanqui, F.; Jouannaud, J.; Rubio, A.
    Logical methods in computer science
    Vol. 11, num. 4, Paper 3, p. 1-45
    DOI: 10.2168/LMCS-11(4:3)2015
    Data de publicació: 2015-10-26
    Article en revista
    Accés al text complet
  • Compositional safety verification with Max-SMT  Accés obert

     Brockschmidt, M.; Larraz, D.; Oliveras, A.; Rodriguez, E.; Rubio, A.
    International Conference on Formal Methods in Computer-Aided Design
    p. 33-40
    Data de presentació: 2015-09-28
    Presentació treball a congrés
    Accés al text complet
  • Termination competition (termCOMP 2015)  Accés obert

     Giesl, J.; Mesnard, F.; Rubio, A.; Thiemann, R.; Waldmann, J.
    International Conference on Automated Deduction
    p. 105-108
    DOI: 10.1007/978-3-319-21401-6_6
    Data de presentació: 2015-08-07
    Presentació treball a congrés
    Accés al text complet
  • Automatic Program Analysis using Max-SMT  Accés obert  Activitat premiada

     Larraz, D.
    Departament de Ciències de la Computació, Universitat Politècnica de Catalunya
    Tesi doctoral
    Accés al text complet
  • Normal higher-order termination  Accés obert

     Jouannaud, J.; Rubio, A.
    ACM transactions on computational logic
    Vol. 16, num. 2, p. 13:1-13:38
    DOI: 10.1145/2699913
    Data de publicació: 2015-03-01
    Article en revista
    Accés al text complet
  • Decomposing utility functions in Bounded Max-Sum for distributed constraint optimization  Accés obert

     Rollon, E.; Larrosa, J.
    International Conference on Principles and Practice of Constraint Programming
    p. 646-654
    DOI: 10.1007/978-3-319-10428-7_47
    Data de presentació: 2014-09-08
    Presentació treball a congrés
    Accés al text complet
  • The IntSat method for integer linear programming  Accés obert

     Nieuwenhuis, R.
    International Conference on Principles and Practice of Constraint Programming
    p. 574-589
    DOI: 10.1007/978-3-319-10428-7_42
    Data de presentació: 2014-09-08
    Presentació treball a congrés
    Accés al text complet
  • The fractal dimension of SAT formulas

     Ansótegui, C.; Bonet, M.; Giráldez, J.; Levy, J.
    International Joint Conference on Automated Reasoning
    p. 107-121
    DOI: 10.1007/978-3-319-08587-6_8
    Data de presentació: 2014-07-19
    Presentació treball a congrés
  • Curriculum-based course timetabling with SAT and MaxSAT

     Asín, R.J.; Nieuwenhuis, R.
    Annals of operations research
    Vol. 218, num. 1, p. 71-91
    DOI: 10.1007/s10479-012-1081-x
    Data de publicació: 2014-07-01
    Article en revista
  • Minimal-model-guided approaches to solving polynomial constraints and extensions  Accés obert

     Larraz, D.; Oliveras, A.; Rodriguez, E.; Rubio, A.
    International Conference on Theory and Applications of Satisfiability Testing
    p. 333-350
    DOI: 10.1007/978-3-319-09284-3-25
    Data de presentació: 2014-07
    Presentació treball a congrés
    Accés al text complet
  • Improved separations of regular resolution from clause learning proof systems

     Bonet, M.; Buss, S.; Johannsen, J.
    Journal of artificial intelligence research
    num. 49, p. 669-703
    Data de publicació: 2014-04-01
    Article en revista
  • Teoría y aplicaciones en satisfactibilidad y optimización de restricciones

     Atserias, A.; Bonet, M.; Esteban, J. L.; Buss, S.; Nordström, J.
    Projecte R+D+I competitiu
  • Una aproximación declarativa al modelado, análisis y resolución de problemas

     Rubio, A.; Rollon, E.; Larrosa, J.; Nieuwenhuis, R.; Messeguer, X.; Nivela, M.; Rivero, J.; Borralleras, C.; Rodriguez, E.; Oliveras, A.; Larraz, D.
    Projecte R+D+I competitiu
  • Proving non-termination using max-SMT  Accés obert

     Larraz, D.; Nimkar, K.; Oliveras, A.; Rodriguez, E.; Rubio, A.
    International Conference on Computer Aided Verification
    p. 779-796
    DOI: 10.1007/978-3-319-08867-9_52
    Presentació treball a congrés
    Accés al text complet
  • Proving termination of imperative programs using Max-SMT  Accés obert

     Larraz, D.; Oliveras, A.; Rodriguez, E.; Rubio, A.
    International Conference on Formal Methods in Computer-Aided Design
    p. 218-225
    Data de presentació: 2013-10-23
    Presentació treball a congrés
    Accés al text complet
  • To encode or to propagate? The best choice for each constraint in SAT  Accés obert

     Abio, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.; Stuckey, P.
    International Conference on Principles and Practice of Constraint Programming
    p. 97-106
    DOI: 10.1007/978-3-642-40627-0_10
    Data de presentació: 2013-09-16
    Presentació treball a congrés
    Accés al text complet
  • A parametric approach for smaller and better encodings of cardinality constraints  Accés obert

     Abio, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.
    International Conference on Principles and Practice of Constraint Programming
    p. 80-96
    DOI: 10.1007/978-3-642-40627-0_9
    Data de presentació: 2013-09-16
    Presentació treball a congrés
    Accés al text complet
  • Improving WPM2 for (weighted) partial MaxSAT

     Ansótegui, C.; Bonet, M.; Gabàs, J.; Levy, J.
    International Conference on Principles and Practice of Constraint Programming
    p. 117-132
    DOI: 10.1007/978-3-642-40627-0_12
    Data de presentació: 2013-09-16
    Presentació treball a congrés
  • An improved separation of regular resolution from pool resolution and clause learning.

     Bonet, M.; Buss, S.
    International Joint Conference on Artificial Intelligence
    p. 2972-2976
    Data de presentació: 2013-08-09
    Presentació treball a congrés
  • Semiring-based mini-bucket partitioning schemes

     Rollon, E.; Larrosa, J.; Dechter, R.
    International Joint Conference on Artificial Intelligence
    p. 644-650
    Data de presentació: 2013-08-03
    Presentació treball a congrés
  • Solving Hard Industrial Combinatorial Problems with SAT  Accés obert

     Abío, I.
    Universitat Politècnica de Catalunya
    Tesi doctoral
    Accés al text complet
  • Fun in CS2

     Duch, A.; Petit, J.; Rodriguez, E.; Roura, S.
    International Conference on Computer Supported Education
    p. 437-442
    DOI: 10.5220/0004389604370442
    Data de presentació: 2013-05-07
    Presentació treball a congrés
  • Resolution procedures for multiple-valued optimization

     Ansótegui, C.; Bonet, M.; Manyà, F.; Levy, J.
    Information sciences
    Vol. 227, p. 43-59
    DOI: 10.1016/j.ins.2012.12.004
    Data de publicació: 2013-04-01
    Article en revista
  • Decomposing utility functions in bounded max-sum for distributed constraint optimization

     Rollon, E.; Larrosa, J.
    Global Congres on Intelligent Systems
    p. 30-33
    DOI: 10.1109/GCIS.2013.11
    Data de presentació: 2013-03-03
    Presentació treball a congrés
  • 6 years of SMT-COMP

     Barrett, C.; Deters, M.; Moura, L.; Oliveras, A.; Stump, A.
    Journal of automated reasoning
    Vol. 50, num. 3, p. 243-277
    DOI: 10.1007/s10817-012-9246-5
    Data de publicació: 2013-03-01
    Article en revista
  • SAT-based MaxSAT algorithms

     Ansótegui, C.; Bonet, M.; Levy, J.
    Artificial intelligence
    Vol. 196, p. 77-105
    DOI: 10.1016/j.artint.2013.01.002
    Data de publicació: 2013-03
    Article en revista
  • Risk-neutral bounded max-sum for distributed constraint optimization

     Larrosa, J.; Rollon, E.
    ACM Symposium on Applied Computing
    p. 92-97
    DOI: 10.1145/2480362.2480383
    Data de presentació: 2013-03
    Presentació treball a congrés
  • The recursive path and polynomial ordering for first-order and higher-order terms

     Bofill, M.; Borralleras, C.; Rodriguez, E.; Rubio, A.
    Journal of logic and computation
    Vol. 23, num. 1, p. 263-305
    DOI: 10.1093/logcom/exs027
    Data de publicació: 2013-01-23
    Article en revista
  • SMT-based array invariant generation

     Larraz, D.; Rodriguez, E.; Rubio, A.
    International Conference on Verification, Model Checking, and Abstract Interpretation
    p. 169-188
    Data de presentació: 2013-01-20
    Presentació treball a congrés
  • Paramodulation with non-monotonic orderings and simplification

     Bofill, M.; Rubio, A.
    Journal of automated reasoning
    Vol. 50, num. 1, p. 51-98
    DOI: 10.1007/s10817-011-9244-z
    Data de publicació: 2013-01
    Article en revista
  • Nominal completion for rewrite systems with binders

     Fernandez, M.; Rubio, A.
    International Colloquium on Automata, Languages, and Programming
    p. 201-213
    DOI: 10.1007/978-3-642-31585-5_21
    Data de presentació: 2012-07-09
    Presentació treball a congrés
  • The complexity of finding multiple solutions to betweenness and quartet compatibility

     Bonet, M.; Linz, S.; St. John, K.
    IEEE-ACM transactions on computational biology and bioinformatics
    Vol. 9, num. 1, p. 273-285
    DOI: 10.1109/TCBB.2011.108
    Data de publicació: 2012-02
    Article en revista
  • Local arc consistency for non-invertible semirings, with an application to multi-objective optimization

     Bistarelli, S.; Gadducci, F.; Larrosa, J.; Rollon, E.; Santini, F.
    Expert systems with applications
    Vol. 39, num. 2, p. 1708-1717
    DOI: 10.1016/j.eswa.2011.06.062
    Data de publicació: 2012-02-01
    Article en revista
  • A new look at BDDs for Pseudo-Boolean constraints

     Abio, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.; Mayer, V.
    Journal of artificial intelligence research
    Vol. 45, num. 1, p. 443-480
    DOI: 10.1613/jair.3653
    Data de publicació: 2012
    Article en revista
  • Improved bounded max-sum for distributed constraint optimization

     Rollon, E.; Larrosa, J.
    International Conference on Principles and Practice of Constraint Programming
    p. 624-632
    DOI: 10.1007/978-3-642-33558-7_45
    Data de presentació: 2012
    Presentació treball a congrés
  • SAT and SMT are still resolution: questions and challenges

     Nieuwenhuis, R.
    International Joint Conference on Automated Reasoning
    p. 10-13
    DOI: 10.1007/978-3-642-31365-3_3
    Presentació treball a congrés
  • Analysis and generation of pseudo-industrial MaxSAT instances

     Ansótegui, C.; Bonet, M.; Li, C.; Levy, J.
    International Conference of the Catalan Association for Artificial Intelligence
    p. 173-184
    DOI: 10.3233/978-1-61499-139-7-173
    Data de presentació: 2012
    Presentació treball a congrés
  • Improving SAT-based Weighted MaxSAT solvers

     Ansótegui, C.; Bonet, M.; Cabàs, J.; Levy, J.
    International Conference on Principles and Practice of Constraint Programming
    p. 86-101
    DOI: 10.1007/978-3-642-33558-7_9
    Presentació treball a congrés
  • An improved separation of regular resolution from pool resolution and clause learning

     Bonet, M.; Buss, S.
    International Conference on Theory and Applications of Satisfiability Testing
    p. 44-57
    DOI: 10.1007/978-3-642-31612-8_5
    Presentació treball a congrés