Revision #2 Authors: Lefteris M. Kirousis, Phokion G. Kolaitis

Accepted on: 1st November 2001 00:00

Downloads: 3212

Keywords:

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 MINSAT(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.

We settle this question affirmatively by establishing a dichotomy theorem for the class

of all MINSAT(S)-problems, where S is a finite set of generalized connectives.

We also prove a dichotomy theorem for a variant of MINSAT(S) in which the minimization is

restricted to a subset of the variables, whereas the remaining variables may vary

arbitrarily (this variant is related to extensions of propositional circumscription and was first

studied by Cadoli). Moreover, we show that similar dichotomy theorems hold also when

some of the variables are assigned constant values.

Finally, we give simple criteria that tell apart the polynomial-time solvable cases

of these minimal satisfiability problems from the NP-complete ones.

Revision #1 Authors: Lefteris M. Kirousis, Phokion G. Kolaitis

Accepted on: 30th May 2001 00:00

Downloads: 3162

Keywords:

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 MINSAT(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.

We settle this question affirmatively by establishing a dichotomy theorem for the class

of all MINSAT(S)-problems, where S is a finite set of generalized connectives.

We also prove a dichotomy theorem for a variant of MINSAT(S) in which the minimization is

restricted to a subset of the variables, whereas the remaining variables may vary

arbitrarily (this variant is related to extensions of propositional circumscription and was first

studied by Cadoli). Moreover, we show that similar dichotomy theorems hold also when

some of the variables are assigned constant values.

Finally, we give simple criteria that tell apart the polynomial-time solvable cases

of these minimal satisfiability problems from the NP-complete ones.

TR00-082 Authors: Lefteris Kirousis, Phokion G. Kolaitis

Publication: 22nd September 2000 20:34

Downloads: 3667

Keywords:

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 MINSAT(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.

We settle this question affirmatively by establishing a

dichotomy theorem for the class of all

MINSAT(S)-problems, where S is a finite set of generalized

connectives. We also prove a dichotomy theorem for a variant of

MINSAT(S) in which the minimization is

restricted to a subset of the variables, whereas

the remaining variables may vary arbitrarily

(this variant is related to extensions of propositional

circumscription and was first studied by Cadoli).

Moreover, we show that

similar dichotomy theorems hold also when some of

the variables are assigned constant values. Finally, we give

simple criteria that tell apart the polynomial-time solvable cases

of these minimal satisfiability problems from the NP-complete ones.