{"entities":{"Q1811072":{"pageid":1821814,"ns":120,"title":"Item:Q1811072","lastrevid":69018393,"modified":"2026-04-13T03:46:11Z","type":"item","id":"Q1811072","labels":{"en":{"language":"en","value":"A complete adaptive algorithm for propositional satisfiability"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1925255"}},"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":"Q1811072$B38EEE68-E6A4-4D14-BD63-E6E2DCE1E911","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b0485dabb955cdc69c73f49a8255c895b04fc5ad","datavalue":{"value":{"text":"A complete adaptive algorithm for propositional satisfiability","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1811072$D449B291-A5AB-46D4-A1ED-3814AFEF7B71","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e42f0ae27105c17506858f488e5d79b68d625d1d","datavalue":{"value":"1019.68043","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1811072$2DB0C904-86B8-4F24-AD0E-D3176E9FDA5F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7bd15601828ec9867f3e93313a232f6b9da80e71","datavalue":{"value":"10.1016/S0166-218X(02)00385-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1811072$DBD77917-5C05-42AB-9708-71A7EBF6D981","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"527715c31d225d5d93893467164e1a8892971b8e","datavalue":{"value":{"entity-type":"item","numeric-id":655182,"id":"Q655182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$5D60F664-8D14-4C27-A5B5-F5DE9697B053","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3de34c40bbd436145163ee502934245d6246cef6","datavalue":{"value":{"entity-type":"item","numeric-id":173870,"id":"Q173870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$569A50C5-AA5B-4F89-A031-ED7665DF62C8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"087f55844cc920aae060b09644168bf17b022e1a","datavalue":{"value":{"entity-type":"item","numeric-id":96294,"id":"Q96294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$6E7BDF44-2251-4A20-B066-8D6CCE0E21DB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ae38298a411e50615364cd6c80d7e0f949b3a896","datavalue":{"value":{"time":"+2003-06-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1811072$AA7524E5-D274-462D-9B82-D625A518A3FE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1811072$1D53AC8B-EE20-498C-890A-7CC019F23EA2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"35da94eb435c442e6b1f79867b9df1ffbfb1ec0e","datavalue":{"value":"1925255","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1811072$93EB8758-BEFD-4DCE-8E5E-385858D845DD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e8fe75ecdeef7e0425c4bb1338f9134c5adf0be","datavalue":{"value":"backtracking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1811072$7DC6C248-DB46-4D5F-9B7F-59A4AF9A2D9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82ec3934de052b4456148280561bf8899e054ca0","datavalue":{"value":"search frameworks","type":"string"},"datatype":"string"},"type":"statement","id":"Q1811072$3D1C0740-FB96-4629-846D-43813C52BD19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1811072$474BFE28-82AD-44B7-BCC8-A9D3563DD007","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5834864074172f90c0db592b61fbce75f9303a03","datavalue":{"value":{"entity-type":"item","numeric-id":16627,"id":"Q16627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$32962821-35B4-4763-8177-4299C4A04902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"56a9ecaca2ef35efc3f134af231037d82db08c02","datavalue":{"value":{"entity-type":"item","numeric-id":21683,"id":"Q21683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$30950824-527C-4A5D-AEC5-9FCB6A22B288","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"314cb7db240b78b9fdebd1fd8b43c1b0f383061e","datavalue":{"value":{"entity-type":"item","numeric-id":24795,"id":"Q24795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$16E8F362-FBF4-46F7-A7DB-E1AC927E0728","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":"Q1811072$1FFBBAA7-724B-4851-A364-DB3069422F72","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8efc2796cb38d8276b7b9b57e9267c43d63a9c6","datavalue":{"value":{"entity-type":"item","numeric-id":5687264,"id":"Q5687264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$88AF18A3-BA40-467F-BBE6-CEA132A043F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d71f2d332360f09a62b7e9e7a47b5aa0286a78e4","datavalue":{"value":{"entity-type":"item","numeric-id":4286227,"id":"Q4286227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$734B0EC3-DF9E-4FDD-A072-36F20D9ABA2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cd1b6f8712d6199daaf9b96dc69a4884afd8fd7","datavalue":{"value":{"entity-type":"item","numeric-id":4473049,"id":"Q4473049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$BC329959-15CD-46FB-9F81-FB544BDF2C63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d0863918228d158fae088a6efc6f79f2c8e8057","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$2A82311A-B334-424B-9AB7-1FA88B9B4AE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9397f656ad7df211fad8613745a81fe55825023f","datavalue":{"value":{"entity-type":"item","numeric-id":4032940,"id":"Q4032940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$C456AD62-AFA9-466E-B28F-00BB59720543","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bd2d94005cf638be560bebea9f4aaaa8555421d","datavalue":{"value":{"entity-type":"item","numeric-id":4255462,"id":"Q4255462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$E7C210D0-3D23-4378-A057-1A13184D4890","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":"Q1811072$7E4D61D1-CC36-4A08-A0DE-0942D57DA55F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$F6D2B841-9639-48F3-B370-A5F0D74CD1EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5a384833facfee1bed7555c136a9c348cab3dd0","datavalue":{"value":{"entity-type":"item","numeric-id":5687266,"id":"Q5687266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$FE702158-0C82-45B4-B285-2A2F4140DD9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0d47402a18255121e8b4c37559d3eb99d007b27","datavalue":{"value":{"entity-type":"item","numeric-id":1170883,"id":"Q1170883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$88F4633E-DB29-402A-8A25-16795CD6FEA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1478273e0e33a79d374260ca5dc8c9927268f336","datavalue":{"value":{"entity-type":"item","numeric-id":5687274,"id":"Q5687274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$20877B70-FC0D-4A48-A23B-7A1B4C5503D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35acb7c065d2a9d2147e073cef035eae32034dca","datavalue":{"value":{"entity-type":"item","numeric-id":2703800,"id":"Q2703800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$D15E96F0-A411-4441-A469-D11B06894FCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb6d3551c28e8173d291f95019cf63f4ea7788b4","datavalue":{"value":{"entity-type":"item","numeric-id":2749861,"id":"Q2749861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$3EF8DE44-67F6-464B-8909-A6FE79E266A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1963aa24001373e5ceaa7806d80ed90d73b392f","datavalue":{"value":{"entity-type":"item","numeric-id":4840102,"id":"Q4840102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$4C08A0E5-0528-4D6C-852F-10ED04FD1E00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d84fc41555f9112589e7a37710ae8c701d08ff8","datavalue":{"value":{"entity-type":"item","numeric-id":3145805,"id":"Q3145805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$0104A2A3-3F72-4D2C-ABDD-5E10C7DAB0A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb4fe328050ef9b6923529a534efe5f549f7a36c","datavalue":{"value":{"entity-type":"item","numeric-id":4319327,"id":"Q4319327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$9B2ABD74-7599-4FBC-B90A-B84C685BB032","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2261e03fb7a4b873cc7bf0aa682c707ae43c92d9","datavalue":{"value":{"entity-type":"item","numeric-id":1356213,"id":"Q1356213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$3CBCB95F-55B7-402F-8826-A0D8FFE16BB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f4ee378a41d931cd10f216e48f4b910155e1a89","datavalue":{"value":{"entity-type":"item","numeric-id":1904401,"id":"Q1904401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$42F65947-29B2-4F19-8488-D7EC98C3AD14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dee5c11e3467c275603f11fa79e4d2987c50139e","datavalue":{"value":{"entity-type":"item","numeric-id":5687268,"id":"Q5687268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$5F5F3568-2E6F-45FD-8DAC-00B1F547ECD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c3cf7cbf24f5ad1e6d8cb76fb93a3b15d7aa5c2","datavalue":{"value":{"entity-type":"item","numeric-id":1356218,"id":"Q1356218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$78BB91AA-49BC-47B2-A5B5-D09F4B517049","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"789c812451654d083d299e8fdb119e99ac2c02ab","datavalue":{"value":{"entity-type":"item","numeric-id":4714131,"id":"Q4714131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$6DDEFA83-E4BF-42C1-A46E-35A6572C9C9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1bcc64509a3b4ae8497ef3a4b4c9f3c08241c8d4","datavalue":{"value":{"entity-type":"item","numeric-id":687090,"id":"Q687090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$5B2300F7-D8E7-4AF7-901F-BDEA104AE573","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"923b31e26f24766e3ddda421d81a92188fdc771e","datavalue":{"value":{"entity-type":"item","numeric-id":2749859,"id":"Q2749859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$4E873618-61C8-4B93-9F92-99AA4EF1E12D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$FDEBDE8A-B1F5-424C-A45F-38486C6B68E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9269e64d2adca53bb2f298ca1a02b550d98c27a7","datavalue":{"value":{"entity-type":"item","numeric-id":4571400,"id":"Q4571400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$0E6CA4C5-BF1F-42CC-91D4-463A863D49DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06844938098368d2f2cf613285d701ed35dce312","datavalue":{"value":{"entity-type":"item","numeric-id":5687269,"id":"Q5687269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$E8B7C6AA-3A72-48A1-9DE8-73EB14B6010B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"96b9f1a7b9d16bc3c8d7642391067b84091013a6","datavalue":{"value":{"entity-type":"item","numeric-id":4705311,"id":"Q4705311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$FEEE66C2-7929-4CAE-BD14-014795FA0787","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb6b44d3ab57341d3a87da9b9124773b1ca70df9","datavalue":{"value":{"entity-type":"item","numeric-id":1977761,"id":"Q1977761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1811072$76BD7A93-ABA7-45E6-BCBB-53FDB3AEC320","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7eca13c81e0cfa25dba3c64e1c8cc34d9154caa9","datavalue":{"value":{"entity-type":"item","numeric-id":4375765,"id":"Q4375765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"805ef4843c0a49622c040e59a9ffd4801cce9907","datavalue":{"value":{"amount":"+0.8144715428352356","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":"Q1811072$928661A4-4C1C-4A26-A389-DCE3BAA39C0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a3e04bad2abc8a5c4aaf60be1708f0c1b7e9e532","datavalue":{"value":{"entity-type":"item","numeric-id":1904401,"id":"Q1904401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b6327610ba3d846b7fa559b04bc4c05c9cd397a","datavalue":{"value":{"amount":"+0.8144691586494446","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":"Q1811072$1AE818DB-0F01-48ED-9E1D-5D39802BFCA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e68a4ecd14d9185b0b097d26bcd476c19dadcf82","datavalue":{"value":{"entity-type":"item","numeric-id":4319327,"id":"Q4319327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53feb2ac45e4ee9e06ba7f991ebe11fc979899da","datavalue":{"value":{"amount":"+0.8012995719909668","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":"Q1811072$31160D56-2AA2-4E06-A9A8-CEA5488E920B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a29e179bbf06cf64dcb40b6c39cad4b300e7df5","datavalue":{"value":{"entity-type":"item","numeric-id":1356218,"id":"Q1356218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2879879a094bb697c91c27d6eaa0b0140c9bae6c","datavalue":{"value":{"amount":"+0.794098436832428","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":"Q1811072$CBA810E3-AEF4-40B3-B565-BFF31021D37B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5f377599ef69fd95d5d3831635020dc8687053b","datavalue":{"value":{"entity-type":"item","numeric-id":1408373,"id":"Q1408373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e89ac88f9e136cb2427d3edf60617dd3a1ffad00","datavalue":{"value":{"amount":"+0.7902960181236267","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":"Q1811072$CF7A0036-A46F-4D8D-AEDB-308A18605406","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A complete adaptive algorithm for propositional satisfiability","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_complete_adaptive_algorithm_for_propositional_satisfiability"}}}}}