Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/2117/24361

The IntSat method for integer linear programming
Nieuwenhuis, Robert Lukas Mario
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
Conflict-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, here we introduce IntSat, a generalization of CDCL to Integer Linear Programming (ILP). Our simple 1400-line C++ prototype IntSat implementation already shows some competitiveness with commercial solvers such as CPLEX or Gurobi. Here we describe this new IntSat ILP solving method, show how it can be implemented efficiently, and discuss a large list of possible enhancements and extensions.
Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica
Linear programming
Computer programming
Integer programming
Commercial solvers
Integer linear programming
Linear arithmetic constraints
Real-world problem
SAT solvers
Solving method
Constraint theory
Programació lineal
info:eu-repo/semantics/submittedVersion
info:eu-repo/semantics/conferenceObject
Springer
         

Mostrar el registro completo del ítem

Documentos relacionados

Otros documentos del mismo autor/a

Asín Acha, Roberto Javier; Aloysius Bezem, Marcus; Nieuwenhuis, Robert Lukas Mario
Asín Acha, Roberto Javier; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric
Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Stuckey, Peter
Godoy Balil, Guillem; Nieuwenhuis, Robert Lukas Mario