{"entities":{"Q1408376":{"pageid":1419116,"ns":120,"title":"Item:Q1408376","lastrevid":67377285,"modified":"2026-04-12T17:13:14Z","type":"item","id":"Q1408376","labels":{"en":{"language":"en","value":"On good algorithms for determining unsatisfiability of propositional formulas"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1981504"}},"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":"Q1408376$0F8BF9C1-8355-4866-8236-3414D0E5989D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2f1b6ffade9d88d6515eb3d0d61c8f9a342d036e","datavalue":{"value":{"text":"On good algorithms for determining unsatisfiability of propositional formulas","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1408376$0C0C5DA8-B602-4731-A518-6D439350FF3C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a7286b8040e1ff695b0e90b8d5db9ee54f5de936","datavalue":{"value":"1029.68077","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408376$97A9EA36-2B55-43AB-BE30-8CAC0F9AC3B3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0f5b3bf895e92e1282261071f33e4031c2871b24","datavalue":{"value":"10.1016/S0166-218X(02)00401-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408376$577C928A-CB7F-4605-A637-1881A987D305","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f53fea46fc27a6147aeab7ae894b4884119ca3f","datavalue":{"value":{"entity-type":"item","numeric-id":703080,"id":"Q703080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$9152DF15-FDCA-40BC-8B1C-BF40A7723F24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb85fd2c1ce489cbecf5dc649288fae9b7018a3f","datavalue":{"value":{"entity-type":"item","numeric-id":673601,"id":"Q673601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$79B9A3E8-7595-4E99-BAE9-4DC1CE82E92A","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":"Q1408376$45900D09-8C5F-422A-B839-1D10CEEE33B2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bdb952d10b49f391b9728d4aaf2d3506fc5000a3","datavalue":{"value":{"time":"+2003-09-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1408376$A76F59ED-D6AA-483E-890B-265F6FD9AE98","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408376$C4CA6804-217B-4359-9720-425B8CAC4437","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f966c6297c2e49ae2ed1f17bea5d14168d8d2d36","datavalue":{"value":"1981504","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408376$78EA5B73-BE69-4FE2-9312-39790A18C149","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c95393006136a65861f345d17e00540c09d9d258","datavalue":{"value":"Satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1408376$8CF9877A-5826-4616-B7CE-5C9461DBFF3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ef0530ef18563772d3f741322062bf074cdc527e","datavalue":{"value":"Resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1408376$B878BC85-0A75-475B-912F-8B8BEE8ABEC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"742acadec2058a1daf33969cf122f1e00d23a668","datavalue":{"value":"Theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1408376$442F9D86-59AA-450E-BCB4-CDAB350ECFFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"564332e55b61e7f17cadf5fbcc8128ee0156e727","datavalue":{"value":"Hitting set","type":"string"},"datatype":"string"},"type":"statement","id":"Q1408376$2BC5134A-E8D7-41A2-A2B8-EF9DCE1AF194","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":"Q1408376$93CD57D9-7E99-483C-B733-C9D30A1223EC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"213888b37453d8aaa1d0d856afbc3c9660e59705","datavalue":{"value":{"entity-type":"item","numeric-id":3191968,"id":"Q3191968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$B5135DFC-CF7B-4923-9CDC-0016EEF95FC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a83312a3e346c7419e7c503e1050470bf3c54e96","datavalue":{"value":{"entity-type":"item","numeric-id":3758242,"id":"Q3758242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$66F489A1-F320-40EE-89B9-44E8600C115F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bc69e791e3ac729c39aee0824be53f2494fd734","datavalue":{"value":{"entity-type":"item","numeric-id":918700,"id":"Q918700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$48BD477F-8D0D-4BA8-847F-AA56D07C4D83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c16d03080cf104b6d9587e78c576489f573cb47","datavalue":{"value":{"entity-type":"item","numeric-id":4228436,"id":"Q4228436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$244E0FA6-1DE3-43B1-80BD-F59035E41DDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91c636dd583a22faf929d1cb972aae014f779c04","datavalue":{"value":{"entity-type":"item","numeric-id":3496310,"id":"Q3496310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$22B59892-9653-47CE-950E-4F0853A4D69C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3150ccd621fbcc6deb9315c7b7f04d84e34b19c","datavalue":{"value":{"entity-type":"item","numeric-id":4360139,"id":"Q4360139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$DA884B39-9D06-40C3-A8E3-E5647DD5F297","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a87839e9cce21429fa5c0660242873028f18a79f","datavalue":{"value":{"entity-type":"item","numeric-id":4952608,"id":"Q4952608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$04A17D2F-14D9-46B2-899B-954491EA3216","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3cccfc1cb465ca1ab2419b14583b90ff3a0a1aad","datavalue":{"value":{"entity-type":"item","numeric-id":4862742,"id":"Q4862742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$4423C241-4D9D-4731-9E39-5B3073CEB467","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"783f5b77f65178466163307ca17329fb72140e4a","datavalue":{"value":{"entity-type":"item","numeric-id":3158517,"id":"Q3158517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$C3F8C500-50BD-4777-9983-C52ABE2F0C09","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":"Q1408376$B08D4F31-BBFD-403E-AE75-7E37FF000C13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c460f983de9e6a420aef566a3398a70e655aa7d","datavalue":{"value":{"entity-type":"item","numeric-id":4876696,"id":"Q4876696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$B083B136-E701-4219-960C-678C4877EEAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"836ad2a04f82225da478ca9f694f5cd99360b315","datavalue":{"value":{"entity-type":"item","numeric-id":4198056,"id":"Q4198056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$B2A118F9-FE65-40BE-8989-76648F462BC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7953570587570bcc9dcd5b0798422508bfde9a69","datavalue":{"value":{"entity-type":"item","numeric-id":4511484,"id":"Q4511484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$E61590CC-BB68-4FB2-B5DD-266DE28462BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"38a504233a997a0376458e299e1a23ac6f83ce5c","datavalue":{"value":{"entity-type":"item","numeric-id":4847396,"id":"Q4847396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$E9D458BA-2069-4CF3-8DDF-A8BD40523075","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3600a0afe71e9b9c22e19ee4b5b7bb726dd22d1","datavalue":{"value":{"entity-type":"item","numeric-id":4240602,"id":"Q4240602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$079B6607-8848-46FF-826D-A6C4CED5BF80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e956899ee0a7e06c94f20261b5948e49f9acb5d8","datavalue":{"value":{"entity-type":"item","numeric-id":4323730,"id":"Q4323730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1408376$FBE25E7A-A94A-4BBD-BCBF-133519EBA76D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8a15655b6e53ff5900dd038e82031157d85d5821","datavalue":{"value":"https://doi.org/10.1016/s0166-218x(02)00401-8","type":"string"},"datatype":"url"},"type":"statement","id":"Q1408376$1CCAEB36-8EF4-4B40-AE29-A19CC5E5FB73","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9a95a5670dfc5b692d6dfa73529fdd56d5277ff9","datavalue":{"value":"W2019983117","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1408376$E778E7F0-4FDB-4A88-A5F3-E44EC7AE91B8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a3917e3e7fe2dc83b3de6c719e805f0e55c1c890","datavalue":{"value":{"entity-type":"item","numeric-id":5466490,"id":"Q5466490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa58ef6e2126fd7675cb22c520819e390192e35f","datavalue":{"value":{"amount":"+0.8395192623138428","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":"Q1408376$38F2256E-9A95-465E-9983-C65DB867F242","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3134d6d93626b2492e70c1b77ac64227cbdc19e5","datavalue":{"value":{"entity-type":"item","numeric-id":4708577,"id":"Q4708577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9e85703ffeae202f0f4d8766283927bee62d1bd6","datavalue":{"value":{"amount":"+0.8334305286407471","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":"Q1408376$072DD835-A062-4659-B79D-92F8FED84CD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"63f8fd2ea61e9cb48fe2ac4632854cbebc6c8571","datavalue":{"value":{"entity-type":"item","numeric-id":3439113,"id":"Q3439113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97e5c7f6535c0658c70f9c29f77e6091b4131b43","datavalue":{"value":{"amount":"+0.8315562009811401","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":"Q1408376$6AE1874C-FEDF-42FC-8FCB-5C9D009DB493","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f217533a22c07b8181a08760432a95b0988ac362","datavalue":{"value":{"entity-type":"item","numeric-id":4471151,"id":"Q4471151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0601ce2eba2fc226670623f767eaa55d0fea038","datavalue":{"value":{"amount":"+0.8289154767990112","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":"Q1408376$76A5ACA1-CA1A-478E-BFE5-4D13A9C426E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dcbd397a9539527abb83715591f0f68c9062dcf5","datavalue":{"value":{"entity-type":"item","numeric-id":4862742,"id":"Q4862742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a78c1a309f5c57e0573b5d41d77adf01481ac232","datavalue":{"value":{"amount":"+0.8256259560585022","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":"Q1408376$C6F95948-C62F-48CF-B680-EECCDB7EE573","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On good algorithms for determining unsatisfiability of propositional formulas","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_good_algorithms_for_determining_unsatisfiability_of_propositional_formulas"}}}}}