1
$\begingroup$

Say you have an arithmetic problem involving two variables, how do you give a Boolean formula for that using standard techniques so that one gets a minimal formula for a given number of quantifiers?

Consider for example a function that decides if $(1)$ $x>y$ or $(2)$ a function that decides $x|y$?

$\endgroup$

closed as unclear what you're asking by D.W., David Richerby, Juho, Jake, Nicholas Mancuso May 5 '15 at 1:07

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 1
    $\begingroup$ Hint: how do you add in elementary school? $\endgroup$ – Raphael Dec 7 '14 at 10:59
  • $\begingroup$ Probably this is a stupid question. But curious about quantifier elimination. $\endgroup$ – T.... Dec 7 '14 at 11:44
1
$\begingroup$

Hint: Use the standard reduction from CircuitSAT to SAT. Equivalently: Use the Tseitin transform.

I assume you do know how to write a boolean circuit to test whether $x>y$. If not, consult a textbook.

$\endgroup$
  • $\begingroup$ Thank you. Actually I 'know' does not mean I am comfortable using quantifiers. Is there a reference? I am thinking there is both a $\forall\exists$ and a $\exists\forall$ version. $\endgroup$ – T.... Dec 7 '14 at 21:34
  • $\begingroup$ I am mostly interested in how many quantifiers you could minimally use? $\endgroup$ – T.... Dec 7 '14 at 21:35
  • 1
    $\begingroup$ @Turbo, I can't tell what you are asking. I would advise you to edit your question. Your question doesn't mention quantifiers at all -- if quantifiers are central to your question, then that needs to be clearly explained in the question. we can't give you a useful answer if you're not clear about what you're looking for. P.S. Please note that the SAT formula that is obtained through my method has only a single quantifier; there are no nested quantifiers. You can read more about the difference between SAT vs 2QBF. $\endgroup$ – D.W. Dec 8 '14 at 3:30

Not the answer you're looking for? Browse other questions tagged or ask your own question.