Lexicographic Boolean satisfiability

Maximal Satisfying Assignment (Lexicographic Boolean satisfiability / LexMaxSAT), the problem of finding the lexicographically maximum x_1, . . . , x_n ∈ {0, 1}^n that satisfies Boolean formula φ, or 0 if φ is not satisfiable, is NP-complete. But how does the certificate look like? Because it is not enough to have assignment that satisfies Boolean formula φ. How can we check that it is the largest in polynomial time?

• As stated the problem is not a decision problem, and so not in NP. (Also, for some natural variants, co-SAT (TAUTOLOGY) can be reduced to them in poly-time, so they surely are not in NP (unless NP = co-NP). Can you rewrite your post to make it more precise? Aug 13 at 19:11

This problem is not in $$NP$$ (unless $$PH$$ collapses), since it is already $$P^{NP}$$-hard, see e.g. [1].
Edit: As it was pointed out in the comments, $$NP$$ is indeed formally defined as a collection of decision problems and not search problems. So what I should have said is that this problem is not solvable by a non-deterministic $$TM$$ in polynomial time (unless $$PH$$ collapses). Also, as it was pointed out by Emil in the comments, the problem as stated is indeed $$FP^{NP}$$-complete, where $$FP$$ is the set of search problems solvable in polynomial time.
• @NealYoung Right. The problem as stated is $\mathrm{FP^{NP}}$-complete. The decision problem testing the value of individual variables in the lexicographically maximal assignment is $\mathrm{P^{NP}}$-complete. Aug 14 at 6:50