SAT-Solver based on conservative retractions

The project aims to solve the famous SAT problem in a efficient way. In order to do that it’s used an original algorithm based on conservative retractions (dual notion of conservtive extension). Further information obout it could be found here?.

The documentation about the modules it’s hosted here.

exDIMACS study

This directory stores several examples of sets of formulas in DIMACS format. See DIMACS format for further information about it.

Trivial Examples

example1

• Corresponds to the formula: (p ^ q)
• It’s True

example2

• Corresponds to the formula: (p ^ q) v (¬p ^ q)
• It’s True

example3

• Corresponds to the formula: (p ^ q) v (¬p ^ q) v (p ^ ¬q)
• It’s True

example4

• Corresponds to the formula: (p ^ q) v (¬p ^ q) v (p ^ ¬q) v (¬p ^ ¬q)
• It’s False

Medium Examples

exampleSat0

*MainFunctions> satCNF "exDIMACS/medium/exampleSat0.txt" frequency
The satisfactibility of instance exDIMACS/medium/exampleSat0.txt is:
True
(0.15 secs, 16,183,888 bytes)

exampleSat1

*MainFunctions> satCNF "exDIMACS/medium/exampleSat1.txt" frequency
The satisfactibility of instance exDIMACS/medium/exampleSat1.txt is:
True
(0.17 secs, 18,794,728 bytes)

exampleSat2

*MainFunctions> satCNF "exDIMACS/medium/exampleSat2.txt" frequency
The satisfactibility of instance exDIMACS/medium/exampleSat2.txt is:
True
(0.33 secs, 38,287,824 bytes)

exampleSat3

*MainFunctions> satCNF "exDIMACS/medium/exampleSat3.txt" frequency
The satisfactibility of instance exDIMACS/medium/exampleSat3.txt is:

Hard Examples

sat100

• Has 430 clauses
• Has 100 variables
• It’s True

sat250

• Has 1065 clauses
• Has 250 variables
• It’s True

unsat250

• Has 1065 clauses
• Has 250 variables
• It’s False

*MainFunctions> satCNF "exDIMACS/hard/unsat250.cnf" frequency
The satisfactibility of instance exDIMACS/hard/unsat250.cnf is:
False
(0.24 secs, 72,635,480 bytes)

References

https://github.com/andrepd/haskell-logic/blob/master/logic_parser.hs

User guide (Spanish)

Aquí se describen las pautas a seguir para poder usar la librería, suponiendo que el lector no tiene instalados ninguno de los programas necesarios.

Git

En primer lugar será necesario git . En caso de no estar instalado siga las instrucciones del enlace anterior.

Una vez instalado git correctamente, vaya a la terminal de comandos y escriba:

git clone https://github.com/DanielRodCha/SAT-canonical.git

Stack

La librería está escrita en lenguaje Haskell, así que se será necesario instalar la herramienta stack. Dicha herramienta será muy útil ya que construirá todo el proyecto, además de descargar las librerías auxiliares.

Tras haber completado la instalación de la herramienta stack, navegue por los ficheros desde el terminal hasta encontrarse en la carpeta SAT-Pol, que se creó en el paso anterior. A continuación, construya el proyecto escribiendo en el terminal:

stack update
stack build

MainFunctions

Cargar el módulo MainFunctions

Por último, se recomienda al usuario que cargue el módulo src/MainFunctions, ya que en él figuran las funciones más importantes de la librería. Para ello, escriba en la terminal:

:SAT-canonical danrodcha$ stack ghci
Configuring GHCi with the following packages: SAT-canonical


The main module to load is ambiguous. Candidates are: 
1. Package `SAT-canonical' component exe:sat with main-is file: /Users/danrodcha/SAT-canonical/app2/Main.hs
2. Package `SAT-canonical' component exe:satCNF with main-is file: /Users/danrodcha/SAT-canonical/app/Main.hs
You can specify which one to pick by: 
 * Specifying targets to stack ghci e.g. stack ghci SAT-canonical:exe:sat
 * Specifying what the main is e.g. stack ghci --main-is SAT-canonical:exe:sat
 * Choosing from the candidate above [1..2]


Specify main module to use (press enter to load none):

Pulse Enter:

Not loading any main modules, as no valid module selected

GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
[1 of 8] Compiling Logic            ( /Users/danrodcha/SAT-canonical/src/Logic.hs, interpreted )
[2 of 8] Compiling Heuristics       ( /Users/danrodcha/SAT-canonical/src/Heuristics.hs, interpreted )
[3 of 8] Compiling LogicParser      ( /Users/danrodcha/SAT-canonical/src/LogicParser.hs, interpreted )
[4 of 8] Compiling Simplification   ( /Users/danrodcha/SAT-canonical/src/Simplification.hs, interpreted )
[5 of 8] Compiling Preprocessing    ( /Users/danrodcha/SAT-canonical/src/Preprocessing.hs, interpreted )
[6 of 8] Compiling Canonical        ( /Users/danrodcha/SAT-canonical/src/Canonical.hs, interpreted )
[7 of 8] Compiling Saturation       ( /Users/danrodcha/SAT-canonical/src/Saturation.hs, interpreted )
[8 of 8] Compiling MainFunctions    ( /Users/danrodcha/SAT-canonical/src/MainFunctions.hs, interpreted )
Ok, 8 modules loaded.
Loaded GHCi configuration from /private/var/folders/k5/5wbfgm4d5cbbbgm0c9hqk94m0000gn/T/ghci5683/ghci-script
*Simplification Canonical Heuristics Logic LogicParser MainFunctions Preprocessing Saturation Simplification> 

Cargue el módulo MainFunctions:

*Simplification Canonical Heuristics Logic LogicParser MainFunctions Preprocessing Saturation Simplification> :l MainFunctions 
[1 of 8] Compiling Logic            ( /Users/danrodcha/SAT-canonical/src/Logic.hs, interpreted )
[2 of 8] Compiling Heuristics       ( /Users/danrodcha/SAT-canonical/src/Heuristics.hs, interpreted )
[3 of 8] Compiling LogicParser      ( /Users/danrodcha/SAT-canonical/src/LogicParser.hs, interpreted )
[4 of 8] Compiling Simplification   ( /Users/danrodcha/SAT-canonical/src/Simplification.hs, interpreted )
[5 of 8] Compiling Preprocessing    ( /Users/danrodcha/SAT-canonical/src/Preprocessing.hs, interpreted )
[6 of 8] Compiling Canonical        ( /Users/danrodcha/SAT-canonical/src/Canonical.hs, interpreted )
[7 of 8] Compiling Saturation       ( /Users/danrodcha/SAT-canonical/src/Saturation.hs, interpreted )
[8 of 8] Compiling MainFunctions    ( /Users/danrodcha/SAT-canonical/src/MainFunctions.hs, interpreted )
Ok, 8 modules loaded.
*MainFunctions> 

Consideraciones previas

Como una base de conocimiento es un conjunto de reglas, las listas de reglas se sumergirán en el tipo de dato Set (conjunto). Esto nos permite trabajar con bases de conocimiento sin elementos repetidos, es decir sin redundancias. Para hacer esta inmersión manualmente se puede usar la función fromList:

*MainFunctions> S.fromList []
fromList []
*MainFunctions> S.fromList [1,2,3,1,2]
fromList [1,2,3]

A continuación se exponen las principales tareas que puede resolver esta librería:

Olvidar una variable mediante el operador de omisión canónico:

Para ello basta con usar la función forgetVarKB:

*MainFunctions> f1 = Disj p q
*MainFunctions> f2 = Conj q p
*MainFunctions> forgetVarKB "p" (S.fromList[f1,f2])
fromList [⊤,q,(q & q)]
*MainFunctions> forgetVarKB "q" (S.fromList[f1,Neg f2])
fromList [⊤,(-p | p)]

Olvidar una lista determinada de variables mediante el operador de omisión canónico:

Existen dos formas de hacerlo, dejando que la librería escoja el orden en el que va a olvidar cada variable (según una heurística) o especificándolo manualmente.

• Según heurística:

*MainFunctions> f1 = Conj p q
*MainFunctions> f2 = (Neg r)
*MainFunctions> f3 = Disj r (Neg q)
*MainFunctions> forgetVarListKB' (S.fromList [f1,f2,f3]) ["p","q","r"] frequency
[fromList [-r,(q & q),(r | -q)],fromList [⊤,r,-r],fromList [⊥]]

• Orden dado:

*MainFunctions> f1 = Conj p q
*MainFunctions> f2 = (Neg r)
*MainFunctions> f3 = Disj r (Neg q)
*MainFunctions> forgetVarListKB (S.fromList [f1,f2,f3]) ["p","q","r"]
[fromList [-r,(q & q),(r | -q)],fromList [⊤,r,-r],fromList [⊥]]
*MainFunctions> forgetVarListKB (S.fromList [f1,f2,f3]) ["r","q","p"]
[fromList [⊤,-q,(p & q)],fromList [⊥],fromList [⊥]]

Resolver el problema SAT

Existen dos funciones para hacerlo, la primera resuelve directamente el problema y nos da la solución:

*MainFunctions> f1 = Conj p q
*MainFunctions> f2 = (Neg r)
*MainFunctions> f3 = Disj r (Neg q)
*MainFunctions> saturateKB (S.fromList [f1,f2,f3]) ["r","q","p"] frequency
False

Mientras que la segunda, devuelve la traza de los cálculos realizados:

*MainFunctions> f1 = Conj p q
*MainFunctions> f2 = (Neg r)
*MainFunctions> f3 = Disj r (Neg q)
*MainFunctions> saturateKBTrace (S.fromList [f1,f2,f3]) ["r","q","p"] frequency
[(fromList [-r,(p & q),(r | -q)],True),(fromList [⊤,-q,(p & q)],True),(fromList [⊤,-q,(q & q)],True),(fromList [⊥],False)]

Instancias escritas en archivos de texto

Una de las ventajas de esta librería es que permite interactuar con ejemplos escritos en archivos de texto, aunque deben estar escritos en formatos aptos, es decir, formato DIMACS o la sintaxis de Prover9:

Si el archivo contiene la base de conocimiento en formato DIMACS, las funciones que sirven para interactuar son:

*MainFunctions> dimacs "exDIMACS/easy/example1.txt"
(fromList [⊤,(p2 | p1)],["p2","p1"])
*MainFunctions> satCNF "exDIMACS/easy/example1.txt" frequency
The satisfactibility of instance exDIMACS/easy/example1.txt is:
True
*MainFunctions> dimacs "exDIMACS/easy/example4.txt"
(fromList [⊤,(p2 | p1),(p2 | -p1),(-p2 | p1),(-p2 | -p1)],["p2","p1"])
*MainFunctions> satCNF "exDIMACS/easy/example4.txt" frequency
The satisfactibility of instance exDIMACS/easy/example4.txt is:
False

Por otro lado, si el archivo contiene la base de conocimiento según la sintaxis de Prover9 (teniendo en cuenta que sólo trabaja con lógica proposicional), las funciones son:

*MainFunctions> formulas "exFORMULAS/easy/example1.txt"
(fromList [-(p4 -> p1),(p3 & p1),(p1 | p2),(p1 | -p3)],["p4","p1","p3","p2"])
*MainFunctions> satFORMULAS "exFORMULAS/easy/example1.txt" frequency
The satisfactibility of instance exFORMULAS/easy/example1.txt is:
False

Resolver una instancia SAT desde la terminal de comandos

La herramienta stack incluye la posibilidad de crear accesos directos a ciertas funciones. Aprovechando esto se han definido dos distintos en función del fichero de entrada. Si el conjunto de fórmulas está en formato DIMACS el ejecutable que se debe usar se llama satCNF, seguido del fichero que se quiere usar, así como de la heurística escogida:

MacBook-Air-de-Daniel:SAT-canonical danrodcha$ stack build
MacBook-Air-de-Daniel:SAT-canonical danrodcha$ stack exec satCNF exDIMACS/medium/exampleSat0.txt frequency
The satisfactibility of instance exDIMACS/medium/exampleSat0.txt is:
True

Si el conjunto de fórmulas sigue la sintaxis de Prove9, el ejecutable que se debe usar se llama sat, y debe ir seguido del fichero que se quiere usar, así como de la heurística escogida:

MacBook-Air-de-Daniel:SAT-canonical danrodcha$ stack build
MacBook-Air-de-Daniel:SAT-Pol danrodcha$ stack exec sat exFORMULAS/easy/example1.txt frequency
The satisfactibility of instance exFORMULAS/easy/example1.txt solved by frequency heuristics is:
False

Cálulo de Bases Débiles (Weak Basis)

Este repositorio incluye la funcionalidad de calcular bases débiles. La función que las calcula recibe como entrada la base de conocimiento y una lista con todas las variables que ocurren en ella.

Para más información sobre las bases débiles ver here? .

*MainFunctions> (kb,vs) <- formulas "exFORMULAS/article/example-4-1.txt"
*MainFunctions> kb
fromList [((t & p) -> s),((t & q) -> s),((t & r) -> s),(((p & q) & t) -> r)]
*MainFunctions> vs
["t","p","s","q","r"]
*MainFunctions> weakBasis kb vs
[["s","r"],["s","q"],["p","q","r"],["p","s"],["t"]]

Cálulo de Bases Débiles desde ficheros de texto

A fin de facilitar la labor al usuario, se incluye la posibilidad de calcular directamente una base débil de una KB almacenada en un fichero de texto (en uno de los formatos ya comentados).