443:, we know that we can reduce M to a boolean formula F. Now, each valid assignment of F corresponds to a unique acceptable path in M, and vice versa. However, each acceptable path taken by M represents a solution to A. In other words, there is a bijection between the valid assignments of F and the solutions to A. So, the reduction used in the proof for Cook-Levin Theorem is parsimonious. This implies that #SAT is #P-hard.
22:
380:
to a
Boolean Formula. #SAT is harder than SAT in the sense that, once the total number of solutions to a Boolean formula is known, SAT can be decided in constant time. However, the converse is not true, because knowing a Boolean formula has
511:(FPRAS), even assuming that each variable occurs in at most 6 clauses, but that a fully polynomial-time approximation scheme (FPTAS) exists when each variable occurs in at most 5 clauses: this follows from analogous results on the problem
746:
663:
Weighted model counting (WMC) generalizes #SAT by computing a linear combination of the models instead of just counting the models. In the literal-weighted variant of WMC, each literal gets assigned a weight, such that
451:
Counting solutions is intractable (#P-complete) in many special cases for which satisfiability is tractable (in P), as well as when satisfiability is intractable (NP-complete). This includes the following.
168:, introduced by Valiant in 1979. In other words, it asks in how many ways the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula
555:
This is the counting version of Planar
Monotone Rectilinear 3SAT. The NP-hardness reduction given by de Berg & Khosravi is parsimonious. Therefore, this problem is #P-complete as well.
361:
583:(CNF) formula. Intractability even holds in the case known as #PP2DNF, where the variables are partitioned into two sets, with each clause containing one variable from each set.
127:
199:
535:
is polynomial, counting the number of solutions is #P-complete. This result follows from a general dichotomy characterizing which SAT-like problems are #P-complete.
319:
299:
279:
259:
239:
219:
667:
1048:
889:
508:
547:. The hardness reduction from 3SAT to Planar 3SAT given by Lichtenstein is parsimonious. This implies that Planar #3SAT is #P-complete.
1027:
Suciu, Dan; Olteanu, Dan; Ré, Christopher; Koch, Christoph (2011), Suciu, Dan; Olteanu, Dan; Ré, Christopher; Koch, Christoph (eds.),
472:
form preserving the number of satisfying assignments. Hence, #SAT and #3SAT are counting equivalent and #3SAT is #P-complete as well.
105:
1273:
998:
Computing and
Combinatorics: 16th Annual International Conference, COCOON 2010, Nha Trang, Vietnam, July 19-21, 2010, Proceedings
436:
404:
can be reduced to an instance of the #SAT problem. This is an important result because many difficult counting problems arise in
1268:
604:
417:
516:
366:
43:
586:
By contrast, it is possible to tractably approximate the number of solutions of a disjunctive normal form formula using the
393:
520:
165:
86:
58:
635:
associated to the SAT formula, whose vertices are the variables and where each clause is represented as a hyperedge.
324:
620:
39:
996:; Khosravi, Amirali (2010). "Optimal binary space partitions in the plane". In Thai, My T.; Sahni, Sartaj (eds.).
835:
405:
201:
is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments (
65:
579:, counting the number of solutions of a DNF amounts to counting the number of solutions of the negation of a
813:
751:
WMC is used for probabilistic inference, as probabilistic queries over discrete random variables such as in
644:
580:
564:
504:
469:
413:
32:
72:
1278:
154:
587:
899:
648:
1198:
Chavira, Mark; Darwiche, Adnan (April 2008). "On probabilistic inference by weighted model counting".
1109:
54:
1070:
926:
Creignou, Nadia; Hermann, Miki (1996). "Complexity of
Generalized Satisfiability Counting Problems".
435:
Next, we prove that #SAT is #P-hard. Take any problem #A in #P. We know that A can be solved using a
484:(deciding whether a 2CNF formula has a solution) is polynomial, counting the number of solutions is
576:
532:
409:
1035:, Synthesis Lectures on Data Management, Cham: Springer International Publishing, pp. 45–52,
175:
1234:
1162:
867:
631:. Here, the treewidth can be the primal treewidth, dual treewidth, or incidence treewidth of the
544:
440:
611:
operator, is the only SAT variant for which the #SAT problem can be solved in polynomial time.
400:(read as sharp P complete). In other words, every instance of a problem in the complexity class
1225:
Kimmig, Angelika; Van den Broeck, Guy; De Raedt, Luc (July 2017). "Algebraic model counting".
1180:
1131:
1090:
1044:
885:
623:
parameters, the #SAT problem can become tractable. For instance, #SAT on SAT instances whose
1244:
1207:
1172:
1121:
1082:
1036:
1001:
972:
943:
935:
877:
844:
792:
752:
652:
397:
169:
134:
1013:
429:
1009:
912:
628:
1000:. Lecture Notes in Computer Science. Vol. 6196. Berlin: Springer. pp. 216–225.
863:
830:
304:
284:
264:
244:
224:
204:
158:
79:
1262:
1086:
797:
780:
758:
Algebraic model counting further generalizes #SAT and WMC over arbitrary commutative
488:-complete. The #P-completeness already in the monotone case, i.e., when there are no
162:
1149:
FICHTE, JOHANNES K.; HECHER, MARKUS; THIER, PATRICK; WOLTRAN, STEFAN (2021-03-12).
993:
608:
1211:
1005:
1040:
881:
416:
without any known formula. If a problem is shown to be hard, then it provides a
123:
21:
1150:
741:{\displaystyle {\text{WMC}}(\phi ;w)=\sum _{M\models \phi }\prod _{l\in M}w(l)}
1248:
1176:
1028:
632:
500:
496:
1184:
1135:
1094:
759:
624:
1126:
939:
572:
489:
643:
Model counting is tractable (solvable in polynomial time) for (ordered)
512:
948:
485:
401:
603:
The variant of SAT corresponding to affine relations in the sense of
976:
848:
1167:
1151:"Exploiting Database Management Systems and Treewidth for Counting"
1239:
872:
833:(1979). "The complexity of enumeration and reliability problems".
481:
465:
461:
1071:"Monte-Carlo approximation algorithms for enumeration problems"
963:
Lichtenstein, David (1982). "Planar
Formulae and Their Uses".
571:-complete, even when all clauses have size 2 and there are no
15:
866:. Society for Industrial and Applied Mathematics: 1531–1548.
1110:"Complexity of Generalized Satisfiability Counting Problems"
607:, i.e., where clauses amount to equations modulo 2 with the
1069:
Karp, Richard M; Luby, Michael; Madras, Neal (1989-09-01).
432:. To prove this, first note that #SAT is obviously in #P.
389:, as there are an exponential number of possibilities.
670:
327:
307:
287:
267:
247:
227:
207:
178:
373:
of
Boolean formula. Instead, #SAT asks to enumerate
420:explanation for the lack of nice looking formulas.
46:. Unsourced material may be challenged and removed.
740:
355:
313:
293:
273:
253:
233:
213:
193:
567:(DNF) formulas, counting the solutions is also
356:{\displaystyle a\lor \neg b={\textsf {TRUE}}.}
1108:Creignou, Nadia; Hermann, Miki (1996-02-25).
627:is bounded by a constant can be performed in
619:If the instances to SAT are restricted using
392:#SAT is a well-known example of the class of
8:
781:"The complexity of computing the permanent"
647:and for some circuit formalisms studied in
153:) is the problem of counting the number of
1238:
1166:
1125:
947:
871:
812:Vadhan, Salil Vadhan (20 November 2018).
796:
714:
698:
671:
669:
439:M. On the other hand, from the proof for
345:
344:
343:
326:
306:
286:
266:
246:
226:
206:
177:
106:Learn how and when to remove this message
1155:Theory and Practice of Logic Programming
771:
599:Affine constraint satisfaction problems
464:. One can show that any formula in SAT
908:
897:
639:Restricted circuit and diagram classes
590:, which is an FPRAS for this problem.
118:The correct title of this article is
7:
988:
986:
509:polynomial-time approximation scheme
44:adding citations to reliable sources
862:Liu, Jingcheng; Lu, Pinyan (2015).
369:(SAT), which asks if there exists
334:
185:
14:
864:"FPTAS for Counting Monotone CNF"
551:Planar Monotone Rectilinear #3SAT
503:, #MONOTONE-2-CNF also cannot be
543:This is the counting version of
495:It is known that, assuming that
460:This is the counting version of
437:Non-deterministic Turing Machine
20:
814:"Lecture 24: Counting Problems"
31:needs additional citations for
1029:"The Query Evaluation Problem"
735:
729:
688:
676:
367:Boolean satisfiability problem
1:
1212:10.1016/j.artint.2007.11.002
1087:10.1016/0196-6774(89)90038-2
1006:10.1007/978-3-642-14031-0_25
798:10.1016/0304-3975(79)90044-6
785:Theoretical Computer Science
605:Schaefer's dichotomy theorem
194:{\displaystyle a\lor \neg b}
139:Sharp Satisfiability Problem
1114:Information and Computation
1041:10.1007/978-3-031-01879-4_3
928:Information and Computation
882:10.1137/1.9781611973730.101
412:, Network Reliability, and
172:. For example, the formula
1295:
515:of counting the number of
385:does not help us to count
122:. The substitution of the
117:
1249:10.1016/j.jal.2016.11.031
1177:10.1017/s147106842100003x
965:SIAM Journal on Computing
836:SIAM Journal on Computing
447:Intractable special cases
406:Enumerative Combinatorics
1227:Journal of Applied Logic
1274:Satisfiability problems
1200:Artificial Intelligence
1033:Probabilistic Databases
755:can be reduced to WMC.
594:Tractable special cases
581:conjunctive normal form
565:disjunctive normal form
531:Similarly, even though
414:Artificial intelligence
365:#SAT is different from
1269:Computational problems
1127:10.1006/inco.1996.0016
940:10.1006/inco.1996.0016
907:Cite journal requires
779:Valiant, L.G. (1979).
742:
575:: this is because, by
568:
357:
315:
295:
275:
255:
235:
215:
195:
128:technical restrictions
1075:Journal of Algorithms
743:
649:knowledge compilation
358:
316:
296:
276:
256:
236:
216:
196:
668:
418:complexity theoretic
325:
305:
285:
265:
245:
225:
205:
176:
40:improve this article
588:Karp-Luby algorithm
533:Horn-satisfiability
492:(#MONOTONE-2-CNF).
410:Statistical physics
831:Valiant, Leslie G.
738:
725:
709:
499:is different from
468:as a formula in 3-
441:Cook-Levin Theorem
353:
311:
291:
271:
251:
231:
211:
191:
141:(sometimes called
1050:978-3-031-01879-4
891:978-1-61197-374-7
710:
694:
674:
615:Bounded treewidth
394:counting problems
387:all the solutions
347:
321:= TRUE), we have
314:{\displaystyle b}
294:{\displaystyle a}
274:{\displaystyle b}
254:{\displaystyle a}
234:{\displaystyle b}
214:{\displaystyle a}
170:evaluates to TRUE
116:
115:
108:
90:
1286:
1253:
1252:
1242:
1222:
1216:
1215:
1206:(6–7): 772–799.
1195:
1189:
1188:
1170:
1146:
1140:
1139:
1129:
1105:
1099:
1098:
1066:
1060:
1059:
1058:
1057:
1024:
1018:
1017:
990:
981:
980:
960:
954:
953:
951:
923:
917:
916:
910:
905:
903:
895:
875:
859:
853:
852:
827:
821:
820:
818:
809:
803:
802:
800:
776:
753:baysian networks
747:
745:
744:
739:
724:
708:
675:
672:
577:De Morgan's laws
517:independent sets
466:can be rewritten
362:
360:
359:
354:
349:
348:
320:
318:
317:
312:
300:
298:
297:
292:
280:
278:
277:
272:
260:
258:
257:
252:
240:
238:
237:
232:
220:
218:
217:
212:
200:
198:
197:
192:
135:computer science
111:
104:
100:
97:
91:
89:
48:
24:
16:
1294:
1293:
1289:
1288:
1287:
1285:
1284:
1283:
1259:
1258:
1257:
1256:
1224:
1223:
1219:
1197:
1196:
1192:
1148:
1147:
1143:
1107:
1106:
1102:
1068:
1067:
1063:
1055:
1053:
1051:
1026:
1025:
1021:
992:
991:
984:
977:10.1137/0211025
962:
961:
957:
925:
924:
920:
906:
896:
892:
861:
860:
856:
849:10.1137/0208032
829:
828:
824:
816:
811:
810:
806:
778:
777:
773:
768:
666:
665:
661:
659:Generalizations
641:
629:polynomial time
617:
601:
596:
561:
553:
541:
529:
478:
458:
449:
426:
424:#P-Completeness
323:
322:
303:
302:
283:
282:
281:= FALSE), and (
263:
262:
243:
242:
223:
222:
203:
202:
174:
173:
155:interpretations
131:
112:
101:
95:
92:
49:
47:
37:
25:
12:
11:
5:
1292:
1290:
1282:
1281:
1276:
1271:
1261:
1260:
1255:
1254:
1217:
1190:
1161:(1): 128–157.
1141:
1100:
1081:(3): 429–448.
1061:
1049:
1019:
982:
971:(2): 329–343.
955:
918:
909:|journal=
890:
854:
843:(3): 410–421.
822:
804:
791:(2): 189–201.
770:
769:
767:
764:
737:
734:
731:
728:
723:
720:
717:
713:
707:
704:
701:
697:
693:
690:
687:
684:
681:
678:
660:
657:
640:
637:
616:
613:
600:
597:
595:
592:
560:
557:
552:
549:
540:
537:
528:
525:
477:
474:
457:
454:
448:
445:
425:
422:
352:
342:
339:
336:
333:
330:
310:
290:
270:
250:
230:
210:
190:
187:
184:
181:
151:model counting
114:
113:
28:
26:
19:
13:
10:
9:
6:
4:
3:
2:
1291:
1280:
1279:Combinatorics
1277:
1275:
1272:
1270:
1267:
1266:
1264:
1250:
1246:
1241:
1236:
1232:
1228:
1221:
1218:
1213:
1209:
1205:
1201:
1194:
1191:
1186:
1182:
1178:
1174:
1169:
1164:
1160:
1156:
1152:
1145:
1142:
1137:
1133:
1128:
1123:
1119:
1115:
1111:
1104:
1101:
1096:
1092:
1088:
1084:
1080:
1076:
1072:
1065:
1062:
1052:
1046:
1042:
1038:
1034:
1030:
1023:
1020:
1015:
1011:
1007:
1003:
999:
995:
994:de Berg, Mark
989:
987:
983:
978:
974:
970:
966:
959:
956:
950:
945:
941:
937:
933:
929:
922:
919:
914:
901:
893:
887:
883:
879:
874:
869:
865:
858:
855:
850:
846:
842:
838:
837:
832:
826:
823:
815:
808:
805:
799:
794:
790:
786:
782:
775:
772:
765:
763:
761:
756:
754:
749:
732:
726:
721:
718:
715:
711:
705:
702:
699:
695:
691:
685:
682:
679:
658:
656:
654:
650:
646:
638:
636:
634:
630:
626:
622:
614:
612:
610:
606:
598:
593:
591:
589:
584:
582:
578:
574:
570:
566:
558:
556:
550:
548:
546:
538:
536:
534:
526:
524:
522:
518:
514:
510:
506:
502:
498:
493:
491:
487:
483:
475:
473:
471:
467:
463:
455:
453:
446:
444:
442:
438:
433:
431:
423:
421:
419:
415:
411:
407:
403:
399:
395:
390:
388:
384:
379:
378:the solutions
376:
372:
368:
363:
350:
340:
337:
331:
328:
308:
288:
268:
248:
228:
208:
188:
182:
179:
171:
167:
164:
160:
156:
152:
148:
144:
140:
136:
129:
125:
121:
110:
107:
99:
88:
85:
81:
78:
74:
71:
67:
64:
60:
57: –
56:
52:
51:Find sources:
45:
41:
35:
34:
29:This article
27:
23:
18:
17:
1230:
1226:
1220:
1203:
1199:
1193:
1158:
1154:
1144:
1117:
1113:
1103:
1078:
1074:
1064:
1054:, retrieved
1032:
1022:
997:
968:
964:
958:
931:
927:
921:
900:cite journal
857:
840:
834:
825:
807:
788:
784:
774:
757:
750:
662:
642:
618:
602:
585:
562:
554:
542:
539:Planar #3SAT
530:
505:approximated
494:
480:Even though
479:
459:
450:
434:
427:
391:
386:
382:
377:
374:
370:
364:
150:
146:
142:
138:
132:
119:
102:
93:
83:
76:
69:
62:
50:
38:Please help
33:verification
30:
1120:(1): 1–12.
949:10068/41883
545:Planar 3SAT
507:by a fully
430:#P-complete
398:#P-complete
396:, known as
241:= FALSE), (
55:"Sharp-SAT"
1263:Categories
1168:2001.04191
1056:2023-09-16
766:References
651:, such as
633:hypergraph
383:a solution
371:a solution
126:is due to
66:newspapers
1240:1211.4475
1233:: 46–62.
1185:1471-0684
1136:0890-5401
1095:0196-6774
873:1311.3728
760:semirings
719:∈
712:∏
706:ϕ
703:⊨
696:∑
680:ϕ
625:treewidth
573:negations
527:#Horn-SAT
490:negations
335:¬
332:∨
261:= FALSE,
221:= TRUE,
186:¬
183:∨
143:Sharp-SAT
96:June 2019
934:: 1–12.
428:#SAT is
301:= TRUE,
161:a given
1014:2720098
653:d-DNNFs
166:formula
163:Boolean
159:satisfy
80:scholar
1183:
1134:
1093:
1047:
1012:
888:
521:graphs
137:, the
82:
75:
68:
61:
53:
1235:arXiv
1163:arXiv
868:arXiv
817:(PDF)
621:graph
476:#2SAT
456:#3SAT
157:that
87:JSTOR
73:books
1181:ISSN
1132:ISSN
1091:ISSN
1045:ISBN
969:11:2
913:help
886:ISBN
645:BDDs
563:For
559:#DNF
482:2SAT
462:3SAT
346:TRUE
147:#SAT
120:#SAT
59:news
1245:doi
1208:doi
1204:172
1173:doi
1122:doi
1118:125
1083:doi
1037:doi
1002:doi
973:doi
944:hdl
936:doi
932:125
878:doi
845:doi
793:doi
673:WMC
609:XOR
519:in
513:♯IS
470:CNF
375:all
149:or
133:In
42:by
1265::
1243:.
1231:22
1229:.
1202:.
1179:.
1171:.
1159:22
1157:.
1153:.
1130:.
1116:.
1112:.
1089:.
1079:10
1077:.
1073:.
1043:,
1031:,
1010:MR
1008:.
985:^
967:.
942:.
930:.
904::
902:}}
898:{{
884:.
876:.
839:.
787:.
783:.
762:.
748:.
655:.
569:#P
523:.
501:RP
497:NP
486:#P
408:,
402:#P
145:,
1251:.
1247::
1237::
1214:.
1210::
1187:.
1175::
1165::
1138:.
1124::
1097:.
1085::
1039::
1016:.
1004::
979:.
975::
952:.
946::
938::
915:)
911:(
894:.
880::
870::
851:.
847::
841:8
819:.
801:.
795::
789:8
736:)
733:l
730:(
727:w
722:M
716:l
700:M
692:=
689:)
686:w
683:;
677:(
351:.
341:=
338:b
329:a
309:b
289:a
269:b
249:a
229:b
209:a
189:b
180:a
130:.
124:#
109:)
103:(
98:)
94:(
84:·
77:·
70:·
63:·
36:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
