388:, i.e. it contains only a single unassigned literal, this clause can only be satisfied by assigning the necessary value to make this literal true. Thus, no choice is necessary. Unit propagation consists in removing every clause containing a unit clause's literal and in discarding the complement of a unit clause's literal from every clause containing that complement. In practice, this often leads to deterministic cascades of units, thus avoiding a large part of the naive search space.
651:, which is the literal considered in the backtracking step. As a result, this is not exactly an algorithm, but rather a family of algorithms, one for each possible way of choosing the branching literal. Efficiency is strongly affected by the choice of the branching literal: there exist instances for which the running time is constant or exponential depending on the choice of the branching literals. Such choice functions are also called
724:
740:
712:
812:
788:
764:
752:
776:
800:
700:
688:
27:
643:
The pseudocode DPLL function only returns whether the final assignment satisfies the formula or not. In a real implementation, the partial satisfying assignment typically is also returned on success; this can be derived by keeping track of branching literals and of the literal assignments made during
635:
is empty, i.e., it contains no clause. Then it is satisfied by any assignment, as all its clauses are vacuously true. Otherwise, when the formula contains an empty clause, the clause is vacuously false because a disjunction requires at least one member that is true for the overall set to be true. In
412:
Unsatisfiability of a given partial assignment is detected if one clause becomes empty, i.e. if all its variables have been assigned in a way that makes the corresponding literals false. Satisfiability of the formula is detected either when all variables are assigned without generating the empty
367:
to it, simplifying the formula and then recursively checking if the simplified formula is satisfiable; if this is the case, the original formula is satisfiable; otherwise, the same recursive check is done assuming the opposite truth value. This is known as the
372:, as it splits the problem into two simpler sub-problems. The simplification step essentially removes all clauses that become true under the assignment from the formula, and all literals that become false from the remaining clauses.
286:
in 1960. Especially in older publications, the DavisāLogemannāLoveland algorithm is often referred to as the "DavisāPutnam method" or the "DP algorithm". Other common names that maintain the distinction are DLL and DPLL.
408:. A pure literal can always be assigned in a way that makes all clauses containing it true. Thus, when it is assigned in such a way, these clauses do not constrain the search anymore, and can be deleted.
1074:
856:
In the 2010-2019 decade, work on improving the algorithm has found better policies for choosing the branching literals and new data structures to make the algorithm faster, especially the part on
864:(CDCL), which is similar to DPLL but after reaching a conflict "learns" the root causes (assignments to variables) of the conflict, and uses this information to perform
122:
1297:
Gomes, Carla P.; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). "Satisfiability
Solvers". In Van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (eds.).
203:
162:
723:
1135:
Marques-Silva, JoĆ£o P. (1999). "The Impact of
Branching Heuristics in Propositional Satisfiability Algorithms". In Barahona, Pedro; Alferes, JosƩ J. (eds.).
739:
413:
clause, or, in modern implementations, if all clauses are satisfied. Unsatisfiability of the complete formula can only be detected after exhaustive search.
1137:
Progress in
Artificial Intelligence: 9th Portuguese Conference on Artificial Intelligence, EPIA '99 Ćvora, Portugal, September 21ā24, 1999 Proceedings
711:
1314:
1287:
1258:
1221:
1156:
1037:
318:
1338:
332:(1996-1999) was an early implementation using DPLL. In the international SAT competitions, implementations based around DPLL such as
1140:
874:) in order to avoid reaching the same conflict again. Most state-of-the-art SAT solvers are based on the CDCL framework as of 2019.
314:
787:
1333:
861:
811:
763:
300:
751:
344:
296:
256:
244:
64:
576:
are functions that return the result of applying unit propagation and the pure literal rule, respectively, to the literal
534:
401:
918:
775:
263:
169:
128:
81:
275:
375:
The DPLL algorithm enhances over the backtracking algorithm by the eager use of the following rules at each step:
1172:
StƄlmarck, G.; SƤflund, M. (October 1990). "Modeling and
Verifying Systems and Software in Propositional Logic".
968:
842:
609:
340:
663:
Davis, Logemann, Loveland (1961) had developed this algorithm. Some properties of this original algorithm are:
835:
828:
417:
252:
52:
397:
348:
687:
838:
for formula verification was presented and patented. It has found some use in industrial applications.
799:
1343:
232:
427:
DPLL Input: A set of clauses Ī¦. Output: A truth value indicating whether Ī¦ is satisfiable.
352:
248:
1227:
995:
950:
931:
883:
652:
329:
279:
271:
1310:
1283:
1254:
1246:
1217:
1152:
1033:
846:
730:
91:
1302:
1209:
1181:
1144:
1016:
985:
977:
940:
895:
379:
240:
216:
172:
900:
267:
179:
138:
131:
84:
699:
309:
1306:
1185:
1020:
1327:
1231:
963:
922:
681:
An example with visualization of a DPLL algorithm having chronological backtracking:
283:
1065:
999:
954:
745:
Now backtrack to immediate level and by force assign opposite value to that variable
990:
636:
this case, the existence of such a clause implies that the formula (evaluated as a
236:
1301:. Foundations of Artificial Intelligence. Vol. 3. Elsevier. pp. 89ā134.
1213:
1200:
416:
The DPLL algorithm can be summarized in the following pseudocode, where Ī¦ is the
870:
364:
304:
74:
1090:
325:
1148:
882:
Runs of DPLL-based algorithms on unsatisfiable instances correspond to tree
336:
and MiniSat were in the first places of the competitions in 2004 and 2005.
981:
945:
926:
363:
The basic backtracking algorithm runs by choosing a literal, assigning a
1208:. Lecture Notes in Computer Science. Vol. 11628. pp. 250ā266.
717:
Make a decision, variable a = False (0), thus green clauses becomes True
850:
631:
The algorithm terminates in one of two cases. Either the CNF formula
333:
860:. However, the main improvement has been a more powerful algorithm,
677:
use learning or non-chronological backtracking (introduced in 1996).
299:
is important both from theoretical and practical points of view. In
640:
of all clauses) cannot evaluate to true and must be unsatisfiable.
212:
26:
1119:
647:
The DavisāLogemannāLoveland algorithm depends on the choice of
1064:
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesar (2004),
1007:
Ouyang, Ming (1998). "How Good Are
Branching Rules in DPLL?".
1199:
Mƶhle, Sibylle; Biere, Armin (2019). "Backing
Backtracking".
1075:
Logic for
Programming, Artificial Intelligence, and Reasoning
1249:. In Rossi, Francesca; Van Beek, Peter; Walsh, Toby (eds.).
1202:
Theory and
Applications of Satisfiability Testing ā SAT 2019
307:, and can appear in a broad variety of applications such as
562:" terminates the algorithm and outputs the following value.
962:
Davis, Martin; Logemann, George; Loveland, Donald (1961).
620:
denotes the simplified result of substituting "true" for
793:
Make a forced decision, but again it leads to a conflict
769:
Backtrack to previous level and make a forced decision
1105:
757:
But a forced decision still leads to another conflict
182:
141:
94:
817:
Continue in this way and the final implication graph
1030:
Handbook of practical logic and automated reasoning
584:. In other words, they replace every occurrence of
168:
127:
80:
70:
60:
1278:Malay Ganai; Aarti Gupta; Dr. Aarti Gupta (2007).
670:It is the basis for almost all modern SAT solvers.
197:
156:
116:
1066:"Abstract DPLL and Abstract DPLL Modulo Theories"
927:"A Computing Procedure for Quantification Theory"
1280:SAT-based scalable formal verification solutions
339:Another application that often involves DPLL is
781:Make a new decision, but it leads to a conflict
644:unit propagation and pure literal elimination.
1032:. Cambridge University Press. pp. 79ā90.
8:
19:
1121:The international SAT Competitions web page
729:After making several decisions, we find an
596:, and simplify the resulting formula. The
456:, Ī¦); // pure literal elimination:
328:has been a research topic for many years.
989:
944:
181:
140:
105:
93:
282:-based procedure developed by Davis and
1059:
1057:
1053:
964:"A Machine Program for Theorem Proving"
683:
347:(SMT), which is a SAT problem in which
476:, Ī¦); // stopping conditions:
351:are replaced with formulas of another
303:it was the first problem proved to be
18:
831:have also been used for SAT solving.
7:
1299:Handbook of knowledge representation
588:with "true" and every occurrence of
319:diagnosis in artificial intelligence
274:and is a refinement of the earlier
35:, choosing the variable assignment
1251:Handbook of constraint programming
1143:. Vol. 1695. pp. 62ā63.
498:false; // DPLL procedure:
14:
436:(Ī¦) // unit propagation:
315:automated planning and scheduling
43:=1 leads, after unit propagation
1247:"Backtracking search algorithms"
810:
798:
786:
774:
762:
750:
738:
722:
710:
698:
693:All clauses making a CNF formula
686:
291:Implementations and applications
25:
862:Conflict-Driven Clause Learning
866:non-chronological backtracking
827:Since 1986, (Reduced ordered)
345:satisfiability modulo theories
221:DavisāPutnamāLogemannāLoveland
192:
186:
151:
145:
111:
98:
65:Boolean satisfiability problem
1:
1307:10.1016/S1574-6526(07)03002-7
1186:10.1016/S1474-6670(17)52173-4
1021:10.1016/S0166-218X(98)00045-6
404:in the formula, it is called
262:It was introduced in 1961 by
1282:. Springer. pp. 23ā32.
1214:10.1007/978-3-030-24258-9_18
1009:Discrete Applied Mathematics
592:with "false" in the formula
249:propositional logic formulae
841:DPLL has been extended for
805:Backtrack to previous level
491:Ī¦ contains an empty clause
324:As such, writing efficient
245:deciding the satisfiability
31:After 5 fruitless attempts
1360:
1073:Proceedings Int. Conf. on
545:" means that the value of
1339:Automated theorem proving
1253:. Elsevier. p. 122.
969:Communications of the ACM
878:Relation to other notions
843:automated theorem proving
733:that leads to a conflict.
655:or branching heuristics.
610:short-circuiting operator
574:pure-literal-assign(l, Ī¦)
341:automated theorem proving
24:
1245:Van Beek, Peter (2006).
1174:IFAC Proceedings Volumes
829:binary decision diagrams
549:changes to the value of
440:there is a unit clause {
393:Pure literal elimination
117:{\displaystyle O(2^{n})}
16:Type of search algorithm
1149:10.1007/3-540-48159-1_5
991:2027/mdp.39015095248095
349:propositional variables
255:, i.e. for solving the
253:conjunctive normal form
55:formula is satisfiable.
1334:Constraint programming
1028:John Harrison (2009).
667:It is based on search.
464:that occurs pure in Ī¦
398:propositional variable
276:DavisāPutnam algorithm
199:
158:
118:
982:10.1145/368273.368557
946:10.1145/321033.321034
400:occurs with only one
200:
159:
119:
570:unit-propagate(l, Ī¦)
568:In this pseudocode,
198:{\displaystyle O(n)}
180:
157:{\displaystyle O(1)}
139:
92:
886:refutation proofs.
653:heuristic functions
470:pure-literal-assign
460:there is a literal
353:mathematical theory
21:
932:Journal of the ACM
836:StƄlmarck's method
823:Related algorithms
537:. For instance, "
533:"←" denotes
272:Donald W. Loveland
195:
154:
114:
1316:978-0-444-52211-5
1289:978-0-387-69166-4
1260:978-0-444-52726-4
1223:978-3-030-24257-2
1158:978-3-540-66548-9
1106:"Minisat website"
1039:978-0-521-89957-4
847:first-order logic
845:for fragments of
731:implication graph
649:branching literal
563:
554:
384:If a clause is a
301:complexity theory
209:
208:
205:(basic algorithm)
1351:
1320:
1293:
1265:
1264:
1242:
1236:
1235:
1207:
1196:
1190:
1189:
1169:
1163:
1162:
1132:
1126:
1125:
1116:
1110:
1109:
1102:
1096:
1095:
1087:
1081:
1080:
1079:, pp. 36ā50
1070:
1061:
1043:
1024:
1015:(1ā3): 281ā286.
1003:
993:
958:
948:
896:Proof complexity
858:unit propagation
814:
802:
790:
778:
766:
754:
742:
726:
714:
702:
690:
634:
627:
623:
619:
607:
601:
595:
591:
587:
583:
580:and the formula
579:
575:
571:
557:
532:
380:Unit propagation
241:search algorithm
217:computer science
204:
202:
201:
196:
173:space complexity
163:
161:
160:
155:
123:
121:
120:
115:
110:
109:
29:
22:
1359:
1358:
1354:
1353:
1352:
1350:
1349:
1348:
1324:
1323:
1317:
1296:
1290:
1277:
1274:
1272:Further reading
1269:
1268:
1261:
1244:
1243:
1239:
1224:
1205:
1198:
1197:
1193:
1171:
1170:
1166:
1159:
1134:
1133:
1129:
1118:
1117:
1113:
1104:
1103:
1099:
1089:
1088:
1084:
1068:
1063:
1062:
1055:
1040:
1027:
1006:
961:
917:
909:
901:Herbrandization
892:
880:
825:
818:
815:
806:
803:
794:
791:
782:
779:
770:
767:
758:
755:
746:
743:
734:
727:
718:
715:
706:
705:Pick a variable
703:
694:
691:
661:
632:
625:
621:
613:
608:statement is a
603:
597:
593:
589:
585:
581:
577:
573:
569:
566:
529:
428:
361:
293:
268:George Logemann
178:
177:
137:
136:
101:
90:
89:
56:
51:: the top left
17:
12:
11:
5:
1357:
1355:
1347:
1346:
1341:
1336:
1326:
1325:
1322:
1321:
1315:
1294:
1288:
1273:
1270:
1267:
1266:
1259:
1237:
1222:
1191:
1164:
1157:
1127:
1111:
1097:
1092:zChaff website
1082:
1052:
1051:
1045:
1044:
1038:
1025:
1004:
976:(7): 394ā397.
959:
939:(3): 201ā215.
923:Putnam, Hilary
908:
905:
904:
903:
898:
891:
888:
879:
876:
849:by way of the
834:In 1989-1990,
824:
821:
820:
819:
816:
809:
807:
804:
797:
795:
792:
785:
783:
780:
773:
771:
768:
761:
759:
756:
749:
747:
744:
737:
735:
728:
721:
719:
716:
709:
707:
704:
697:
695:
692:
685:
679:
678:
671:
668:
660:
657:
565:
564:
555:
504:choose-literal
450:unit-propagate
429:
423:
422:
410:
409:
394:
390:
389:
382:
370:splitting rule
360:
357:
310:model checking
292:
289:
207:
206:
194:
191:
188:
185:
175:
166:
165:
153:
150:
147:
144:
134:
125:
124:
113:
108:
104:
100:
97:
87:
78:
77:
72:
71:Data structure
68:
67:
62:
58:
57:
30:
15:
13:
10:
9:
6:
4:
3:
2:
1356:
1345:
1342:
1340:
1337:
1335:
1332:
1331:
1329:
1318:
1312:
1308:
1304:
1300:
1295:
1291:
1285:
1281:
1276:
1275:
1271:
1262:
1256:
1252:
1248:
1241:
1238:
1233:
1229:
1225:
1219:
1215:
1211:
1204:
1203:
1195:
1192:
1187:
1183:
1179:
1175:
1168:
1165:
1160:
1154:
1150:
1146:
1142:
1138:
1131:
1128:
1123:
1122:
1115:
1112:
1107:
1101:
1098:
1094:
1093:
1086:
1083:
1078:
1076:
1067:
1060:
1058:
1054:
1050:
1049:
1041:
1035:
1031:
1026:
1022:
1018:
1014:
1010:
1005:
1001:
997:
992:
987:
983:
979:
975:
971:
970:
965:
960:
956:
952:
947:
942:
938:
934:
933:
928:
924:
920:
919:Davis, Martin
916:
915:
914:
913:
906:
902:
899:
897:
894:
893:
889:
887:
885:
877:
875:
873:
872:
867:
863:
859:
854:
852:
848:
844:
839:
837:
832:
830:
822:
813:
808:
801:
796:
789:
784:
777:
772:
765:
760:
753:
748:
741:
736:
732:
725:
720:
713:
708:
701:
696:
689:
684:
682:
676:
672:
669:
666:
665:
664:
659:Visualization
658:
656:
654:
650:
645:
641:
639:
629:
617:
611:
606:
600:
561:
556:
552:
548:
544:
540:
536:
531:
530:
527:
523:
520:
516:
512:
509:
505:
501:
497:
494:
490:
486:
483:
479:
475:
471:
467:
463:
459:
455:
451:
447:
443:
439:
435:
432:
426:
421:
419:
414:
407:
403:
399:
395:
392:
391:
387:
383:
381:
378:
377:
376:
373:
371:
366:
359:The algorithm
358:
356:
354:
350:
346:
342:
337:
335:
331:
327:
322:
320:
316:
312:
311:
306:
302:
298:
290:
288:
285:
284:Hilary Putnam
281:
278:, which is a
277:
273:
269:
265:
260:
258:
254:
250:
246:
242:
238:
234:
230:
226:
222:
218:
214:
189:
183:
176:
174:
171:
167:
148:
142:
135:
133:
130:
126:
106:
102:
95:
88:
86:
83:
79:
76:
73:
69:
66:
63:
59:
54:
50:
47:, to success
46:
42:
38:
34:
28:
23:
1298:
1279:
1250:
1240:
1201:
1194:
1180:(6): 31ā36.
1177:
1173:
1167:
1136:
1130:
1120:
1114:
1100:
1091:
1085:
1072:
1047:
1046:
1029:
1012:
1008:
973:
967:
936:
930:
911:
910:
881:
869:
865:
857:
855:
840:
833:
826:
680:
674:
662:
648:
646:
642:
637:
630:
615:
604:
598:
567:
559:
550:
546:
542:
538:
525:
521:
518:
514:
510:
507:
503:
499:
495:
492:
488:
484:
481:
477:
473:
469:
465:
461:
457:
453:
449:
445:
441:
437:
433:
430:
424:
415:
411:
405:
385:
374:
369:
362:
338:
323:
308:
294:
264:Martin Davis
261:
237:backtracking
228:
224:
220:
210:
48:
44:
40:
36:
32:
1344:SAT solvers
1124:, sat! live
1077:, LPAR 2004
871:backjumping
853:algorithm.
638:conjunction
480:Ī¦ is empty
386:unit clause
365:truth value
326:SAT solvers
305:NP-complete
297:SAT problem
132:performance
85:performance
75:Binary tree
1328:Categories
907:References
884:resolution
535:assignment
487:true;
280:resolution
170:Worst-case
164:(constant)
82:Worst-case
1232:195755607
506:(Ī¦);
425:Algorithm
420:formula:
259:problem.
229:algorithm
129:Best-case
1048:Specific
1000:15866917
955:31888376
925:(1960).
890:See also
675:does not
541:←
431:function
402:polarity
233:complete
45:(bottom)
912:General
851:DPLL(T)
602:in the
547:largest
539:largest
528:{Ā¬l});
444:} in Ī¦
257:CNF-SAT
239:-based
49:(green)
1313:
1286:
1257:
1230:
1220:
1155:
1036:
998:
953:
605:return
560:return
508:return
496:return
485:return
334:zChaff
317:, and
219:, the
1228:S2CID
1206:(PDF)
1069:(PDF)
996:S2CID
951:S2CID
868:(aka
590:not l
517:{l})
458:while
438:while
396:If a
330:GRASP
231:is a
213:logic
61:Class
33:(red)
1311:ISBN
1284:ISBN
1255:ISBN
1218:ISBN
1153:ISBN
1141:LNCS
1034:ISBN
572:and
551:item
543:item
522:DPLL
511:DPLL
493:then
482:then
468:Ī¦ ā
448:Ī¦ ā
434:DPLL
406:pure
295:The
270:and
243:for
225:DPLL
215:and
39:=1,
20:DPLL
1303:doi
1210:doi
1182:doi
1145:doi
1017:doi
986:hdl
978:doi
941:doi
673:It
624:in
618:{l}
524:(Ī¦
513:(Ī¦
418:CNF
343:or
251:in
247:of
211:In
53:CNF
1330::
1309:.
1226:.
1216:.
1178:23
1176:.
1151:.
1139:.
1071:,
1056:^
1013:89
1011:.
994:.
984:.
972:.
966:.
949:.
935:.
929:.
921:;
628:.
614:Ī¦
612:.
599:or
519:or
502:ā
489:if
478:if
466:do
446:do
355:.
321:.
313:,
266:,
235:,
227:)
1319:.
1305::
1292:.
1263:.
1234:.
1212::
1188:.
1184::
1161:.
1147::
1108:.
1042:.
1023:.
1019::
1002:.
988::
980::
974:5
957:.
943::
937:7
633:Ī¦
626:Ī¦
622:l
616:ā§
594:Ī¦
586:l
582:Ī¦
578:l
558:"
553:.
526:ā§
515:ā§
500:l
474:l
472:(
462:l
454:l
452:(
442:l
223:(
193:)
190:n
187:(
184:O
152:)
149:1
146:(
143:O
112:)
107:n
103:2
99:(
96:O
41:b
37:a
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
