{"entities":{"Q800915":{"pageid":802763,"ns":120,"title":"Item:Q800915","lastrevid":64472298,"modified":"2026-04-11T20:06:35Z","type":"item","id":"Q800915","labels":{"en":{"language":"en","value":"The complexity of the satisfiability problem for Krom formulas"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3878907"}},"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":"Q800915$B4CB373E-123D-4284-BD2F-A58E1403429D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c371a815a71199390d86e85c3ce08c5ca8f8e9fb","datavalue":{"value":{"text":"The complexity of the satisfiability problem for Krom formulas","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q800915$4985620E-B054-4269-8CDB-357990C17048","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"62b6e508f6be5d43f05e5b78a3e6e4eb7a32fd90","datavalue":{"value":"0552.03023","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800915$13DE27A3-C0BD-4130-8F06-834B365956CB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6a5ddedbc8ca116993b583d99220a1cfd4b3ca0e","datavalue":{"value":"10.1016/0304-3975(84)90138-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800915$F5F838DB-1070-4030-93F5-D8495338C48C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f7fcb889156969e5a5ded8e850ad2883bdb8ab84","datavalue":{"value":{"entity-type":"item","numeric-id":800913,"id":"Q800913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$C726BCBC-AA42-4CA5-9CA4-B80AF019009B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"377f0577777abeddabd75e3344d5dbc70225d82f","datavalue":{"value":{"entity-type":"item","numeric-id":800914,"id":"Q800914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$E1367214-D67C-4EDB-85F3-BA241CB996F2","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":"Q800915$10DAC5C0-5581-41CB-BEE5-0434B1D9717B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q800915$45BD4A5E-D638-48F5-9C74-E9F8DD16EEFC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b7527cfdbabbfa46887384abb44e9752e7604bcd","datavalue":{"value":"A Krom formula is a formula of pure quantificational theory whose matrix is in conjunctive normal form with at most two disjuncts in each conjunct. The authors study the computational complexity of the satisfiability problem for Krom formulas. Their results are as follows:    (1) Satisfiability is decidable in polynomial time for Krom formulas with prefix \\(\\forall \\exists \\forall\\). Moreover, the unsatisfiable Krom formulas with prefix \\(\\forall \\exists \\forall\\) form a class complete for nondeterministic log space.    (2) Satisfiability for Krom formulas with prefix \\(\\exists^*\\forall^*\\exists^*\\) is a complete problem for deterministic exponential time. But for each fixed k, satisfiability for Krom formulas with prefix \\(\\exists^*\\forall^ k\\exists^*\\) is decidable in polynomial time.    (3) Satisfiability for Krom formulas with prefix \\(\\exists^*\\forall^*\\) is a complete problem for polynomial space.    (4) Satisfiability for monadic Krom formulas is complete for P.","type":"string"},"datatype":"string"},"type":"statement","id":"Q800915$0DA40BF1-1AD7-431E-BFC7-212F83BAB95E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d7656d1c841701431b0b3d99d23720089a267cbb","datavalue":{"value":"03D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800915$C403F5E2-3BC3-42EF-BDDA-1482ECB2229B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800915$1FD4B4A0-5B04-4BCB-A7E8-A026BE9FFE7E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"aa678d282662eca6a9f362ea47ab5d5cb0b3d693","datavalue":{"value":"3878907","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800915$AEA12F91-A62A-46C8-88FE-0E9E392151FA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c98ec2f3f6bf865417696f78296c14b2e998dca1","datavalue":{"value":"Krom formula","type":"string"},"datatype":"string"},"type":"statement","id":"Q800915$5AA937D4-D5CB-4522-BE38-9A379ACBC858","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f0b4d6e6089943a261128dec792d30fd4cdc9763","datavalue":{"value":"satisfiability problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q800915$B33D2C98-6ED7-465E-8F66-12189116CA90","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"59699d8ba436c4690eab2e3c0ee0a7ef0d967cec","datavalue":{"value":{"entity-type":"item","numeric-id":1177040,"id":"Q1177040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$A691A882-7C2B-43DF-B4CB-E1E96323F8D6","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c007ae1867363f659c11dfe2e26b294ddb7e58e3","datavalue":{"value":{"entity-type":"item","numeric-id":33608,"id":"Q33608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$99324BCF-BA4C-41E0-8678-73C77C543C93","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":"Q800915$705F422B-D8CF-463F-8901-9DADF6BDE762","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"07e661d3aa67adc788049e2df5a3be008aee0287","datavalue":{"value":"https://doi.org/10.1016/0304-3975(84)90138-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q800915$8839E5ED-E959-464D-BE48-CE72B5EAF5A6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b9bc7dd6f743e374c544157a8523cca58442b988","datavalue":{"value":"W2007102962","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800915$93F63182-1F4C-4FB4-B350-DA9A08A776A3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4202f09d7cd72f0d6bd2fae7066a0a1771e5069","datavalue":{"value":{"entity-type":"item","numeric-id":5639707,"id":"Q5639707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$8568060C-2F86-4091-A213-634F39F5AC11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd263c609fab8bc901736d47fce033ac3e5df6ff","datavalue":{"value":{"entity-type":"item","numeric-id":4090321,"id":"Q4090321"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$F7905B6E-1913-4B26-A436-921D475CD31C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1cf035d2fecb7e445991dd16e141f37bab3768a8","datavalue":{"value":{"entity-type":"item","numeric-id":1254112,"id":"Q1254112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$6AB2C337-F487-44B3-AE1E-3768955BFD4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"648af4444efef3dfface63422920536bd2b0c180","datavalue":{"value":{"entity-type":"item","numeric-id":3928246,"id":"Q3928246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$E23760F2-6EAC-4EEB-BB28-2F1226516228","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef757ecac8e00102e8fe2d81d7657ee3391ff698","datavalue":{"value":{"entity-type":"item","numeric-id":4138187,"id":"Q4138187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$7D9D904A-99CD-4A13-B1A0-F4B425E2EA87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da9035a3503d06ad7946ad5c060940ce1e7b476e","datavalue":{"value":{"entity-type":"item","numeric-id":3905252,"id":"Q3905252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$65321282-5C53-4A6C-A814-015C451E0E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"870c5a38858355caeeae9f446f0a3e85a9be75a4","datavalue":{"value":{"entity-type":"item","numeric-id":5517673,"id":"Q5517673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$95FCA78E-13F1-4788-A755-048F33F47BCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d396cb7909eb8ef7cf9892a2d4d1be562fcbdc7","datavalue":{"value":{"entity-type":"item","numeric-id":4109298,"id":"Q4109298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$55723ED3-D36C-43F0-BD3C-651E9E83B715","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"373c65ef4069b52a23fe230e08a271e32f56a00a","datavalue":{"value":{"entity-type":"item","numeric-id":1235982,"id":"Q1235982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$74ACF693-DA73-4AC7-A16D-970EEC3B56CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dda6d4bc4ff06358c5dfe216b9a7a58bec1514be","datavalue":{"value":{"entity-type":"item","numeric-id":4102765,"id":"Q4102765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$8FE58098-FFC6-4303-8F3D-100DF665E72F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eda2db14c950cfacb2d9bab387b35d1aadfc67b0","datavalue":{"value":{"entity-type":"item","numeric-id":3284606,"id":"Q3284606"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$D7D72927-86FB-48F2-89BE-D456FB5E4369","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e81d57b58abc3a82b100d072439fecb147f7ea86","datavalue":{"value":{"entity-type":"item","numeric-id":3716320,"id":"Q3716320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$246BF776-5513-482B-9C88-2D8EEF8D1643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"446f1e7359d727b7ebadf68424d4ea447292feff","datavalue":{"value":{"entity-type":"item","numeric-id":3856727,"id":"Q3856727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$3A75104A-7855-4FD6-BA34-92BDA46BCFAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d6e5a2ec66a572177ef7c34d7ff9e3c5a3050d5","datavalue":{"value":{"entity-type":"item","numeric-id":1157324,"id":"Q1157324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$33B0D398-18A1-4AA3-9793-C647E7AFAAED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"71f28db7f96068e5ce3938c306e6d15e9aefa614","datavalue":{"value":{"entity-type":"item","numeric-id":3915990,"id":"Q3915990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$9BACFCD9-57B8-421D-8D56-3D6AAD1D1FC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ecc6f55557416025d6c02fe837dd8287da5d5b83","datavalue":{"value":{"entity-type":"item","numeric-id":5523671,"id":"Q5523671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$DF25E26C-E6A8-447B-9B66-895603B58C9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99b4eae7493d8f6c982d7549031f59a2b3902483","datavalue":{"value":{"entity-type":"item","numeric-id":3922169,"id":"Q3922169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$DF138A7F-F8AE-4235-A5C0-84F0B58BE2DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5003f1b35a3d8f903232f84c855b80979eec5e4f","datavalue":{"value":{"entity-type":"item","numeric-id":3888985,"id":"Q3888985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800915$4D199C0B-F092-4569-82E4-F8375C8B65A1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df684ab8201b649acc8d339dca420dbf8bf70615","datavalue":{"value":{"entity-type":"item","numeric-id":5402560,"id":"Q5402560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"90750a4b99c442cbbf184ab43076baab9eb2e344","datavalue":{"value":{"amount":"+0.7807751297950745","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":"Q800915$CD811AD3-7B59-47F3-B69E-E2436E35EAE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb861e6987f8122ae01660c60ce6f633ed4aa47f","datavalue":{"value":{"entity-type":"item","numeric-id":915716,"id":"Q915716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cde9e4e0cd1b93779f1eed02f0d87ebfcdc75992","datavalue":{"value":{"amount":"+0.770979106426239","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":"Q800915$33CADEA7-DF24-41A2-A4E6-ECEDAAC428E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bddfc75f5fc7e06f7d03193a2884493995fea06f","datavalue":{"value":{"entity-type":"item","numeric-id":5498869,"id":"Q5498869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2a1eb4b5332049e6bf414afb1a298ae2c6220be","datavalue":{"value":{"amount":"+0.7696687579154968","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":"Q800915$E47D2E56-DD61-497C-B711-AE57DF873749","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04415b4acfa317c05592d9e4057f2a56b8a072ef","datavalue":{"value":{"entity-type":"item","numeric-id":3815282,"id":"Q3815282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70ba477417255501a1065623a84402fd56dec022","datavalue":{"value":{"amount":"+0.7631921172142029","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":"Q800915$BDEDD888-94F3-453F-80E0-2BEA7AFCAB7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0a6bbb5e1a3a2447aa22aa16e34f75135c5de521","datavalue":{"value":{"entity-type":"item","numeric-id":3474280,"id":"Q3474280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"52be9b5f10ebc394c8b3fa7b172eafbd929d51ad","datavalue":{"value":{"amount":"+0.7618473768234253","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":"Q800915$9D14E096-BE39-43E3-A1AC-C7339960D103","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The complexity of the satisfiability problem for Krom formulas","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_complexity_of_the_satisfiability_problem_for_Krom_formulas"}}}}}