Prev: Last Call for Papers Reminder (extended): IAENG International Conference on Communication Systems and Applications (ICCSA 2010)
Next: now open all blocked site with our proxy
From: cplxphil on 2 Jan 2010 23:40

I've asked this on comp.theory before, though it's been over a year
since the discussion took place...but looking through the archives of
the previous discussion, I'm still not clear as to how do what I'm
interested in doing.

I would like to learn how to program an efficient mapping of a
decision-problem version of the discrete logarithm problem to SAT. I
do not want to design a verifier Turing machine for the problem, as
that sounds unnecessarily difficult.

Does anyone know of a website or, failing that, a textbook, that
explains specifically how to map a decision problem to SAT? (Yes,
I've searched Google, but haven't found anything helpful, at least not
yet.) I have Sipser's Introduction to the Theory of Computation,
which explains Cook's Theorem in detail...but I recall from the
previous discussion that there's something about constructing a
circuit that is involved. I think the issue may be that my computer
architecture background is weak.

Thanks for any information anyone can provide.

-Phil
From: tchow on 3 Jan 2010 14:16
In article <c12f6401-b401-4d01-81d7-012933e8db10(a)c3g2000yqd.googlegroups.com>,
cplxphil <cplxphil(a)gmail.com> wrote:
>Does anyone know of a website or, failing that, a textbook, that
>explains specifically how to map a decision problem to SAT?

This is the sort of thing that is best learned by doing rather than by
reading an explanation.

I suggest that as a warm-up exercise, you try to map Sudoku to SAT.

To get you started: Let x_{ijk} be a binary variable that is 1 if the
cell in position (i,j) contains the value k and is 0 otherwise. Here
i,j,k run from 1 to 9.

You need to express the Sudoku constraints as constraints on the values
of these variables. For example, you can't have more than one symbol
in the same cell. That means that for every i and j (from 1 to 9), and
for every pair of distinct k and k', we have to satisfy the clause

(NOT x_{ijk}) OR (NOT x_{ijk'}).

That should be enough to get you started.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
From: cplxphil on 4 Jan 2010 09:27
On Jan 3, 2:16 pm, tc...(a)lsa.umich.edu wrote:
> In article <c12f6401-b401-4d01-81d7-012933e8d...(a)c3g2000yqd.googlegroups.com>,
>
> cplxphil  <cplxp...(a)gmail.com> wrote:
> >Does anyone know of a website or, failing that, a textbook, that
> >explains specifically how to map a decision problem to SAT?
>
> This is the sort of thing that is best learned by doing rather than by
> reading an explanation.
>
> I suggest that as a warm-up exercise, you try to map Sudoku to SAT.
>
> To get you started: Let x_{ijk} be a binary variable that is 1 if the
> cell in position (i,j) contains the value k and is 0 otherwise.  Here
> i,j,k run from 1 to 9.
>
> You need to express the Sudoku constraints as constraints on the values
> of these variables.  For example, you can't have more than one symbol
> in the same cell.  That means that for every i and j (from 1 to 9), and
> for every pair of distinct k and k', we have to satisfy the clause
>
>   (NOT x_{ijk}) OR (NOT x_{ijk'}).
>
> That should be enough to get you started.
> --
> Tim Chow       tchow-at-alum-dot-mit-dot-edu
> The range of our projectiles---even ... the artillery---however great, will
> never exceed four of those miles of which as many thousand separate us from
> the center of the earth.  ---Galileo, Dialogues Concerning Two New Sciences

Cool, thanks for the tips. I'll try the Sudoku mapping. A slight
impediment is that I don't know anything about Sudoku, but I'm sure
that will be an easy problem to remedy.

Thanks again.

-Phil
From: Paul E. Black on 4 Jan 2010 13:38
On Monday 04 January 2010 09:27, cplxphil wrote:

> On Jan 3, 2:16 pm, tc...(a)lsa.umich.edu wrote:
>> In article
>> <c12f6401-b401-4d01-81d7-012933e8d...(a)c3g2000yqd.googlegroups.com>,
>>
>> cplxphil  <cplxp...(a)gmail.com> wrote:
>> >Does anyone know of a website or, failing that, a textbook, that
>> >explains specifically how to map a decision problem to SAT?
>>
>> This is the sort of thing that is best learned by doing rather than by
>> reading an explanation.
>>
>> I suggest that as a warm-up exercise, you try to map Sudoku to SAT.

An even smaller step is to map "binary sudoku" to SAT

http://xkcd.com/74/

Seriously, it allows one to think through some of the complexities and
still be manageable.

-paul-
--
Paul E. Black (p.black(a)acm.org)
 | 
Pages: 1
Prev: Last Call for Papers Reminder (extended): IAENG International Conference on Communication Systems and Applications (ICCSA 2010)
Next: now open all blocked site with our proxy