Resolvedor SAT, basado en procedimientos Davis-Putnam-Longemann-Loveland

Consultar RECERCAT

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

Título:	Resolvedor SAT, basado en procedimientos Davis-Putnam-Longemann-Loveland
Autor/a:	Gabriel Cerna, Pedro Víctor; Nieuwenhuis, Robert Lukas Mario
Otros autores:	Universitat Politècnica de Catalunya. Departament d'Expressió Gràfica a l'Enginyeria; Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
Abstract:	El 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 resolvedor SAT a partir de procedimientos DPLL.
Abstract:	The problem of SAT is a problem NP-HARD, a way for solve is by Davis-Putnam-Longemann_Lovelan procedure (DPLL), here there is a SAT solver by this type of procedure
Materia(s):	-Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica -SAT -Resolvedor SAT
Derechos:
Tipo de documento:	Artículo - Versión publicada Informe
Compartir:

Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric

Abío Roig, Ignasi; Deters, Morgan; Nieuwenhuis, Robert Lukas Mario; Stuckey, Peter

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

Nieuwenhuis, Robert Lukas Mario

Coordinación

Patrocinio