Browsing by Author "Nieuwenhuis, Robert Lukas Mario"
Now showing items 1-17 of 17
-
A heuristic approach to the design of optimal cross-docking boxes
Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Institute of Electrical and Electronics Engineers (IEEE), 2021-09-03)
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 ... -
A parametric approach for smaller and better encodings of cardinality constraints
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer, 2013)
Conference report
Open AccessAdequate 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 ... -
Basic superposition is complete
Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto (1991-10-15)
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 ... -
BDDs for Pseudo-Boolean Constraints
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer Verlag, 2011)
Conference report
Restricted access - publisher's policyPseudo-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
Asín Acha, Roberto Javier; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer, 2009)
Conference report
Restricted access - publisher's policyWe 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 ... -
Classes of term rewrite systems with polynomial confluence problems
Godoy Balil, Guillem; Nieuwenhuis, Robert Lukas Mario (2002-06-06)
Research report
Open AccessThe confluence property of ground (i.e., variable-free) term rewrite systems (GTRS) is well-known to be decidable. This was proved independently in [DTHL87,DHLT90] and in [Oya87] using tree automata techniques and ground ... -
COMPILADORS I (Examen 1r quadrim.)
Nieuwenhuis, Robert Lukas Mario (Universitat Politècnica de Catalunya, 2002-01-15)
Exam
Restricted access to the UPC academic community -
COMPILADORS I (Examen 1r quadrim.)
Nieuwenhuis, Robert Lukas Mario (Universitat Politècnica de Catalunya, 2002-01-15)
Exam
Restricted access to the UPC academic community -
Decision levels are stable: towards better SAT heuristics
Nieuwenhuis, Robert Lukas Mario; Lozano Navarro, Adrián; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (EasyChair Publications, 2020)
Conference report
Restricted access - publisher's policyWe 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 ... -
Efficient deduction in equality Horn logic by Horn-completion
Nieuwenhuis, Robert Lukas Mario; Nivela Alós, M. Pilar Brígida (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 ... -
Employee scheduling with SAT-based pseudo-boolean constraint solving
Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rollón Rico, Emma (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 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 ... -
First-order completion with ordering constraints: some positive and some negative results
Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto (1991-10-15)
Research report
Open AccessWe show by means of counter examples that some well-known 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 ... -
Improving IntSat by expressing disjunctions of bounds as linear constraints
Asín Acha, Roberto Javier; Aloysius Bezem, Marcus; Nieuwenhuis, Robert Lukas Mario (2016)
Article
Restricted access - publisher's policyConflict-Driven Clause Learning (CDCL) SAT solvers can automatically solve very large real-world problems. IntSat is a new technique extending CDCL to Integer Linear Programming (ILP). For some conflicts, IntSat generates ... -
Reducing chaos in SAT-like search: finding solutions close to a given one
Abío Roig, Ignasi; Deters, Morgan; Nieuwenhuis, Robert Lukas Mario; Stuckey, Peter (Springer Verlag, 2011)
Conference report
Restricted access - publisher's policyMotivated by our own industrial users, we attack the following challenge that is crucial in many practical planning, scheduling or timetabling applications. Assume that a solver has found a solution for a given hard ... -
Resolvedor SAT, basado en procedimientos Davis-Putnam-Longemann-Loveland
Gabriel Cerna, Pedro Víctor; Nieuwenhuis, Robert Lukas Mario (2007-01)
Research report
Open AccessEl problema de satisfación de fórmulas lógicas (SAT), es un problema NP-Hard. Una forma de resolverlo es por medio de procedimientos Davis-Putnam-Longemann-Loveland (DPLL), ahora presentamos una implementación de un ... -
The IntSat method for integer linear programming
Nieuwenhuis, Robert Lukas Mario (Springer, 2014)
Conference report
Open AccessConflict-Driven Clause-Learning (CDCL) SAT solvers can automatically solve very large real-world problems. To go beyond, and in particular in order to solve and optimize problems involving linear arithmetic constraints, ... -
To encode or to propagate? The best choice for each constraint in SAT
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Stuckey, Peter (Springer, 2013)
Conference report
Open AccessSophisticated 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 ...