TY - GEN
T1 - The complexity of minimal satisfiability problems
AU - Kirousis, Lefteris M.
AU - Kolaitis, Phokion G.
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2001.
PY - 2001
Y1 - 2001
N2 - A dichotomy theorem for a class of decision problems is a result asserting that certain problems in the class are solvable in polynomial time, while the rest are NP-complete. The first remarkable such dichotomy theorem was proved by T.J. Schaefer in 1978. It concerns the class of generalized satisfiability problems SAT(S), whose input is a CNF(S)-formula, i.e., a formula constructed from elements of a fixed set S of generalized connectives using conjunctions and substitutions by variables. Here, we investigate the complexity of minimal satisfiability problems MIN SAT(S), where S is a fixed set of generalized connectives. The input to such a problem is a CNF(S)-formula and a satisfying truth assignment; the question is to decide whether there is another satisfying truth assignment that is strictly smaller than the given truth assignment with respect to the coordinate-wise partial order on truth assignments. Minimal satisfiability problems were first studied by researchers in artificial intelligence while investigating the computational complexity of propositional circumscription. The question of whether dichotomy theorems can be proved for these problems was raised at that time, but was left open. In this paper, we settle this question affirmatively by establishing a dichotomy theorem for the class of all MIN SAT(S)-problems.
AB - A dichotomy theorem for a class of decision problems is a result asserting that certain problems in the class are solvable in polynomial time, while the rest are NP-complete. The first remarkable such dichotomy theorem was proved by T.J. Schaefer in 1978. It concerns the class of generalized satisfiability problems SAT(S), whose input is a CNF(S)-formula, i.e., a formula constructed from elements of a fixed set S of generalized connectives using conjunctions and substitutions by variables. Here, we investigate the complexity of minimal satisfiability problems MIN SAT(S), where S is a fixed set of generalized connectives. The input to such a problem is a CNF(S)-formula and a satisfying truth assignment; the question is to decide whether there is another satisfying truth assignment that is strictly smaller than the given truth assignment with respect to the coordinate-wise partial order on truth assignments. Minimal satisfiability problems were first studied by researchers in artificial intelligence while investigating the computational complexity of propositional circumscription. The question of whether dichotomy theorems can be proved for these problems was raised at that time, but was left open. In this paper, we settle this question affirmatively by establishing a dichotomy theorem for the class of all MIN SAT(S)-problems.
UR - http://www.scopus.com/inward/record.url?scp=26444524434&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=26444524434&partnerID=8YFLogxK
U2 - 10.1007/3-540-44693-1_36
DO - 10.1007/3-540-44693-1_36
M3 - Conference contribution
AN - SCOPUS:26444524434
SN - 9783540416951
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 407
EP - 418
BT - STACS 2001 - 18th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings
A2 - Ferreira, Afonso
A2 - Reichel, Horst
PB - Springer Verlag
T2 - 18th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2001
Y2 - 15 February 2001 through 17 February 2001
ER -