1
$\begingroup$

I'm working with several problems, which can have special unsatisfiable configurations. For example, consider the simple function $f(x,y)=x+y+2$ with $n$-bit unsigned inputs and $(n+2)$-bit unsigned output. This function can be easily expressed as a SAT problem.

Note, that the outputs $f(x,y)=0$ and $f(x,y)=1$ are not possible.

For my problems, I'm specifically interested in such impossible configurations. The usual method for finding such configurations, is to try possible configurations and check if they are UNSAT instances. However, this has the obvious drawback, that it is computational intensive (for my problems confirming UNSAT is much more expensive than finding SAT solutions) and relies on a certain density of the impossible configurations in the problem space (or external knowledge to narrow down the possible candidates).

This leads to my question: Is there some way to reformulate/convert/transform a SAT problem, of the form as described above into another SAT problem, where the satisfiable solutions are the impossible configurations I'm interested in?

Intuitively it should be possible, but all ways I could come up with, will simply output impossible solutions like $x=1, y=1, f(x,y)=3$.

Some paper searches also did not turn up anything useful.

Does anyone have ideas or pointers how to tackle this problem? Also, any pointers to impossibility results that show this approach is not feasible are welcome.

Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ A general method like this would prove NP equals coNP, no? This is a major open problem. On the more practical side, did you try throwing your problem at a SAT solver? In my experience (which is not necessarily with a very varied type of input) they are quite good with both positive and negative instances. $\endgroup$
    – Ville Salo
    Commented Jun 9, 2022 at 8:15
  • $\begingroup$ I'm not sure about the NP equals coNP, as this might be a special instance. Regarding simply using a SAT solver: the problem is, that I need to instantiate all possible outcomes as separate instances and solve each one. If the output space is large, this is infeasible or at least has a low success probability for finding an UNSAT instance. $\endgroup$
    – DasArchive
    Commented Jun 9, 2022 at 8:43
  • $\begingroup$ Are you asking for a technique that (sometimes) lets you go down from $\Sigma_2$ of the polynomial hierarchy to $\Sigma_1$ by somehow inverting the last quantifier? Or am I completely off? I know that there's some research into higher levels of the hierarchy, but I don't know how practical this is (a funny method I heard about, dunno how well it works, is to feed a SAT solver into a SAT solver...). $\endgroup$
    – Ville Salo
    Commented Jun 9, 2022 at 8:53
  • $\begingroup$ I'm not familiar with the polynomial hierarchy, but the example you mention with a SAT solver solving a SAT solver ( $solver(solverSAT(problem)==UNSAT)$ ) would be a solution to my problem (even if it does not sound very feasible...). $\endgroup$
    – DasArchive
    Commented Jun 9, 2022 at 10:17
  • $\begingroup$ NP = $\Sigma_1$ = languages like $\{u \;|\; \exists v: P(u, v)\}$, and $\Sigma_2$ is languages like $\{u \;|\; \exists v: \forall w: P(u, v, w)\}$ for some polynomially checkable predicates. $\endgroup$
    – Ville Salo
    Commented Jun 9, 2022 at 10:34

1 Answer 1

Reset to default
1
$\begingroup$

Indeed, it is most likely not possible to find a polynomial-size propositional formula whose models are exactly the non-outputs of $f(x,y)$, the problem for general $f$ is $\Sigma_2^p$-complete. You probably need to express your problem as a quantified Boolean formula (QBF) of the form $\exists z \; \forall x, y \; f(x, y) \neq z$. If you already have a formula encoding $f(x, y) = z$, you could just add the negated quantifiers $\forall z \; \exists x, y \; f(x, y) = z$, and check with a QBF solver that it is false; there are quite a few good ones out there, and they will also give you a witness of falsity, in this case a value for $z$.

I recommend to take a look at the input formats QDIMACS and the more flexible QCIR. For solvers, try Cadet, DepQBF, or CaQE (QDIMACS input), QuAbs, or Qfun (QCIR input), or Qute (both inputs; disclaimer, I'm one of the co-authors of Qute).

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .