You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

An Extension of Deficiency and Minimal Unsatisfiability of Quantified Boolean Formulas

Article type: Research Article

Authors: Kleine Büning, Hansa | Zhao, Xishunb; *

Affiliations: [a] Department of Computer Science, Universität Paderborn, 33095 Paderborn, Germany. E-mail: kbcsl@upb.de | [b] Institute of Logic and Cognition, Sun Yat-sen University, 510275 Guangzhou, P.R. China. E-mail: hsszxs@mail.sysu.edu.cn

Note: [*] Research was partially supported by the NSFC projects under grant No. 60573011, 10410638 and a MOE project under grant No. 05JJD72040122.

Keywords: deficiency, cohesion, QBF, minimal unsatisfiability, minimal falsity

DOI: 10.3233/SAT190032

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 3, no. 3-4, pp. 115-123, 2007

Received 1 September 2007
|
Revision received 1 October 2007
|
Published: 1 October 2007
Get PDF open access

Abstract

The notion of minimal unsatisfiability and minimal falsity will be extended to non-clausal and non-prenex quantified Boolean formulas. For quantified Boolean formulas in negation normal form we generalize the notion of deficiency to the so-called cohesion, which is 1+ the difference between the number of occurrences of the conjunction symbol ∧ and the number of existential and free variables. Further, we show that all the complexity results with respect to minimal unsatisfiability or minimal falsity known for formulas with fixed deficiency can be adapted to formulas with fixed cohesion. For example, (1) the minimal unsatisfiability of propositional formulas with fixed cohesion is still solvable in polynomial time and, (2) the minimal falsity of quantified Boolean formulas with cohesion 1 is solvable in polynomial time.

Show more