Exploració per autor "Oliveras Llunell, Albert"
Ara es mostren els items 1-17 de 17
-
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 ... -
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 ... -
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 ... -
Learning shorter redundant clauses in SDCL using MaxSAT
(Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023)
Text en actes de congrés
Accés obertIn this paper we present the design and implementation of a Satisfaction-Driven Clause Learning (SDCL) SAT solver, MapleSDCL, which uses a MaxSAT-based technique that enables it to learn shorter, and hence better, redundant ... -
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 ... -
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 ... -
Proving termination of imperative programs using Max-SMT
(2013)
Text en actes de congrés
Accés obertWe show how Max-SMT can be exploited in constraint-based program termination proving. Thanks to expressing the generation of a ranking function as a Max-SMT optimization problem where constraints are assigned different ... -
Proving termination through conditional termination
(Springer, 2017)
Text en actes de congrés
Accés obertWe present a constraint-based method for proving conditional termination of integer programs. Building on this, we construct a framework to prove (unconditional) program termination using a powerful mechanism to combine ... -
Speeding up the constraint-based method in difference logic
(2016)
Text en actes de congrés
Accés obertOver the years the constraint-based method has been successfully applied to a wide range of problems in program analysis, from invariant generation to termination and non-termination proving. Quite often the semantics of ... -
To encode or to propagate? The best choice for each constraint in SAT
(Springer, 2013)
Text en actes de congrés
Accés obertSophisticated compact SAT encodings exist for many types of constraints. Alternatively, for instances with many (or large) constraints, the SAT solver can also be extended with built-in propagators (the SAT Modulo Theories ...
