633:
331:
583:
254:
233:
202:
923:(ASP)(actually, identical, after my quick skim). However, ASP doesn't have quantifiers. But then we read that many SMT solvers don't support/have quantifiers either. So at least, this level, ASP and SMT have a lot of similarity, in terms of both expressiveness, and presumably also in speed/performance (as they get based on the same/similar algos). So .. what, precisely is the difference?
680:
985:
in hardware/software. From what I can tell, though, the theories of bitvectors & arrays, etc. can be reduced to uninterpreted predicate logic formulas (I'd really like to know if I'm wrong or right on this). If so, then I'd expect comparable performance (for satisfiability) for both ASP and SMT
865:
to describe a family of historically and culturally different but similar technologies (MiniZinc and friends) which typically operate on discrete variable domains. I am planning to "keep with the trouble" and try to faithfully describe this at some point, but haven't gotten to it yet. AFAICT there
792:
I think that the first 2 sentences in the section titled "SMT Solver
Approaches" are misplaced. The approach described is decidedly NOT SMT - its how you would solve the problem if you didnt have an SMT solver. I think it belongs under a motivation section or perhaps in the introduction
352:
164:
723:
I don't think the decidability of the underlying theories is relevant to whether a formula is or is not an SMT instance. SMT solvers like
Simplify and CVC incorporate semidecision procedures for quantified arithmetic formulas.
707:
I think the article should be more precise on what formulas can be instances of a SMT. For example, satisfiability of formulas in first order predicate logic is undecidable. The same is true for first-order arithmetic over N.
950:
atisfiability, a "yes" or "no" decision problem, whereas ASP is about finding a set of satisfying models. Some SMT solvers can produce models for satisfiable formulas, but this is a rare, experimental feature. Second, SMT is
1015:
I think the anonymous user is an example of why the bold face here is highly confusing. I doubt readers understand what it is indicating in this case, whether they followed the redirect to get to this page or not.
376:
857:
I realise that I am gravedigging here, but this is an excellent question that should be answered by the article. My take on this is that constraint programming is used rather confusingly
1038:
Another option would be to bold CVC4 in the lead to the article, currently it's plain text, and to move the redirect there. But I think I would favor adding a small subsection on CVC4.
516:
158:
55:
742:
I see. I got confused because further down is written "Most of the common SMT approaches support decidable theories". So I'm interested in what these theories are, apart from SAT.
433:
371:
1121:
304:
294:
1126:
1116:
270:
478:
90:
819:
I think we should probably just delete the CVC article and information rather than copy-and-paste it into this one. It's out of place where it is now.
1131:
861:
to describe constraint problems, of which SMT is a formalisation I would say (though it may also be seen as a formalisation of other things I guess),
452:
317:
261:
238:
541:
179:
96:
146:
743:
424:
896:
800:
645:
405:
140:
497:
110:
41:
591:
115:
35:
31:
136:
85:
1082:
I'm not sure I personally have enough info to write about it. Also, it seems that there was previously an article on CVC:
462:
343:
213:
1023:
if we had a specific subsection titled CVC4, dedicated to the solver. I wouldn't be opposed to adding such a section.
960:
472:
386:
186:
76:
1065:
507:
269:
related articles on
Knowledge. If you would like to participate, please visit the project page, where you can join
534:
1098:
1043:
1028:
674:
201:
900:
747:
152:
120:
1056:
If you have sufficient information to write about CVC4, this would be the best. Could you put your text at
920:
912:
871:
839:
804:
981:
Hmm, yes. Many of the SMT solvers focus on bitvectors and arrays & etc. so that they can be used for
959:
heories: the solvers incorporate special-purpose procedures for interpreted functions and constants from
1061:
1010:
713:
443:
219:
709:
892:
847:
843:
796:
658:
587:
1094:
1039:
1024:
982:
172:
66:
17:
968:
824:
773:
729:
81:
867:
362:
62:
1102:
1069:
1047:
1032:
1020:
995:
972:
932:
904:
875:
851:
828:
808:
777:
751:
733:
717:
414:
266:
991:
928:
632:
488:
330:
353:
Requested articles/Applied arts and sciences/Computer science, computing, and
Internet
1110:
964:
886:
Another SMT solver, which should listed there is MiniSmt. Here is the external link:
820:
769:
765:
725:
887:
652:
1091:
https://en.wikipedia.org/search/?title=CVC_(theorem_prover)&action=history
987:
924:
395:
253:
232:
963:. AFAICT, ASP works strictly on uninterpreted predicate logic formulas.
919:
The section that defines "basic terms" makes SMT sound a whole lot like
866:
are also no good sociological sources to verify this sort of thing. --
768:
for a sample of what kinds of formulas SMT solver can work with.
1057:
938:
There's a connection, but there's two big differences with ASP:
573:
471:
Find pictures for the biographies of computer scientists (see
195:
26:
842:? Is it the same thing invented by a different community?
986:
when working on hardware/software design verification...
1090:
615:
609:
603:
597:
171:
265:, a collaborative effort to improve the coverage of
1093:that got deleted/merged. (See talk section above.)
651:* Describe input formats for SMT solvers, such as
377:Computer science articles needing expert attention
44:for general discussion of the article's subject.
517:WikiProject Computer science/Unreferenced BLPs
185:
8:
1060:, thus turning the redirect into a stub? -
669:List a few prominent theories with examples
434:Computer science articles without infoboxes
372:Computer science articles needing attention
199:
640:Here are some tasks awaiting attention:
338:Here are some tasks awaiting attention:
312:
227:
673:Explain the relationship between SMT and
657:Describe satisifiability modulo theories
1122:Low-importance Computer science articles
229:
1019:I think it would make sense to follow
279:Knowledge:WikiProject Computer science
1127:WikiProject Computer science articles
1117:Start-Class Computer science articles
282:Template:WikiProject Computer science
7:
259:This article is within the scope of
834:relation to constraint programming?
218:It is of interest to the following
34:for discussing improvements to the
18:Talk:Satisfiability Modulo Theories
666:Update and prune the solvers table
453:Timeline of computing 2020–present
25:
479:Computing articles needing images
1132:Knowledge pages with to-do lists
678:
663:Insert previous SMT-COMP results
631:
581:
329:
252:
231:
200:
56:Click here to start a new topic.
299:This article has been rated as
592:Satisfiability modulo theories
36:Satisfiability modulo theories
1:
1103:05:04, 11 December 2021 (UTC)
905:08:47, 22 February 2011 (UTC)
533:Tag all relevant articles in
273:and see a list of open tasks.
53:Put new text under old text.
1070:19:22, 9 December 2021 (UTC)
1048:16:53, 9 December 2021 (UTC)
1033:16:42, 9 December 2021 (UTC)
876:09:49, 20 October 2020 (UTC)
778:03:24, 11 October 2008 (UTC)
542:WikiProject Computer science
318:WikiProject Computer science
262:WikiProject Computer science
809:23:05, 1 January 2013 (UTC)
752:13:16, 9 October 2008 (UTC)
734:16:53, 8 October 2008 (UTC)
718:16:28, 7 October 2008 (UTC)
473:List of computer scientists
61:New to Knowledge? Welcome!
1148:
946:. :-) First, SMT is about
852:01:33, 15 March 2010 (UTC)
305:project's importance scale
996:21:00, 15 June 2011 (UTC)
973:21:11, 11 June 2011 (UTC)
675:automated theorem provers
535:Category:Computer science
311:
298:
285:Computer science articles
247:
226:
91:Be welcoming to newcomers
933:19:35, 9 June 2011 (UTC)
829:14:15, 6 June 2008 (UTC)
537:and sub-categories with
921:answer set programming
913:answer set programming
840:constraint programming
838:How is SMT related to
766:SMT-LIB list of logics
659:for higher-order logic
498:Computer science stubs
208:This article is rated
86:avoid personal attacks
788:Misplaced description
111:Neutral point of view
316:Things you can help
116:No original research
983:formal verification
961:background theories
764:Take a look at the
621:Updated 2024-01-27
214:content assessment
97:dispute resolution
58:
895:comment added by
799:comment added by
703:Basic terminology
700:
699:
694:
693:
572:
571:
568:
567:
564:
563:
560:
559:
556:
555:
194:
193:
77:Assume good faith
54:
16:(Redirected from
1139:
1062:Jochen Burghardt
1021:MOS:BOLDREDIRECT
1014:
1011:Jochen Burghardt
907:
811:
685:
682:
681:
635:
628:
627:
622:
585:
584:
574:
546:
540:
415:Computer science
344:Article requests
333:
326:
325:
313:
287:
286:
283:
280:
277:
276:Computer science
267:Computer science
256:
249:
248:
243:
239:Computer science
235:
228:
211:
205:
204:
196:
190:
189:
175:
106:Article policies
27:
21:
1147:
1146:
1142:
1141:
1140:
1138:
1137:
1136:
1107:
1106:
1008:
1006:
917:
890:
884:
836:
817:
794:
790:
705:
696:
695:
690:
683:
679:
596:
582:
552:
549:
544:
538:
526:Project-related
521:
502:
483:
457:
438:
419:
400:
381:
357:
284:
281:
278:
275:
274:
241:
212:on Knowledge's
209:
132:
127:
126:
125:
102:
72:
23:
22:
15:
12:
11:
5:
1145:
1143:
1135:
1134:
1129:
1124:
1119:
1109:
1108:
1095:Caleb Stanford
1088:
1087:
1086:
1085:
1084:
1083:
1075:
1074:
1073:
1072:
1051:
1050:
1040:Caleb Stanford
1025:Caleb Stanford
1005:
1002:
1001:
1000:
999:
998:
976:
975:
916:
909:
883:
880:
879:
878:
835:
832:
816:
813:
789:
786:
785:
784:
783:
782:
781:
780:
757:
756:
755:
754:
737:
736:
704:
701:
698:
697:
692:
691:
689:
688:
687:
686:
670:
667:
664:
661:
639:
637:
636:
624:
579:
577:
570:
569:
566:
565:
562:
561:
558:
557:
554:
553:
551:
550:
548:
547:
530:
522:
520:
519:
513:
503:
501:
500:
494:
484:
482:
481:
476:
468:
458:
456:
455:
449:
439:
437:
436:
430:
420:
418:
417:
411:
401:
399:
398:
392:
382:
380:
379:
374:
368:
358:
356:
355:
349:
337:
335:
334:
322:
321:
309:
308:
301:Low-importance
297:
291:
290:
288:
271:the discussion
257:
245:
244:
242:Low‑importance
236:
224:
223:
217:
206:
192:
191:
129:
128:
124:
123:
118:
113:
104:
103:
101:
100:
93:
88:
79:
73:
71:
70:
59:
50:
49:
46:
45:
39:
24:
14:
13:
10:
9:
6:
4:
3:
2:
1144:
1133:
1130:
1128:
1125:
1123:
1120:
1118:
1115:
1114:
1112:
1105:
1104:
1100:
1096:
1092:
1081:
1080:
1079:
1078:
1077:
1076:
1071:
1067:
1063:
1059:
1055:
1054:
1053:
1052:
1049:
1045:
1041:
1037:
1036:
1035:
1034:
1030:
1026:
1022:
1017:
1012:
1004:CVC4 redirect
1003:
997:
993:
989:
984:
980:
979:
978:
977:
974:
970:
966:
962:
958:
954:
949:
945:
941:
937:
936:
935:
934:
930:
926:
922:
914:
910:
908:
906:
902:
898:
894:
889:
881:
877:
873:
869:
864:
860:
856:
855:
854:
853:
849:
845:
841:
833:
831:
830:
826:
822:
814:
812:
810:
806:
802:
798:
787:
779:
775:
771:
767:
763:
762:
761:
760:
759:
758:
753:
749:
745:
744:194.39.218.10
741:
740:
739:
738:
735:
731:
727:
722:
721:
720:
719:
715:
711:
702:
677:
676:
671:
668:
665:
662:
660:
656:
655:
654:
650:
648:
647:
642:
641:
638:
634:
630:
629:
626:
623:
620:
617:
614:
611:
608:
605:
602:
599:
595:
593:
589:
578:
576:
575:
543:
536:
532:
531:
529:
527:
523:
518:
515:
514:
512:
510:
509:
504:
499:
496:
495:
493:
491:
490:
485:
480:
477:
474:
470:
469:
467:
465:
464:
459:
454:
451:
450:
448:
446:
445:
440:
435:
432:
431:
429:
427:
426:
421:
416:
413:
412:
410:
408:
407:
402:
397:
394:
393:
391:
389:
388:
383:
378:
375:
373:
370:
369:
367:
365:
364:
359:
354:
351:
350:
348:
346:
345:
340:
339:
336:
332:
328:
327:
324:
323:
319:
315:
314:
310:
306:
302:
296:
293:
292:
289:
272:
268:
264:
263:
258:
255:
251:
250:
246:
240:
237:
234:
230:
225:
221:
215:
207:
203:
198:
197:
188:
184:
181:
178:
174:
170:
166:
163:
160:
157:
154:
151:
148:
145:
142:
138:
135:
134:Find sources:
131:
130:
122:
121:Verifiability
119:
117:
114:
112:
109:
108:
107:
98:
94:
92:
89:
87:
83:
80:
78:
75:
74:
68:
64:
63:Learn to edit
60:
57:
52:
51:
48:
47:
43:
37:
33:
29:
28:
19:
1089:
1018:
1007:
956:
952:
947:
943:
939:
918:
911:Relation to
897:87.5.110.199
885:
868:Planetwrench
862:
858:
837:
818:
801:67.198.70.33
795:— Preceding
791:
706:
672:
644:
643:
625:
618:
612:
606:
600:
586:
580:
525:
524:
508:Unreferenced
506:
505:
487:
486:
461:
460:
442:
441:
423:
422:
404:
403:
385:
384:
361:
360:
342:
341:
300:
260:
220:WikiProjects
182:
176:
168:
161:
155:
149:
143:
133:
105:
30:This is the
891:—Preceding
710:Borishollas
210:Start-class
159:free images
42:not a forum
1111:Categories
844:Eclecticos
588:To-do list
815:CVC merge
396:Computing
99:if needed
82:Be polite
32:talk page
965:Clconway
893:unsigned
821:Clconway
797:unsigned
770:Clconway
726:Clconway
444:Maintain
387:Copyedit
67:get help
40:This is
38:article.
888:MiniSmt
882:MiniSmt
653:SMT-LIB
616:refresh
604:history
425:Infobox
363:Cleanup
303:on the
165:WP refs
153:scholar
955:odulo
646:Expand
406:Expand
216:scale.
137:Google
988:linas
925:linas
610:watch
489:Stubs
463:Photo
320:with:
180:JSTOR
141:books
95:Seek
1099:talk
1066:talk
1058:CVC4
1044:talk
1029:talk
992:talk
969:talk
942:and
929:talk
901:talk
872:talk
859:both
848:talk
825:talk
805:talk
774:talk
748:talk
730:talk
714:talk
598:edit
590:for
173:FENS
147:news
84:and
863:and
295:Low
187:TWL
1113::
1101:)
1068:)
1046:)
1031:)
994:)
971:)
944:MT
931:)
903:)
874:)
850:)
827:)
807:)
776:)
750:)
732:)
716:)
708:--
545:}}
539:{{
167:)
65:;
1097:(
1064:(
1042:(
1027:(
1013::
1009:@
990:(
967:(
957:T
953:M
948:S
940:S
927:(
915:?
899:(
870:(
846:(
823:(
803:(
772:(
746:(
728:(
712:(
684:Y
649::
619:·
613:·
607:·
601:·
594::
528::
511::
492::
475:)
466::
447::
428::
409::
390::
366::
347::
307:.
222::
183:·
177:·
169:·
162:·
156:·
150:·
144:·
139:(
69:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
