{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:45:31Z","timestamp":1740138331843,"version":"3.37.3"},"reference-count":7,"publisher":"World Scientific Pub Co Pte Ltd","issue":"03n04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Artif. Intell. Tools"],"published-print":{"date-parts":[[2020,6]]},"abstract":"<jats:p> We introduce an enhanced notion of unsatisfiable cores for QBF in prenex CNF that allows to weaken universal quantifiers to existential quantifiers in addition to the traditional removal of clauses. The resulting unsatisfiable cores can be different from those of the traditional notion in terms of syntax, standard semantics, and proof-based semantics. This not only gives rise to explanations of unsatisfiability but, via duality, also leads to diagnoses and repairs of unsatisfiability that are not obtained with traditional unsatisfiable cores. We use a source-to-source transformation on QBF in PCNF such that the weakening of universal quantifiers to existential quantifiers in the original formula corresponds to the removal of clauses in the transformed formula. This makes any tool or method for the computation of unsatisfiable cores of the traditional notion available for the computation of unsatisfiable cores of our enhanced notion. We implement our approach as an extension to the QBF solver DepQBF, and we perform an extensive experimental evaluation on a subset of QBFLIB. We illustrate with several case studies that helpful information can be provided by unsatisfiable cores of our enhanced notion. <\/jats:p>","DOI":"10.1142\/s021821302060012x","type":"journal-article","created":{"date-parts":[[2020,6,17]],"date-time":"2020-06-17T11:01:59Z","timestamp":1592391719000},"page":"2060012","source":"Crossref","is-referenced-by-count":1,"title":["Enhanced Unsatisfiable Cores for QBF: Weakening Universal to Existential Quantifiers"],"prefix":"10.1142","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5638-3678","authenticated-orcid":false,"given":"Viktor","family":"Schuppan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2020,6,18]]},"reference":[{"key":"p_2","first-page":"10","author":"Rintanen J.","year":"1999","journal-title":"J. Artif. Intell. Res."},{"key":"p_7","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.3.2.157"},{"key":"p_8","first-page":"9","author":"Bruni R.","year":"2001","journal-title":"Electronic Notes in Discrete Mathematics"},{"key":"p_22","first-page":"70","author":"Reimer S.","year":"2014","journal-title":"ECEASST"},{"key":"p_32","doi-asserted-by":"publisher","DOI":"10.1145\/1507244.1507247"},{"key":"p_34","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0242-1"},{"key":"p_60","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9084-z"}],"container-title":["International Journal on Artificial Intelligence Tools"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S021821302060012X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,17]],"date-time":"2020-06-17T11:02:09Z","timestamp":1592391729000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S021821302060012X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6]]},"references-count":7,"journal-issue":{"issue":"03n04","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["10.1142\/S021821302060012X"],"URL":"https:\/\/doi.org\/10.1142\/s021821302060012x","relation":{},"ISSN":["0218-2130","1793-6349"],"issn-type":[{"type":"print","value":"0218-2130"},{"type":"electronic","value":"1793-6349"}],"subject":[],"published":{"date-parts":[[2020,6]]}}}