DPP and DPLL algorithms

Davis-Putnam Procedure and Davis-Putnam-Loveland-Logemann Procedure are implemented herein. Both of them aims to solve the satisfiability of a CNF formula. Further information about them could be found in SAT Basics.

The documentation about the modules it’s hosted here.

exDIMACS study DPP

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

*DPP> dPP "exDIMACS/medium/exampleSat0.txt"
True
(0.03 secs, 3,354,776 bytes)

exampleSat1

*DPP> dPP "exDIMACS/medium/exampleSat1.txt"
True
(0.07 secs, 3,905,176 bytes)

exampleSat2

*DPP> dPP "exDIMACS/medium/exampleSat2.txt"
True
(0.06 secs, 12,532,944 bytes)

exampleSat3

Hard Examples

sat100

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

*DPP> dPP "exDIMACS/hard/sat100.cnf"
 *** Exception: stack overflow

sat250

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

*DPP> dPP "exDIMACS/hard/sat250.cnf"
 *** Exception: stack overflow

unsat250

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

*DPP> dPP "exDIMACS/hard/unsat250.cnf"
 *** Exception: stack overflow

exDIMACS study DPLL

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

*DPLL> dPLL "exDIMACS/medium/exampleSat0.txt"
True
(0.03 secs, 3,343,304 bytes)

exampleSat1

*DPLL> dPLL "exDIMACS/medium/exampleSat1.txt"
True
(0.03 secs, 3,885,384 bytes)

exampleSat2

*DPLL> dPLL "exDIMACS/medium/exampleSat2.txt"
True
(0.03 secs, 8,937,712 bytes)

exampleSat3

*DPLL> dPLL "exDIMACS/medium/exampleSat3.txt"
True
(0.10 secs, 12,827,976 bytes)

Hard Examples

sat100

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

*DPLL> dPLL "exDIMACS/hard/sat100.cnf"
True
(49.64 secs, 20,665,524,672 bytes)

sat250

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

*DPP> dPP "exDIMACS/hard/sat250.cnf"
 *** Exception: stack overflow

unsat250

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

*DPP> dPP "exDIMACS/hard/unsat250.cnf"
 *** Exception: stack overflow