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.

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.

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.