Exploració per autor "Rodríguez Carbonell, Enric"
Ara es mostren els items 1-20 de 24
-
A heuristic approach to the design of optimal cross-docking boxes
(Institute of Electrical and Electronics Engineers (IEEE), 2021-09-03)
Article
Accés obertMultinational 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 ... -
A parametric approach for smaller and better encodings of cardinality constraints
(Springer, 2013)
Text en actes de congrés
Accés obertAdequate encodings for high-level constraints are a key ingredient for the application of SAT technology. In particular, cardinality constraints state that at most (at least, or exactly) k out of n propositional variables ... -
Analyzing multiple conflicts in SAT: an experimental evaluation
(EasyChair Publications, 2023)
Text en actes de congrés
Accés obertUnit propagation and conflict analysis are two essential ingredients of CDCL SAT Solving. The order in which unit propagation is computed does not matter when no conflict is found, because it is well known that there exists ... -
Automatic generation of polynomial loop invariants for imperative programs
(2003-11)
Report de recerca
Accés obertA 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 ... -
Automatic generation of polynomial loop invariants: algebraic foundations
(2004-01)
Report de recerca
Accés obertA general framework is presented for automating the discovery of loop invariants for imperative programs. Theoretical results about the correctness and completeness of the proposed method are given. More importantly, it ... -
BDDs for Pseudo-Boolean Constraints
(Springer Verlag, 2011)
Text en actes de congrés
Accés restringit per política de l'editorialPseudo-Boolean constraints are omnipresent in practical applications, and therefore a significant effort has been devoted to the development of good SAT encoding techniques for these constraints. Several of these encodings ... -
Cardinality networks and their applications
(Springer, 2009)
Text en actes de congrés
Accés restringit per política de l'editorialWe introduce Cardinality Networks, a new CNF encoding of cardinality constraints. It improves upon the previously existing encodings such as the sorting networks of [ES06] in that it requires much less clauses and auxiliary ... -
Compositional safety verification with Max-SMT
(2015)
Text en actes de congrés
Accés obertWe present an automated compositional program verification technique for safety properties based on conditional inductive invariants. For a given program part (e.g., a single loop) and a postcondition, we show how to, using ... -
Decision levels are stable: towards better SAT heuristics
(EasyChair Publications, 2020)
Text en actes de congrés
Accés restringit per política de l'editorialWe shed new light on the Literal Block Distance (LBD) and glue-based 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 ... -
Employee scheduling with SAT-based pseudo-boolean constraint solving
(Institute of Electrical and Electronics Engineers (IEEE), 2021)
Article
Accés obertThe aim of this paper is practical: to show that, for at least one important real-world problem, modern SAT-based technology can beat the extremely mature branch-and-cut solving methods implemented in well-known state-of-the-art ... -
Estructures de Dades i Algorismes Col·lecció d’Exàmens
(Universitat Politècnica de Catalunya, 2011-09-09)
Examen
Accés restringit a la comunitat UPC -
Examen final de laboratori
(Universitat Politècnica de Catalunya, 2023-01-19)
Examen
Accés restringit a la comunitat UPC -
Generation of basic semi-algebraic invariants using convex polyhedra
(2005-04)
Report de recerca
Accés obertA technique for generating invariant polynomial inequalities of bounded degree is presented using the abstract interpretation framework. It is based on overapproximating basic semi-algebraic sets, i.e., sets defined ... -
Incomplete SMT techniques for solving non-linear formulas over the integers
(2019-08-01)
Article
Accés obertWe present new methods for solving the Satisfiability Modulo Theories problem over the theory of QuantifierFree Non-linear Integer Arithmetic, SMT(QF-NIA), which consists of deciding the satisfiability of ground formulas ... -
IntSat: integer linear programming by conflict-driven constraint learning
(Taylor & Francis Group, 2023-09-27)
Article
Accés restringit per política de l'editorialState-of-the-art SAT solvers are nowadays able to handle huge real-world instances. The key to this success is the Conflict-Driven Clause-Learning (CDCL) scheme, which encompasses a number of techniques that exploit the ... -
Joc d’estructures de dades i algorismes
(Universitat Politècnica de Catalunya. Institut de Ciències de l'Educació, 2014-04-24)
Text en actes de congrés
Accés obertL'activitat consisteix en la implementació d'un jugador per a un joc d'ordinador. L'objectiu és que els estudiants hi apliquin els algorismes i estructures de dades explicats en el curs. Un joc consisteix en un tauler on ... -
Jutge.org: characteristics and experiences
(2018-07)
Article
Accés obertJutge.org is an open educational online programming judge designed for students and instructors, featuring a repository of problems that is well organized by courses, topics and difficulty. Internally, Jutge.org uses a ... -
Minimal-model-guided approaches to solving polynomial constraints and extensions
(Springer, 2014)
Text en actes de congrés
Accés obertIn this paper we present new methods for deciding the satisfiability of formulas involving integer polynomial constraints. In previous work we proposed to solve SMT(NIA) problems by reducing them to SMT(LIA): non-linear ... -
On schema and functional architectures for multilevel secure and multiuser model federated DB systems
(1997-07-02)
Report de recerca
Accés obertThis paper presents an approach for tightly federated database systems with several federated schemas that consists of a schema architecture and a functional architecture. The reference schema architecture has been ... -
Proving non-termination using max-SMT
(Springer, 2014)
Text en actes de congrés
Accés obertWe show how Max-SMT-based invariant generation can be exploited for proving non-termination of programs. The construction of the proof of non-termination is guided by the generation of quasi-invariants - properties such ...
