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