Resolvedor SAT, basado en procedimientos Davis-Putnam-Longemann-Loveland
Visualitza/Obre
Tipus de documentReport de recerca
Data publicació2007-01
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
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. 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
CitacióGabriel, P., Nieuwenhuis, R. "Resolvedor SAT, basado en procedimientos Davis-Putnam-Longemann-Loveland". 2007.
Forma partLSI-06-4-T
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
T06-4.pdf | 221,6Kb | Visualitza/Obre |