LOGPROG  Lògica i Programació
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ó (MaxSAT, MaxSMT); 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.
The group carries out research in basic computer science. In particular, it has internationallyrecognised expertise in the (closely related) fields of logic in computer science, computational complexity and constraintsolving problems, and in the use of advanced programming techniques (e.g. constraint programming, automated deduction, etc.) for the development of practical software tools.
In what follows, we give a brief overview of these research lines. Logic has been called "the calculus of computer science", because its role in computer science is similar to that of mathematics in the physical sciences (see, for example, www.cs.rice.edu/~vardi/logic).
Similarly to the way in which architects and engineers analyse their designs mathematically, computer scientists use logic to analyse systems¿ properties (e.g. correctness, safety and security), during all the phases of their life cycles (e.g. specification, development, verification and maintenance). Also, for systems whose efficiency is critical, logicbased analysis can be very helpful, and in all kinds of systems, logicbased techniques help to reduce costs (see, for example, the section on software productivity tools at research.microsoft.com). Hence, it is not surprising that there is an increasing tendency to use logicbased formalisms in all kinds of hardware and software systems and their components, such as databases or programming languages, among others.
Computational complexity involves the study of the resources required during computation to solve a given problem. The most common resources are time (number of computation steps) and space (amount of memory). Other resources can also be considered, such as randomness (how randomness can increase efficiency) and parallelism (how the use of parallel processors can help). Today, the connections between logic and complexity are well established. For example, the field of proof complexity involves the study of the mathematical relationships between complexity classes (i.e. classes of problems that are solvable using the same amount of resources) and the length of proofs in certain logical systems. This field arose as an approach to the wellknown problem of whether the P class of problems equals the NP class or not (see the milliondollar prizes at www.claymath.org): if one could show that, for every propositional proof system, there is a class of tautologies with no short proofs, then the answer is negative. The study of the limitations of proof systems has also led to the discovery of important new algorithms.
Constraint programming is the study of computational systems based on constraints. It has recently emerged as an area of research that engages researchers from a variety of fields. The idea is to solve problems by stating constraints (i.e. conditions, properties) that must be satisfied by the solution. Constraint programming consists of the generation of requirements (constraints) and the solution of these requirements by specialised constraint solvers. It has been successfully applied in numerous domains, including computer graphics (to express geometric coherence), natural language processing (to construct efficient parsers), database systems (to ensure and/or restore the consistency of the data), operations research (optimisation problems), molecular biology (DNA sequencing), business applications (option trading), electrical engineering (to locate faults), circuit design (to compute layouts), etc. Most, if not all, of these practical problems fall into the complexity class of NPcomplete problems, for which proof complexity results give insight into classes of deterministic algorithms.
The research group will continue to carry out research in logicbased methods in the areas of automated deduction, rewriting, constraint/logic programming, hardware and software verification, and symbolic computation. For constraintsatisfaction problems and algorithms for combinatorial optimisation problems, the group will also continue to work on aspects such as heuristics, symmetries, and valued constraints, and carry out research in the field of proof and circuit complexity and its close relationship with automated theoremproving and the satisfiability problem.
Specific tools that are being developed and maintained include automated deduction systems for firstorder logic, efficient decision procedures for decidable logics of interest, environments for automated termination proofs, and environments for program verification. Moreover, the research group will continue to apply such tools to circuit verification, industrial planning/scheduling, the Semantic Web, and education, and to pursue their free distribution throughout the Internet.
New research lines of particular interest include the forthcoming Semantic World Wide Web and its associated description logics for semantic search criteria, consistency/integrity restrictions, etc. Another example is the crucial need for logicbased techniques for the verification of cryptographic protocols, in applications such as secrecy, electronic signatures, and electronic money (since testing is useless against malicious attackers). From a more theoretical point of view, we intend to open new lines of research in quantum computing, cryptography, data compression, and applications of game theory to computer science.
All the members of the group have international experience, some as researchers, lecturers and guest lecturers at international institutions. This facilitates close relationships with prestigious institutions, such as the Institute for Advanced Study in Princeton (USA), the DIMACS Research Centre at Rutgers University (USA), the University of Toronto (Canada), the University of California at San Diego (USA), the MaxPlanckInstitut for Computer Science (Germany), the École Normale Superieure (France), the École Polytechnique (France), etc.
The group carries out research in basic computer science. In particular, it has internationallyrecognised expertise in the (closely related) fields of logic in computer science, computational complexity and constraintsolving problems, and in the use of advanced programming techniques (e.g. constraint programming, automated deduction, etc.) for the development of practical software tools.
In what follows, we give a brief overview of these research lines. Logic has been called "the calculus of computer science", because its role in computer science is similar to that of mathematics in the physical sciences (see, for example, www.cs.rice.edu/~vardi/logic).
Similarly to the way in which architects and engineers analyse their designs mathematically, computer scientists use logic to analyse systems¿ properties (e.g. correctness, safety and security), during all the phases of their life cycles (e.g. specification, development, verification and maintenance). Also, for systems whose efficiency is critical, logicbased analysis can be very helpful, and in all kinds of systems, logicbased techniques help to reduce costs (see, for example, the section on software productivity tools at research.microsoft.com). Hence, it is not surprising that there is an increasing tendency to use logicbased formalisms in all kinds of hardware and software systems and their components, such as databases or programming languages, among others.
Computational complexity involves the study of the resources required during computation to solve a given problem. The most common resources are time (number of computation steps) and space (amount of memory). Other resources can also be considered, such as randomness (how randomness can increase efficiency) and parallelism (how the use of parallel processors can help). Today, the connections between logic and complexity are well established. For example, the field of proof complexity involves the study of the mathematical relationships between complexity classes (i.e. classes of problems that are solvable using the same amount of resources) and the length of proofs in certain logical systems. This field arose as an approach to the wellknown problem of whether the P class of problems equals the NP class or not (see the milliondollar prizes at www.claymath.org): if one could show that, for every propositional proof system, there is a class of tautologies with no short proofs, then the answer is negative. The study of the limitations of proof systems has also led to the discovery of important new algorithms.
Constraint programming is the study of computational systems based on constraints. It has recently emerged as an area of research that engages researchers from a variety of fields. The idea is to solve problems by stating constraints (i.e. conditions, properties) that must be satisfied by the solution. Constraint programming consists of the generation of requirements (constraints) and the solution of these requirements by specialised constraint solvers. It has been successfully applied in numerous domains, including computer graphics (to express geometric coherence), natural language processing (to construct efficient parsers), database systems (to ensure and/or restore the consistency of the data), operations research (optimisation problems), molecular biology (DNA sequencing), business applications (option trading), electrical engineering (to locate faults), circuit design (to compute layouts), etc. Most, if not all, of these practical problems fall into the complexity class of NPcomplete problems, for which proof complexity results give insight into classes of deterministic algorithms.
The research group will continue to carry out research in logicbased methods in the areas of automated deduction, rewriting, constraint/logic programming, hardware and software verification, and symbolic computation. For constraintsatisfaction problems and algorithms for combinatorial optimisation problems, the group will also continue to work on aspects such as heuristics, symmetries, and valued constraints, and carry out research in the field of proof and circuit complexity and its close relationship with automated theoremproving and the satisfiability problem.
Specific tools that are being developed and maintained include automated deduction systems for firstorder logic, efficient decision procedures for decidable logics of interest, environments for automated termination proofs, and environments for program verification. Moreover, the research group will continue to apply such tools to circuit verification, industrial planning/scheduling, the Semantic Web, and education, and to pursue their free distribution throughout the Internet.
New research lines of particular interest include the forthcoming Semantic World Wide Web and its associated description logics for semantic search criteria, consistency/integrity restrictions, etc. Another example is the crucial need for logicbased techniques for the verification of cryptographic protocols, in applications such as secrecy, electronic signatures, and electronic money (since testing is useless against malicious attackers). From a more theoretical point of view, we intend to open new lines of research in quantum computing, cryptography, data compression, and applications of game theory to computer science.
All the members of the group have international experience, some as researchers, lecturers and guest lecturers at international institutions. This facilitates close relationships with prestigious institutions, such as the Institute for Advanced Study in Princeton (USA), the DIMACS Research Centre at Rutgers University (USA), the University of Toronto (Canada), the University of California at San Diego (USA), the MaxPlanckInstitut for Computer Science (Germany), the École Normale Superieure (France), the École Polytechnique (France), etc.
Collections in this community

Articles de revista [16]

Reports de recerca [21]
Recent Submissions

Efficient deduction in equality Horn logic by Horncompletion
(1991)
Research report
Open AccessWe present a new unfailing completion procedure for Horn clauses with equality, including goal clauses. It is refutationally complete, and improves previous methods in that superpositions are computed only with unconditional ... 
An implementation of the KNS ordering
(199104)
Research report
Open AccessWe describe an implementation of the KNS ordering within the TRIP system, a QuintusProlog written laboratory for experimenting with new rewritelike approaches to theorem proving in firstorder logic. The aim of the TRIP ... 
Automatic generation of polynomial loop invariants for imperative programs
(200311)
Research report
Open AccessA general framework is presented for automatig the discovery of loop invariants for imperative programs. Theoretical results about the correctness and completeness of the proposed method are given. More importantly, it is ... 
Choosing the root of the tree decomposition when solving WCSPs: preliminary results
(IOS Press, 2021)
Conference report
Open AccessIn this paper we analyze the effect of selecting the root in a tree decomposition when using decompositionbased backtracking algorithms. We focus on optimization tasks for Graphical Models using the BTD algorithm. We show ... 
Employee scheduling with SATbased pseudoboolean constraint solving
(Institute of Electrical and Electronics Engineers (IEEE), 2021)
Article
Open AccessThe aim of this paper is practical: to show that, for at least one important realworld problem, modern SATbased technology can beat the extremely mature branchandcut solving methods implemented in wellknown stateoftheart ... 
A heuristic approach to the design of optimal crossdocking boxes
(Institute of Electrical and Electronics Engineers (IEEE), 20210903)
Article
Open AccessMultinational companies frequently work with manufacturers that receive large orders for different products (or product varieties: size, shape, color, texture, material), to serve thousands of different final destinations ... 
Stuckatoff fault analysis in memristorbased architecture for synchronization
(Institute of Electrical and Electronics Engineers (IEEE), 2019)
Conference report
Restricted access  publisher's policyNonlinear circuits may be interconnected and organized in networks to couple their dynamics and achieve synchronization, a process that is commonly observed in nature. Recent works have shown that memristors may be used ... 
Decision levels are stable: towards better SAT heuristics
(EasyChair Publications, 2020)
Conference report
Restricted access  publisher's policyWe shed new light on the Literal Block Distance (LBD) and gluebased heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals ... 
Firstorder completion with ordering constraints: some positive and some negative results
(19911015)
Research report
Open AccessWe show by means of counter examples that some wellknown results on the completeness of deduction methods with ordering constraints are incorrect. The problem is caused by the fact that the usual lifting lemmata do not ... 
Basic superposition is complete
(19911015)
Research report
Open AccessWe define a formalism of equality constraints and use it to prove the completeness of what we have called basic superposition: a restricted form of superposition in which only the subterms not originated in previous ... 
Augmenting the power of (partial) MaxSat resolution with extension
(AAAI Press, 2020)
Conference lecture
Restricted access  publisher's policyThe refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof ... 
On one query selfreducible sets
(199101)
Research report
Open AccessWe study one worddecreasing selfreducible sets, which were introduced by Lozano and Torán. These are usual selfreducible sets with the peculiarity that the selfreducibility machine makes at most one query and this is ...