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

The Complexity of Some Subclasses of Minimal Unsatisfiable Formulas

Article type: Research Article

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

Affiliations: [a] Department of Computer Science, University of Paderborn, 33095 Paderborn (Germany). E-mail: [email protected] | [b] Institute of Logic and Cognition, Sun Yat-sen University, 510275 Guangzhou (P. R. China). E-mail: [email protected]

Note: [*] The second author was partially supported by the NSFC projects under grant numbers: 60573011, 10410638 and the MOE project under grant number 05JJD72040122.

Keywords: minimal unsatisfiable formulas, maximal MU, marginal MU, unique satisfiability, disjunctive splitting, complexity

DOI: 10.3233/SAT190026

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 3, no. 1-2, pp. 1-17, 2007

Received 1 December 2006
|
Revision received 1 April 2007
|
Published: 1 May 2007
Get PDF open access

Abstract

This paper is concerned with the complexity of some natural subclasses of minimal unsatisfiable formulas. We show the DP–completeness of the classes of maximal and marginal minimal unsatisfiable formulas. Then we consider the class Unique–MU of minimal unsatisfiable formulas which have after removing a clause exactly one satisfying truth assignment. We show that Unique–MU has the same complexity as the unique satisfiability problem with respect to polynomial reduction. However, a slight modification of this class leads to the DP–completeness. Finally we show that the class of minimal unsatisfiable formulas which can be divided for every variable into two separate minimal unsatisfiable formulas is at least as hard as the unique satisfiability problem.

Show more