The Davis-Putnam-Logemann-Loveland (DPLL) algorithm is a complete backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.
The DPLL algorithm enhances over the backtracking algorithm by the eager use of the following rules at each step –
-
Unit Propagation – If a clause is a unit clause, i.e. contains only a single unassigned literal, this clause can only be satisfied by assigning the necessary value to make this literal true. Thus, it removes every clause containing a unit clause’s literal and in discarding the complement of the same from every clause containing that complement.
-
Branching Heuristics – Jersolow-Wang 2-sided method is used in the implementation of the SAT Solver.
The Jersolow-Wang 2-sided heuristic estimates the contribution each literal is likely to make to satisfy the clause set. Each literal is scored as follows –
For each clause c (containing either polarity of a given literal) the literal appears in, 2 -|c| is added to the literal’s score, where |c| is the number of literals in c. The split-rule is then applied to the literal with the highest score.
-
parse_dimacs (filename) – Parses the clauses present in the input DIMACs CNF file.
Returns the clauses as a list and the number of variables in the CNF. -
get_weighted_abs_counter (formula, weight = 2) – As mentioned above, this function adds 2-|c| to the literal’s score, where |c| is the number of literals in each clause (in the formula).
Returns a dictionary with the weighted score of the literals. -
jeroslow_wang_2_sided (formula) – Returns literal with highest score.
Function 2 and 3 together implement the Jersolow-Wang 2-sided method.
-
bcp (formula, unit) – Boolean Constraint Propagation : The ‘unit’ is set to true and the cnf is updated as per the following rules –
- Clauses that contain unit are removed (due to ‘OR’)
- Clauses are updated by removing ‘-unit’ from them if it exist (due to ‘OR’)
-
unit_propagation (formula) – Formula Simplification : If a clause is a unit clause (one with only one variable), then the only way for the formula to be satisfiable is for that variable to be assigned consistently with its sign in that clause. Thus, we know that variable must take on that assignment, which tells us that all other clauses with that literal are now satisfied. In addition, we know that clauses with the literal's negation will not be satisfied by that component, so we can remove the negation from all clauses.
-
backtracking (formula, assignment) - The DPLL algorithm - Recursive Backtracking : The algorithm "guesses" a variable to be true, recursively determines if that subproblem is satisfiable; if it is not, the algorithm then "guesses" the variable to be false and tries again.
run_benchmarks (filename, folder) – Benchmarks Tester : Tests a folder consisting of DIMACs files (CNF formulas) and gets the average time taken by the SAT-Solver.
Writes “SAT” followed by the model, if the formula is satisfiable, else writes “UNSAT”.
The filenames are also prefixed for clarity.
Benchmark Results Log -
uuf150-08.cnf : UNSAT
uuf150-09.cnf : UNSAT
uf150-014.cnf : SAT [1,-2,-3,4,-5,6,7,-8,9,10,11,-12,-13,14,-15,16,-17,18,-19,20,-21,-22,-23,24,-25,-26,-27,-28,29,-30,31,32,33,34,-35,-36,-37,38,-39,40,-41,42,43,44,-45,-46,47,48,-49,-50,51,52,-53,54,-55,56,57,58,-59,60,61,62,-63,64,65,66,-67,-68,69,70,71,-72,-73,-74,-75,76,-77,-78,-79,80,-81,-82,-83,-84,-85,-86,-87,-88,89,90,-91,-92,-93,-94,95,-96,97,-98,-99,-100,101,102,-103,104,105,106,-107,108,-109,-110,111,112,113,-114,115,-116,117,118,-119,120,-121,122,123,-124,-125,126,-127,128,-129,130,131,132,-133,134,135,136,137,138,139,140,141,142,-143,144,145,-146,-147,148,-149,150,]
uf150-015.cnf : SAT [1,-2,-3,4,5,6,-7,-8,-9,10,11,-12,13,-14,-15,-16,-17,18,-19,20,21,-22,23,-24,25,26,27,-28,29,30,31,32,-33,-34,-35,-36,37,38,39,40,41,42,43,44,-45,46,-47,-48,49,-50,51,52,-53,-54,55,-56,57,58,59,60,61,-62,-63,-64,65,66,67,68,69,-70,71,-72,73,-74,-75,76,77,-78,79,-80,81,82,83,-84,-85,-86,-87,88,89,-90,91,92,93,-94,-95,96,-97,-98,-99,100,101,-102,103,104,-105,106,107,108,-109,-110,111,-112,113,114,-115,-116,117,118,-119,120,121,122,123,-124,-125,-126,-127,-128,-129,-130,131,-132,-133,134,135,136,-137,-138,-139,140,-141,-142,143,144,-145,146,-147,-148,149,150,]
uf150-011.cnf : SAT [1,-2,-3,-4,-5,-6,7,-8,9,-10,11,12,13,14,-15,16,17,-18,19,-20,21,-22,-23,24,25,26,-27,28,-29,-30,-31,32,-33,-34,35,-36,37,38,39,-40,41,42,-43,44,45,-46,47,-48,49,50,-51,-52,-53,54,-55,56,-57,-58,59,-60,-61,-62,63,-64,65,-66,-67,68,69,-70,71,72,-73,74,75,-76,77,78,-79,80,-81,-82,-83,-84,-85,-86,-87,88,-89,90,-91,92,-93,94,-95,-96,97,-98,99,100,101,-102,-103,104,105,-106,-107,108,-109,-110,-111,-112,113,114,115,-116,117,-118,119,120,121,122,123,124,-125,-126,-127,128,129,-130,-131,132,133,134,135,-136,-137,-138,-139,140,-141,142,143,144,-145,-146,147,-148,-149,150,]
uf150-010.cnf : SAT [1,2,-3,4,5,-6,7,-8,9,10,11,12,-13,14,15,16,17,-18,-19,20,-21,22,-23,-24,-25,26,-27,28,-29,-30,-31,32,33,34,-35,36,-37,-38,-39,40,41,42,43,-44,-45,46,47,-48,-49,-50,51,-52,53,-54,-55,56,-57,-58,-59,-60,-61,62,-63,64,65,66,-67,-68,-69,-70,-71,72,-73,74,75,-76,-77,-78,-79,80,-81,82,83,84,85,86,87,-88,89,-90,-91,92,-93,94,95,96,-97,-98,99,100,101,102,103,-104,-105,-106,-107,108,109,110,-111,112,113,114,-115,-116,117,118,119,120,121,122,123,124,125,126,127,-128,129,130,131,132,133,134,135,-136,137,138,-139,-140,141,142,143,144,145,146,-147,148,-149,150,]
uf150-012.cnf : SAT [1,-2,3,-4,-5,6,-7,-8,9,-10,11,-12,-13,-14,-15,-16,17,18,-19,20,-21,-22,-23,-24,-25,-26,27,28,29,-30,31,32,-33,34,35,-36,37,38,-39,-40,41,42,43,-44,-45,46,-47,-48,-49,-50,-51,52,-53,54,-55,56,57,58,59,60,-61,-62,-63,-64,65,66,-67,68,-69,70,-71,72,73,-74,75,76,77,-78,-79,80,-81,82,-83,84,85,-86,-87,88,89,-90,-91,92,-93,-94,-95,96,97,-98,99,-100,-101,-102,-103,-104,-105,-106,107,108,109,110,-111,-112,113,-114,115,-116,117,118,119,120,-121,122,123,-124,125,126,-127,128,129,130,131,-132,-133,134,-135,-136,-137,138,139,-140,141,-142,-143,-144,145,-146,147,-148,149,-150,]
uf150-013.cnf : SAT [-1,-2,3,4,-5,-6,-7,-8,9,10,11,12,13,14,15,16,-17,-18,19,20,-21,-22,23,-24,-25,-26,27,-28,29,-30,31,32,-33,34,35,36,-37,38,39,40,-41,-42,43,44,45,-46,-47,48,49,50,51,-52,-53,54,55,56,-57,-58,59,60,-61,-62,63,64,-65,66,-67,-68,69,70,71,-72,73,74,75,76,-77,78,79,80,81,-82,83,84,85,-86,-87,88,89,90,-91,-92,93,94,95,96,97,98,99,-100,101,102,103,104,105,-106,-107,-108,-109,-110,111,112,-113,114,115,116,-117,-118,-119,120,-121,-122,123,-124,125,-126,-127,128,-129,130,-131,132,-133,134,135,136,137,138,-139,140,141,142,143,-144,145,146,147,148,-149,-150,]
uf20-02.cnf : SAT [-1,-2,3,-4,5,6,7,8,9,-10,-11,12,-13,14,15,16,-17,-18,19,-20,]
uf150-03.cnf : SAT [-1,2,-3,4,-5,-6,7,-8,9,-10,-11,12,-13,14,15,-16,17,18,-19,20,21,22,-23,24,-25,26,-27,28,-29,30,31,32,33,34,-35,36,37,38,-39,-40,41,42,43,44,-45,-46,-47,-48,49,-50,51,52,-53,54,55,56,57,58,59,-60,61,62,63,64,-65,66,-67,68,69,70,71,72,-73,-74,-75,-76,77,-78,79,-80,-81,-82,-83,84,85,-86,87,-88,-89,90,-91,-92,93,-94,-95,96,97,98,99,-100,101,-102,-103,104,-105,-106,-107,108,109,-110,111,-112,113,114,115,-116,-117,-118,-119,120,-121,-122,123,124,125,-126,-127,-128,129,-130,131,132,133,-134,-135,-136,-137,138,139,-140,141,142,143,144,-145,146,147,-148,-149,-150,]
uf150-02.cnf : SAT [1,2,3,-4,5,6,7,-8,-9,10,-11,12,-13,14,-15,-16,17,-18,19,20,21,22,23,-24,25,26,-27,28,-29,30,31,32,-33,34,35,36,-37,-38,39,40,41,42,43,44,45,46,47,48,49,-50,-51,52,53,54,-55,-56,57,58,59,60,61,62,-63,-64,-65,66,-67,-68,69,-70,71,-72,73,-74,75,-76,77,78,-79,-80,-81,-82,-83,84,85,86,-87,-88,89,90,91,92,93,94,-95,96,-97,-98,-99,100,101,-102,103,104,105,-106,107,108,109,110,111,-112,113,-114,-115,116,-117,-118,-119,-120,-121,-122,-123,124,-125,126,-127,-128,129,-130,-131,132,-133,-134,135,136,137,138,139,-140,141,-142,143,-144,-145,146,-147,-148,149,150,]
uf20-03.cnf : SAT [1,2,3,4,-5,6,7,8,9,10,11,-12,13,-14,-15,16,17,18,-19,20,]
uf20-01.cnf : SAT [-1,2,3,4,-5,-6,-7,8,9,10,11,-12,-13,14,15,-16,17,18,19,20,]
uuf150-019.cnf : UNSAT
uuf150-018.cnf : UNSAT
uf150-01.cnf : SAT [1,2,-3,4,-5,6,-7,8,9,-10,11,-12,-13,14,-15,-16,17,-18,-19,20,-21,-22,-23,24,-25,26,27,-28,29,-30,31,32,33,34,-35,36,37,38,39,40,41,42,-43,44,45,-46,47,48,-49,-50,-51,52,-53,-54,-55,-56,57,58,59,60,61,-62,63,-64,-65,66,67,68,69,70,-71,-72,-73,-74,-75,76,-77,-78,79,80,-81,82,83,84,85,86,-87,88,-89,90,-91,92,93,94,95,-96,-97,98,99,-100,-101,102,103,-104,-105,106,-107,-108,109,110,111,-112,-113,114,-115,-116,-117,118,119,120,121,122,123,-124,-125,126,127,128,129,130,131,132,133,-134,135,136,137,138,139,-140,141,142,143,144,145,-146,147,148,-149,-150,]
uf20-04.cnf : SAT [1,-2,3,4,-5,-6,7,-8,-9,10,11,-12,13,-14,-15,16,17,-18,-19,-20,]
uf150-05.cnf : SAT [-1,2,-3,-4,5,6,-7,-8,9,10,11,12,13,-14,15,-16,17,-18,19,-20,21,-22,-23,24,25,-26,-27,28,-29,30,31,32,33,-34,-35,-36,37,-38,39,40,-41,42,43,-44,45,46,-47,-48,49,50,51,52,-53,54,55,-56,-57,-58,-59,60,61,-62,-63,-64,-65,66,67,-68,-69,70,71,72,73,-74,-75,-76,77,-78,79,80,81,-82,-83,84,85,86,-87,88,89,-90,-91,-92,-93,94,95,96,97,-98,99,-100,101,-102,103,-104,-105,-106,107,108,109,-110,-111,-112,113,114,-115,-116,117,118,119,-120,-121,-122,-123,-124,125,-126,-127,-128,-129,-130,-131,-132,-133,134,-135,-136,137,138,139,140,-141,-142,143,-144,145,146,-147,148,149,150,]
...
...
...
...
...
uf20-012.cnf : SAT [-1,-2,3,-4,-5,6,-7,8,9,-10,-11,12,13,14,-15,16,17,-18,19,-20,]
uf20-013.cnf : SAT [-1,-2,-3,-4,5,-6,7,8,9,-10,-11,12,-13,-14,-15,16,-17,-18,-19,20,]
uuf150-06.cnf : UNSAT
uuf150-04.cnf : UNSAT
uf20-011.cnf : SAT [1,2,-3,-4,5,6,7,-8,-9,-10,-11,-12,-13,14,15,16,17,18,19,-20,]
uf20-010.cnf : SAT [1,-2,3,4,5,6,-7,-8,9,10,-11,12,13,14,15,-16,-17,-18,19,20,]
uuf150-05.cnf : UNSAT
The ‘argparse’ module is used to create user-friendly command-line interfaces.
Users are provided with two options –
- Run the SAT solver over all files in a folder (taken as parser argument) and get a log file (as shown above)
Usage :python3 SAT_Solver.py --run_benchmarks FOLDER - Run the SAT solver on a DIMACs CNF file and get output in the command-line.
Usage :python3 SAT_Solver.py --input_file FILE
Output when the CNF is satisfiable
s SATISFIABLE
v 1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 15 -16 -17 -18 -19 -20 21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 35 -36 -37 38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 63 -64 -65 -66 -67 -68 -69 70 -71 -72 -73 -74 -75 76 -77 -78 -79 -80 -81 -82 83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 97 -98 -99 -100 -101 -102 -103 -104 -105 -106 107 -108 -109 -110 -111 -112 -113 -114 -115 -116 117 -118 -119 -120 121 -122 -123 -124 -125 -126 127 -128 -129 -130 -131 -132 -133 -134 -135 -136 -137 138 -139 -140 -141 -142 -143 -144 -145 -146 -147 -148 -149 150 -151 -152 -153 -154 -155 -156 -157 158 -159 -160 -161 -162 -163 -164 -165 -166 -167 -168 -169 -170 171 -172 -173 -174 175 -176 -177 -178 -179 -180 -181 -182 -183 -184 185 -186 -187 -188 -189 -190 -191 -192 -193 -194 195 -196 -197 -198 -199 -200 201 -202 -203 -204 -205 -206 -207 -208 -209 -210 -211 -212 -213 214 -215 -216 -217 218 -219 -220 -221 -222 -223 -224 -225 226 -227 -228 -229 -230 -231 -232 -233 -234 -235 -236 -237 -238 -239 -240 -241 242 -243 -244 -245 -246 247 -248 -249 -250 -251 -252 -253 -254 -255 -256 257 -258 -259 -260 -261 -262 -263 -264 -265 -266 267 -268 -269 -270 -271 -272 -273 -274 -275 -276 277 -278 -279 -280 -281 -282 -283 -284 -285 -286 287 -288 -289 290 -291 -292 -293 -294 -295 -296 -297 298 -299 -300 -301 -302 -303 -304 -305 -306 -307 -308 309 -310 -311 -312 -313 -314 -315 -316 -317 -318 -319 -320 -321 -322 -323 324 -325 -326 327 -328 -329 -330 -331 -332 -333 -334 -335 -336 -337 -338 -339 -340 341 -342 343 -344 -345 -346 -347 -348 -349 -350 -351 -352 -353 -354 -355 356 -357 -358 -359 -360 -361 -362 -363 -364 -365 366 -367 -368 -369 -370 -371 -372 -373 -374 -375 -376 -377 378 -379 -380 -381 -382 -383 -384 385 -386 -387 -388 -389 -390 391 -392 -393 -394 -395 -396 -397 398 -399 -400 -401 -402 -403 -404 -405 -406 -407 -408 -409 -410 -411 412 -413 -414 -415 -416 -417 -418 -419 -420 -421 -422 423 -424 425 -426 -427 -428 -429 -430 -431 -432 -433 -434 435 -436 -437 -438 -439 -440 -441 442 -443 -444 -445 -446 -447 -448 -449 -450 -451 -452 -453 454 -455 -456 -457 -458 -459 -460 -461 -462 -463 -464 -465 -466 467 -468 -469 -470 -471 -472 473 -474 -475 -476 -477 -478 -479 -480 -481 -482 483 -484 -485 -486 -487 -488 -489 -490 -491 -492 -493 494 -495 -496 -497 498 -499 -500 -501 -502 -503 -504 -505 -506 -507 -508 -509 -510 -511 -512 513 514 -515 -516 -517 -518 -519 -520 -521 -522 -523 -524 -525 -526 527 -528 -529 -530 -531 -532 -533 -534 -535 -536 537 -538 -539 -540 -541 -542 -543 544 -545 -546 -547 -548 -549 -550 551 -552 -553 -554 -555 -556 -557 -558 -559 -560 -561 -562 -563 -564 565 -566 -567 -568 -569 -570 -571 -572 573 -574 -575 -576 577 -578 -579 -580 -581 -582 -583 -584 -585 -586 -587 -588 589 -590 -591 -592 -593 -594 -595 596 -597 -598 -599 -600 -601 -602 -603 -604 -605 -606 -607 -608 -609 610 -611 -612 -613 -614 -615 -616 -617 -618 -619 620 -621 -622 -623 -624 -625 626 -627 -628 -629 -630 -631 -632 -633 -634 -635 -636 -637 -638 639 -640 -641 642 -643 -644 -645 -646 -647 -648 -649 -650 -651 -652 653 -654 -655 -656 -657 -658 659 -660 -661 -662 -663 -664 -665 -666 -667 -668 -669 -670 -671 -672 673 -674 -675 -676 -677 -678 679 -680 -681 -682 -683 -684 -685 -686 -687 -688 -689 -690 -691 -692 693 -694 -695 696 -697 -698 -699 -700 -701 -702 -703 -704 -705 -706 -707 708 -709 -710 -711 -712 -713 -714 -715 -716 -717 -718 719 -720 721 -722 -723 -724 -725 -726 -727 -728 -729 0
Execution time: 0.45 seconds
Output when the CNF is unsatisfiable
s UNSATISFIABLE
Execution time: 0.00 seconds
To view the help message,
python3 SAT_Solver.py --help
usage: SAT_Solver.py [-h] [--input_file INPUT_FILE] [--run_benchmarks RUN_BENCHMARKS]
SAT Solver based on DPLL Algorithm
-----------------------------------
Returns
1. A model if the formula is satisfiable
2. Reports that the formula is unsatisfiable
optional arguments:
-h, --help show this help message and exit
--input_file INPUT_FILE
runs the sat solver over the input file (must be in DIMACs format)
--run_benchmarks RUN_BENCHMARKS
runs the sat solver over all files in the input folder (provide only the
folder name)
The k-dimensional Sudoku Puzzle Pair Solver and Generator can be found here.