SAT-Solver based on Polynomials

The project aims to solve the famous SAT problem in a efficient way. In order to do that it’s used a different algorithm based on transforming propositional logic formulas into polynomials and then use the independence rule. There is further information obout the algorithm in this paper?.

The documentation about the modules it’s hosted here.

User guide

Here are the instructions to use this library, assuming that the reader does not have any of the necessary programs installed.

Git

First of all, Git is needed. Here are instrucctions to install it.

Once you have installed it, download the library by typping the following command in the shell:

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

Stack

The library is written in Haskell language, so the stack tool it needed in order to build it. This tool will automatically download and build all the dependencies.

After you have finished the stack instalation, go to the SAT-Pol folder (It was created in the step above). Next, build the project:

stack update
stack build

MainFunctions

Load MainFunctions module:

Finally, it is recommended to load the src/MainFunctions module because it contains the most important functions of the library. In order to do that, use the following commands:

SAT-Pol danrodcha$ stack ghci
SAT-Pol-0.1.0.0: initial-build-steps (lib + exe)
Configuring GHCi with the following packages: SAT-Pol

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

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

Press 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 13] Compiling Haskell4Maths    ( /Users/danrodcha/SAT-Pol/src/Haskell4Maths.hs, interpreted )
[ 2 of 13] Compiling F2               ( /Users/danrodcha/SAT-Pol/src/F2.hs, interpreted )
[ 3 of 13] Compiling Heuristics       ( /Users/danrodcha/SAT-Pol/src/Heuristics.hs, interpreted )
[ 4 of 13] Compiling Logic            ( /Users/danrodcha/SAT-Pol/src/Logic.hs, interpreted )
[ 5 of 13] Compiling Analizador       ( /Users/danrodcha/SAT-Pol/src/Analizador.hs, interpreted )
[ 6 of 13] Compiling Subsumption      ( /Users/danrodcha/SAT-Pol/src/Subsumption.hs, interpreted )
[ 7 of 13] Compiling Transformations  ( /Users/danrodcha/SAT-Pol/src/Transformations.hs, interpreted )
[ 8 of 13] Compiling Preprocessing    ( /Users/danrodcha/SAT-Pol/src/Preprocessing.hs, interpreted )
[ 9 of 13] Compiling LogicParser      ( /Users/danrodcha/SAT-Pol/src/LogicParser.hs, interpreted )
[10 of 13] Compiling Derivative       ( /Users/danrodcha/SAT-Pol/src/Derivative.hs, interpreted )
[11 of 13] Compiling Rule             ( /Users/danrodcha/SAT-Pol/src/Rule.hs, interpreted )
[12 of 13] Compiling Saturation       ( /Users/danrodcha/SAT-Pol/src/Saturation.hs, interpreted )
[13 of 13] Compiling MainFunctions    ( /Users/danrodcha/SAT-Pol/src/MainFunctions.hs, interpreted )
Ok, 13 modules loaded.
Loaded GHCi configuration from /private/var/folders/k5/5wbfgm4d5cbbbgm0c9hqk94m0000gn/T/ghci12315/ghci-script
*Transformations Analizador Derivative F2 Haskell4Maths Heuristics Logic LogicParser MainFunctions Preprocessing Rule Saturation Subsumption Transformations>

Load MainFunctions module:

*Transformations Analizador Derivative F2 Haskell4Maths Heuristics Logic LogicParser MainFunctions Preprocessing Rule Saturation Subsumption Transformations> :l MainFunctions 
[ 1 of 12] Compiling Haskell4Maths    ( /Users/danrodcha/SAT-Pol/src/Haskell4Maths.hs, interpreted )
[ 2 of 12] Compiling F2               ( /Users/danrodcha/SAT-Pol/src/F2.hs, interpreted )
[ 3 of 12] Compiling Heuristics       ( /Users/danrodcha/SAT-Pol/src/Heuristics.hs, interpreted )
[ 4 of 12] Compiling Logic            ( /Users/danrodcha/SAT-Pol/src/Logic.hs, interpreted )
[ 5 of 12] Compiling Analizador       ( /Users/danrodcha/SAT-Pol/src/Analizador.hs, interpreted )
[ 6 of 12] Compiling Subsumption      ( /Users/danrodcha/SAT-Pol/src/Subsumption.hs, interpreted )
[ 7 of 12] Compiling Transformations  ( /Users/danrodcha/SAT-Pol/src/Transformations.hs, interpreted )
[ 8 of 12] Compiling Preprocessing    ( /Users/danrodcha/SAT-Pol/src/Preprocessing.hs, interpreted )
[ 9 of 12] Compiling Derivative       ( /Users/danrodcha/SAT-Pol/src/Derivative.hs, interpreted )
[10 of 12] Compiling Rule             ( /Users/danrodcha/SAT-Pol/src/Rule.hs, interpreted )
[11 of 12] Compiling Saturation       ( /Users/danrodcha/SAT-Pol/src/Saturation.hs, interpreted )
[12 of 12] Compiling MainFunctions    ( /Users/danrodcha/SAT-Pol/src/MainFunctions.hs, interpreted )
Ok, 12 modules loaded.
*MainFunctions>

Previous considerations

Theoretically a knowledge basis (KB) is a set of rules, so it will be represented with the datatype set. But in practice, the KB will be given as a list of rules so we must transform it by using the function fromList:

*MainFunctions> S.fromList []
fromList []
*MainFunctions> S.fromList [1,2,3,1,2]
fromList [1,2,3]
*MainFunctions> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> S.fromList [x1,x2,x1+1,x1]
fromList [x1,x1+1,x2]

As is shown above, the variables must be declared before using them to define polynomials. Later, this will not be necessary if we import the KB from a text file.

The main tasks that this library solves will be shown in the following section:

Forget a variable by using the independece rule:

This is done using the forgetVarKB function:

*MainFunctions> x1 = (var "x1") :: PolF2
*MainFunctions> x2 = (var "x2") :: PolF2
*MainFunctions> forgetVarKB x2 (S.fromList [x2,x1*x2,x1+1])
fromList [x1,x1+1,1]
*MainFunctions> forgetVarKB x1 (S.fromList [x1,x1+1,1])
fromList [0]

Forget a list of variables by using the independece rule

There are two ways of doing it, by letting the library to choose the order (according to a heuristic) or by forcing an specific order:

According to a heuristic:

*MainFunctions> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> forgetVarListKB' (S.fromList [x2,x1*x2,x1+1,x3+x4,x1*x2*x4+x2+1],[x1,x2,x3,x4]) frequency
[fromList [x1x2x4+x2+1,x1x2,x1+1,x2,1],fromList [x1x2,x1x2+x2+1,x1+1,x2,1],fromList [0],fromList [0]]

Specific order:

*MainFunctions> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> forgetVarListKB (S.fromList [x2,x1*x2,x1+1,x3+x4,x1*x2*x4+x2+1],[x3,x2,x4,x1])
[fromList [x1x2x4+x2+1,x1x2,x1+1,x2,1],fromList [x1x4,x1,x1+1,1],fromList [x1,x1+1,1],fromList [0]]

Solve SAT problem

There are two ways of doing it, the first solves the problem and return only the solution:

*MainFunctions> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> saturateKB (S.fromList [x2,x1*x2,x1+1,x3+x4,x1*x2*x4+x2+1],[x1,x2,x3,x4]) frequency
False

While the second one, returns all the calculation trace.

*MainFunctions> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> saturateKBTrace (S.fromList [x2,x1*x2,x1+1,x3+x4,x1*x2*x4+x2+1],[x1,x2,x3,x4]) frequency
[(fromList [x1x2x4+x2+1,x1x2,x1+1,x2,x3+x4],True),(fromList [0],False)]

Problem instances written in text files

One of the main advantages of this library is that allows us to work with problems examples written in tex files. But them must be written in good formats as DIMACS or Prover9 syntax:

If the KB is in DIMACS format, the useful functions are:

*MainFunctions> dimacs2Pols "exDIMACS/easy/example1.txt"
(fromList [x1x2+x1+x2,1],[x1,x2])
*MainFunctions> satCNF "exDIMACS/easy/example1.txt" "frequency"
The satisfactibility of instance exDIMACS/easy/example1.txt solved by frequency heuristics is:
True

Note that we must specify which heuristic we want to use. In the above case we used frequency heuristic but there are many other. If the reader want to explore them (or even define others) go to Heuristic module.

If the KB is written used the Prover9 syntax, the functions are the following:

*MainFunctions> formulas2Pols "exFORMULAS/easy/example4.txt"
(fromList [x1x2+x1+x2,x1x2+x1+1,x1x2+x2+1,x1x2+1],[x1,x2])
*MainFunctions> satFORMULAS "exFORMULAS/easy/example4.txt" "frequency"
The satisfactibility of instance exFORMULAS/easy/example1.txt solved by frequency heuristics is:
False

Solve a SAT instace by commands:

The stack tool allow us to create some executables. We have made two of them, depending on the format of the file. If the KB is in DIMACS format the executable is named satCNF and must be followed by the file name and the heuristic:

MacBook-Air-de-Daniel:SAT-Pol danrodcha$ stack build
MacBook-Air-de-Daniel:SAT-Pol danrodcha$ stack exec satCNF exDIMACS/medium/exampleSat2.txt frequency
The satisfactibility of instance exDIMACS/medium/exampleSat2.txt solved by frequency heuristics is:
True

If the KB is written by Prover9 syntax, the executable is named sat:

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

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 solved by frequency heuristics is:
True
(0.22 secs, 62,421,664 bytes)

exampleSat1

*MainFunctions> satCNF "exDIMACS/medium/exampleSat1.txt" "frequency"
The satisfactibility of instance exDIMACS/medium/exampleSat1.txt solved by frequency heuristics is:
True
(0.30 secs, 91,977,392 bytes)

exampleSat2

*MainFunctions> satCNF "exDIMACS/medium/exampleSat2.txt" "frequency"
The satisfactibility of instance exDIMACS/medium/exampleSat2.txt solved by frequency heuristics is:
True
(5.75 secs, 2,316,817,464 bytes)

exampleSat3

*MainFunctions> satCNF
The satisfactibility of instance exDIMACS/medium/exampleSat3.txt solved by frequency heuristics 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
The satisfactibility of instance exDIMACS/hard/unsat250.cnf solved by frequency heuristics is:
False
(0.07 secs, 34,195,800 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-Pol.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-Pol danrodcha$ stack ghci
SAT-Pol-0.1.0.0: initial-build-steps (lib + exe)
Configuring GHCi with the following packages: SAT-Pol

The main module to load is ambiguous. Candidates are: 
1. Package `SAT-Pol' component exe:sat with main-is file: /Users/danrodcha/SAT-Pol/app2/Main.hs
2. Package `SAT-Pol' component exe:satCNF with main-is file: /Users/danrodcha/SAT-Pol/app/Main.hs
You can specify which one to pick by: 
 * Specifying targets to stack ghci e.g. stack ghci SAT-Pol:exe:sat
 * Specifying what the main is e.g. stack ghci --main-is SAT-Pol: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 13] Compiling Haskell4Maths    ( /Users/danrodcha/SAT-Pol/src/Haskell4Maths.hs, interpreted )
[ 2 of 13] Compiling F2               ( /Users/danrodcha/SAT-Pol/src/F2.hs, interpreted )
[ 3 of 13] Compiling Heuristics       ( /Users/danrodcha/SAT-Pol/src/Heuristics.hs, interpreted )
[ 4 of 13] Compiling Logic            ( /Users/danrodcha/SAT-Pol/src/Logic.hs, interpreted )
[ 5 of 13] Compiling Analizador       ( /Users/danrodcha/SAT-Pol/src/Analizador.hs, interpreted )
[ 6 of 13] Compiling Subsumption      ( /Users/danrodcha/SAT-Pol/src/Subsumption.hs, interpreted )
[ 7 of 13] Compiling Transformations  ( /Users/danrodcha/SAT-Pol/src/Transformations.hs, interpreted )
[ 8 of 13] Compiling Preprocessing    ( /Users/danrodcha/SAT-Pol/src/Preprocessing.hs, interpreted )
[ 9 of 13] Compiling LogicParser      ( /Users/danrodcha/SAT-Pol/src/LogicParser.hs, interpreted )
[10 of 13] Compiling Derivative       ( /Users/danrodcha/SAT-Pol/src/Derivative.hs, interpreted )
[11 of 13] Compiling Rule             ( /Users/danrodcha/SAT-Pol/src/Rule.hs, interpreted )
[12 of 13] Compiling Saturation       ( /Users/danrodcha/SAT-Pol/src/Saturation.hs, interpreted )
[13 of 13] Compiling MainFunctions    ( /Users/danrodcha/SAT-Pol/src/MainFunctions.hs, interpreted )
Ok, 13 modules loaded.
Loaded GHCi configuration from /private/var/folders/k5/5wbfgm4d5cbbbgm0c9hqk94m0000gn/T/ghci12315/ghci-script
*Transformations Analizador Derivative F2 Haskell4Maths Heuristics Logic LogicParser MainFunctions Preprocessing Rule Saturation Subsumption Transformations>

Cargue el módulo MainFunctions:

*Transformations Analizador Derivative F2 Haskell4Maths Heuristics Logic LogicParser MainFunctions Preprocessing Rule Saturation Subsumption Transformations> :l MainFunctions 
[ 1 of 12] Compiling Haskell4Maths    ( /Users/danrodcha/SAT-Pol/src/Haskell4Maths.hs, interpreted )
[ 2 of 12] Compiling F2               ( /Users/danrodcha/SAT-Pol/src/F2.hs, interpreted )
[ 3 of 12] Compiling Heuristics       ( /Users/danrodcha/SAT-Pol/src/Heuristics.hs, interpreted )
[ 4 of 12] Compiling Logic            ( /Users/danrodcha/SAT-Pol/src/Logic.hs, interpreted )
[ 5 of 12] Compiling Analizador       ( /Users/danrodcha/SAT-Pol/src/Analizador.hs, interpreted )
[ 6 of 12] Compiling Subsumption      ( /Users/danrodcha/SAT-Pol/src/Subsumption.hs, interpreted )
[ 7 of 12] Compiling Transformations  ( /Users/danrodcha/SAT-Pol/src/Transformations.hs, interpreted )
[ 8 of 12] Compiling Preprocessing    ( /Users/danrodcha/SAT-Pol/src/Preprocessing.hs, interpreted )
[ 9 of 12] Compiling Derivative       ( /Users/danrodcha/SAT-Pol/src/Derivative.hs, interpreted )
[10 of 12] Compiling Rule             ( /Users/danrodcha/SAT-Pol/src/Rule.hs, interpreted )
[11 of 12] Compiling Saturation       ( /Users/danrodcha/SAT-Pol/src/Saturation.hs, interpreted )
[12 of 12] Compiling MainFunctions    ( /Users/danrodcha/SAT-Pol/src/MainFunctions.hs, interpreted )
Ok, 12 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]
*MainFunctions> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> S.fromList [x1,x2,x1+1,x1]
fromList [x1,x1+1,x2]

Tal y como se ve en el ejemplo anterior, si queremos definir nuestros propios polinomios se deben declarar las variables previamente. Posteriormente se verá que esto no es necesario si importamos una base de conocimiento desde un archivo de texto.

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

Olvidar una variable mediante la regla de independencia:

Para ello basta con usar la función forgetVarKB:

*MainFunctions> x1 = (var "x1") :: PolF2
*MainFunctions> x2 = (var "x2") :: PolF2
*MainFunctions> forgetVarKB x2 (S.fromList [x2,x1*x2,x1+1])
fromList [x1,x1+1,1]
*MainFunctions> forgetVarKB x1 (S.fromList [x1,x1+1,1])
fromList [0]

Olvidar una lista determinada de variables mediante la regla de independecia

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> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> forgetVarListKB' (S.fromList [x2,x1*x2,x1+1,x3+x4,x1*x2*x4+x2+1],[x1,x2,x3,x4]) frequency
[fromList [x1x2x4+x2+1,x1x2,x1+1,x2,1],fromList [x1x2,x1x2+x2+1,x1+1,x2,1],fromList [0],fromList [0]]

Orden dado:

*MainFunctions> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> forgetVarListKB (S.fromList [x2,x1*x2,x1+1,x3+x4,x1*x2*x4+x2+1],[x3,x2,x4,x1])
[fromList [x1x2x4+x2+1,x1x2,x1+1,x2,1],fromList [x1x4,x1,x1+1,1],fromList [x1,x1+1,1],fromList [0]]

Resolver el problema SAT

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

*MainFunctions> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> saturateKB (S.fromList [x2,x1*x2,x1+1,x3+x4,x1*x2*x4+x2+1],[x1,x2,x3,x4]) frequency
False

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

*MainFunctions> [x1,x2,x3,x4] = map var ["x1","x2","x3","x4"] :: [PolF2]
*MainFunctions> saturateKBTrace (S.fromList [x2,x1*x2,x1+1,x3+x4,x1*x2*x4+x2+1],[x1,x2,x3,x4]) frequency
[(fromList [x1x2x4+x2+1,x1x2,x1+1,x2,x3+x4],True),(fromList [0],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> dimacs2Pols "exDIMACS/easy/example1.txt"
(fromList [x1x2+x1+x2,1],[x1,x2])
*MainFunctions> satCNF "exDIMACS/easy/example1.txt" "frequency"
The satisfactibility of instance exDIMACS/easy/example1.txt solved by frequency heuristics is:
True

Se debe tener en cuenta que se especifica el nombre de la heurística que se quiere utilizar mediante una cadena de caracteres.

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> formulas2Pols "exFORMULAS/easy/example4.txt"
(fromList [x1x2+x1+x2,x1x2+x1+1,x1x2+x2+1,x1x2+1],[x1,x2])
*MainFunctions> satFORMULAS "exFORMULAS/easy/example4.txt" "frequency"
The satisfactibility of instance exFORMULAS/easy/example1.txt solved by frequency heuristics 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-Pol danrodcha$ stack build
MacBook-Air-de-Daniel:SAT-Pol danrodcha$ stack exec satCNF exDIMACS/medium/exampleSat2.txt frequency
The satisfactibility of instance exDIMACS/medium/exampleSat2.txt solved by frequency heuristics 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-Pol danrodcha$ stack build
MacBook-Air-de-Daniel:SAT-Pol danrodcha$ stack exec sat exFORMULAS/easy/example4.txt frequency
The satisfactibility of instance exFORMULAS/easy/example1.txt solved by frequency heuristics is:
False

Name		Name	Last commit message	Last commit date
Latest commit History 70 Commits
app		app
app2		app2
bench		bench
docs		docs
exDIMACS		exDIMACS
exFORMULAS/easy		exFORMULAS/easy
src		src
test-doc		test-doc
test-spec		test-spec
.gitignore		.gitignore
LICENSE		LICENSE
README.org		README.org
SAT-Pol.cabal		SAT-Pol.cabal
Setup.hs		Setup.hs
package.yaml		package.yaml
stack-docs		stack-docs
stack.yaml		stack.yaml

License

DanielRodCha/SAT-Pol

Folders and files

Latest commit

History

Repository files navigation

SAT-Solver based on Polynomials

User guide

Git

Stack

MainFunctions

Load MainFunctions module:

Previous considerations

Forget a variable by using the independece rule:

Forget a list of variables by using the independece rule

Solve SAT problem

Problem instances written in text files

Solve a SAT instace by commands:

exDIMACS study

Trivial Examples

example1

example2

example3

example4

Medium Examples

exampleSat0

exampleSat1

exampleSat2

exampleSat3

Hard Examples

sat100

sat250

unsat250

References

User guide (Spanish)

Git

Stack

MainFunctions

Cargar el módulo MainFunctions

Consideraciones previas

Olvidar una variable mediante la regla de independencia:

Olvidar una lista determinada de variables mediante la regla de independecia

Resolver el problema SAT

Instancias escritas en archivos de texto

Resolver una instancia SAT desde la terminal de comandos

About

Topics

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Contributors 2

Uh oh!

Languages

Packages