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
(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
(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
(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
(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
(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
(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.)
(Universitat Politècnica de Catalunya, 2002-01-15)
Exam
Restricted access to the UPC academic community -
COMPILADORS I (Examen 1r quadrim.)
(Universitat Politècnica de Catalunya, 2002-01-15)
Exam
Restricted access to the UPC academic community -
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 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
(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
(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
(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
(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
(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
(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
(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
(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 ...
