{"entities":{"Q428887":{"pageid":430654,"ns":120,"title":"Item:Q428887","lastrevid":61766232,"modified":"2026-04-11T01:31:30Z","type":"item","id":"Q428887","labels":{"en":{"language":"en","value":"A pearl on SAT and SMT solving in Prolog"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6049400"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$43B70D07-9258-4958-A406-2204BF0E423D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bee0d550f96f4f71360ea3f2cc46d0fff068693b","datavalue":{"value":{"text":"A pearl on SAT and SMT solving in Prolog","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q428887$92D24DAD-00CC-4E7D-A1A4-F3CBEEB3DAF1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bfac50278b551e7a615e7bee99a605825faccd49","datavalue":{"value":"1248.68455","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q428887$30C68268-EA08-4C8B-8BCB-A8479E23D4EB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b78be09e060d47a3be0e8316b77e796d8d6efd97","datavalue":{"value":{"entity-type":"item","numeric-id":294782,"id":"Q294782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$3E398E4E-13DC-468F-B318-BE61A63CDE5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3398e52dfa611cfbebe7884f888145f10a6bb45a","datavalue":{"value":{"entity-type":"item","numeric-id":294783,"id":"Q294783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$BAF48825-56E8-4A85-BC53-0649D20CE825","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$A7A08E76-7EBA-4269-9D34-A6E0D54CDA1A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f72164bd681bf7e905e9de5f982349bc17f0310f","datavalue":{"value":{"time":"+2012-06-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q428887$9CB5DEED-CA33-43E0-878B-EC123B8EF7A3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"62ad8ff266935f1167d13df42b6c5172ee444e64","datavalue":{"value":"A succinct and elegant solver of twenty two Prolog clauses for the Boolean satisfiability problem (SAT solver) is presented. The brevity of the program is achieved using Prolog to transform a propositional formula into a conjunctive normal form (CNF). The match between Prolog, SAT, Davis-Putnam-Logeman-Loveland (DPLL) algorithm with watched literals -- one of the most power features in speeding up SAT solvers -- promotes a lot the author's success. The solver provides an easy entry into the SAT and SAT modulo theories (SMT). The SAT solver exploits the control provided by delay declarations to implement watched literals and unit propagation. The SAT solver can be integrated into an SMT framework which uses the constraint solvers that are available in many Prolog systems. The presented SAT solver is not going to be competitive on large, difficult problems set as challenges in the international SAT and SMT competitions. Nevertheless, the solver does provide a declarative description of SAT solving with watched literals in a succinct and self-contained manner, and one which can be extended in a number of ways. For instance, its incorporation into an SMT scheme using the constraint packages often distributed with Prolog systems gives a straightforward realization of the theory of linear real arithmetic.","type":"string"},"datatype":"string"},"type":"statement","id":"Q428887$76ACB770-047D-4162-A361-68B15461E9B7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q428887$68F982BA-2E3A-4E9C-A4F7-B06681D4B7DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b492f281b8f52c724f2bc547e7e570cccf4bd5e0","datavalue":{"value":"68N17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q428887$FFA4CF47-CBDD-46F8-AF93-B7A3ACC1D3F9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"677a39a132f1e1363a038792cc253c5ef9ff9d4c","datavalue":{"value":"6049400","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q428887$E919369D-ACCB-4860-8D22-AD5099E3756E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87021f83c0bc2bfb13b38866d6825671687cfc77","datavalue":{"value":"SAT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q428887$396BADDB-C058-4D50-BBFE-160FA1DD1C74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dac36a0d5bcef050bd5c5ec480998b0eb01458a6","datavalue":{"value":"SMT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q428887$C9CE80CF-B698-4EC2-8E5F-07378773FEF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff67fedbe8c50d3daca036875aed531217cd953b","datavalue":{"value":"Prolog","type":"string"},"datatype":"string"},"type":"statement","id":"Q428887$FA3E8E9B-2F28-4B6D-843A-FE7EB60A093F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ae3f0d13ad92818eaf45462f9d67f2d319a5148","datavalue":{"value":"constraint logic programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q428887$21F62351-F77A-4ACC-9B4D-D61E9CCAD074","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b5f32448630df5dd2a9e1e0e1fee17cf18ba16e7","datavalue":{"value":"delay declarations","type":"string"},"datatype":"string"},"type":"statement","id":"Q428887$C051580F-6F9C-4C80-B100-3C00DDE282F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba65afbaf22dc20002e9adb588721a9231352199","datavalue":{"value":"watched literal","type":"string"},"datatype":"string"},"type":"statement","id":"Q428887$0C3C2CDC-B49F-46F5-B00A-7949C25547B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"55fd841e56aa22d3b4f3d5a7e5817ed86272bf5f","datavalue":{"value":"unit propagation","type":"string"},"datatype":"string"},"type":"statement","id":"Q428887$4335DA53-8977-4025-99CA-2615AF23189C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$D0E09C38-7131-473E-AA84-0740473DF487","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$944B6C96-1820-455A-B946-402255904834","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$01FCE26F-8960-49DD-8836-06DB1202C6DC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"67fe79cb461fb255aa395379fc8a6a4b6b5a97a0","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2012.02.024","type":"string"},"datatype":"url"},"type":"statement","id":"Q428887$0CF12093-0051-4504-9C82-4952234DC59C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"45d7c85c12e4a8bb028393c0362780150a5a27c6","datavalue":{"value":"W2121531736","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q428887$99576235-8327-41E2-9242-42AE2BD8FB5D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c527e263525faa34ac4a72501bf8563b41ad015a","datavalue":{"value":{"entity-type":"item","numeric-id":4297316,"id":"Q4297316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$69F80034-6A02-48B0-92B9-EFEA6CFA34EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1554dfab5cf085f69f00324d9012f1eda05c39f6","datavalue":{"value":{"entity-type":"item","numeric-id":4669649,"id":"Q4669649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$38F425CD-8D26-4ECE-BDE3-51A35320C2A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad026089fb04c0f4f8582f6eea53ec98c478bf49","datavalue":{"value":{"entity-type":"item","numeric-id":5437652,"id":"Q5437652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$72432D0C-5006-411C-8FB5-ABF4B44246BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$9F7545F3-7F66-442C-8007-7FB4387132E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59767b12ed66c84a6db379782183675893492bd0","datavalue":{"value":{"entity-type":"item","numeric-id":4940937,"id":"Q4940937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$CE7CD3E2-2FFF-4B98-82F5-A72B95DECB41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22ef5f661c4f0016c7fdb92e88e8b94907f8385b","datavalue":{"value":{"entity-type":"item","numeric-id":5713748,"id":"Q5713748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$09777EBB-E671-49F9-B6A0-247D2BC9927A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$BCB1DB4C-F709-4B59-8BAF-F273EC8EB22E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98cfcf6e31ee74bc995fea8ab23c427fcd008a74","datavalue":{"value":{"entity-type":"item","numeric-id":3524241,"id":"Q3524241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$DE6A5512-2DC0-45E6-82A2-107852FB9D33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5fd74507b5c5628ad74a03f8a3d92f21a7f17d6f","datavalue":{"value":{"entity-type":"item","numeric-id":4736508,"id":"Q4736508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$1548EC00-1346-45A4-87D4-B7074C0BE4AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb01e27bc97bff97fba9528fa89381d2b8ab8f01","datavalue":{"value":{"entity-type":"item","numeric-id":4452593,"id":"Q4452593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$B6C7C833-5F53-4AE1-9307-727A52455408","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"374d98a831143d9feecd3c5171908372820ffadf","datavalue":{"value":{"entity-type":"item","numeric-id":3558337,"id":"Q3558337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$1D6631BD-FD06-44DD-8463-1B147C1E20BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ff043886c15344e26a5762a58f1c95f9724f12c","datavalue":{"value":{"entity-type":"item","numeric-id":4594216,"id":"Q4594216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$B20887F5-9CD0-4DC0-AD06-7B801D853E7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"824332076bf3d753d652a7b94c13f873009fc74f","datavalue":{"value":{"entity-type":"item","numeric-id":5472914,"id":"Q5472914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$B2F075F0-739C-4A4C-9A3A-B28D27EA2045","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5617fdd69c618e263e8fa2bd0476fbd6e5cae4ab","datavalue":{"value":{"entity-type":"item","numeric-id":4190095,"id":"Q4190095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$DE8EF9EB-B303-48D0-BCF4-1777D68D9B2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76f085e060cc02117b4ec73931c77617da801d17","datavalue":{"value":{"entity-type":"item","numeric-id":2473386,"id":"Q2473386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$1AA09703-59E8-45A6-AB46-CB445C53DB98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6fd86a574ce52183f6056be53a5d5584999bfd8","datavalue":{"value":{"entity-type":"item","numeric-id":1082058,"id":"Q1082058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$164A3309-5AF9-4986-B1B6-D4A8FBBC7710","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5791c716254aa1932faf4df96272562ac819ae0","datavalue":{"value":{"entity-type":"item","numeric-id":5703869,"id":"Q5703869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$176A0ABF-86C9-4BFC-A246-1C1DAEF20A7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$DEAA8765-D25F-4B64-AB81-2270C3AB676A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e98bea2faf0f1e7139247049b725eb54de257627","datavalue":{"value":{"entity-type":"item","numeric-id":5593816,"id":"Q5593816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$D33AC597-B72F-4762-B784-0FA22D3630C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5e1604a00628ddd7abdcaadf06538f9adcc20d2","datavalue":{"value":{"entity-type":"item","numeric-id":4804883,"id":"Q4804883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q428887$9A72B143-D6AF-49D9-9390-9798D3632483","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bab183a84859ab9d9df0492083d1e8fd7c0da2a3","datavalue":{"value":"10.1016/J.TCS.2012.02.024","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q428887$E95784F0-40E7-44DE-B3C9-28EF8CDC1668","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47b25c22c46d0ca86f6ce2c2532a917e61e47abc","datavalue":{"value":{"entity-type":"item","numeric-id":3558337,"id":"Q3558337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35d9011b04a9c39447790da06fa7bc568bdd7931","datavalue":{"value":{"amount":"+0.961304008960724","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q428887$CEBBC193-3D6C-4D7B-9E89-0CE665269DF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"96e9e186ec34980181af43efc9a3de126ba38a6c","datavalue":{"value":{"entity-type":"item","numeric-id":5437652,"id":"Q5437652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bc01dea63be20f67d75278be48e0d49e136e4c6c","datavalue":{"value":{"amount":"+0.8306584358215332","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q428887$C6C1336B-CB15-4080-BD91-F6E7FE5E55D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6b2a937bce5baa1e44f54c9029c4c73e58425d9","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b1085dbf426c27d2d160197fa63dd2f9224a19f","datavalue":{"value":{"amount":"+0.7826739549636841","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q428887$5E915B04-E7C3-4CB7-82E2-DBC51C893832","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"535af615ad5bf605dca3fda0c9eabaf6f7d8b0e7","datavalue":{"value":{"entity-type":"item","numeric-id":5398068,"id":"Q5398068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec1ce5e3914e54970e8f37389ba98cb6568ddbe4","datavalue":{"value":{"amount":"+0.7803534269332886","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q428887$8B70BDB8-1FDB-410B-89CD-9C0ED0A5352F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbd1f875057910272dc1f6cefa7437b5d6cd54c8","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2618ed902ceb80db69ff0ba4a9e4432bb1856820","datavalue":{"value":{"amount":"+0.7679336071014404","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q428887$FBBD1484-F6D9-4CD0-BE30-8DC8BDBC7214","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A pearl on SAT and SMT solving in Prolog","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_pearl_on_SAT_and_SMT_solving_in_Prolog"}}}}}