The New Sudoku Players' Forum

[Mathimagics]

Sudoku as a SAT problem is entirely about the "exactly one of" function (being an exact cover problem).

Encoding any Sudoku (any size, any jigsaw template) is simply a matter of generating the appropriate sequence of ExactlyOneOf(x1, x2, x3, ... xn) formulae, one for each cell, each row, and each region.

Here are 3 different encoding methods, in addition to the naive method (aka binomial), with the number of clauses required for various N, where N is the number of choices in the list x:

Code: Select all

 N     6   7   8   9  10  11  12  13  14  15  16
------------------------------------------------
Naive 16  22  29  37  46  56  67  79  92 106 121   
Bin   16  19  23  27  31  36  40  43  47  51  55
Tern  16  18  21  25  28  32  35  39  44  46  51
SAD   14  17  20  23  26  29  32  35  38  41  44

 N     25   36   49   64   81  100  121  144  169  196  225  256
----------------------------------------------------------------
Naive 301  631 1177 2017 3241 4951 7261  10k  14k  19k  25k  32k
Bin    91  135  187  247  316  391  475  567  668  775  891 1015 
Tern   81  119  165  217  277  343  417  499  585  679  781  889
SAD    71  104  143  188  239  296  359  428  503  584  671  764


Bin encoding splits the list into pairs and treats them like a binary tree. Tern is ternary, which does the same thing but in groups of 3 (the combinatorial advantage of these approaches evaporates beyond 3).

SAD is appropriately named as we will see shortly. On the surface it is one of those simple but so elegant methods that just takes your breath away. The method simulates a Serial Adder circuit, that "counts" the true values in the list and produces true if that count is 0 or 1, otherwise false (ie > 1 value is true). Combine that with a single clause that tells you whether any of the values are true, and hey presto.

The encoding itself is linear, while the other 2 methods require some recursion. Neat, huh? Clause count is 3N - 4.

The really sad part is that every invocation requires N - 1 extra variables, so in practice, while reducing the clauses count, it turns out to be no faster than binary encoding.

Since ternary encoding uses the same principle as binary, but with less clauses and less extra variables (~log3(N)), it is almost always the best performing method in practice.

[blue]

Hi Mathimagics,

Are you sure these are the right numbers (for the binary encoding in particular) ?
The one that I know, would use 4 auxiliary variables, and 1+16*4 = 65 clauses, for "1 of 16" (for example).
There would be ways to modify it to use fewer than 1+N*log2(N) clauses sometimes ... but only when N isn't a power of 2.

Code: Select all

N        |  5   6   7   8   9  10  11  12  13  14  15  16
---------+-----------------------------------------------
Native-C | 11  16  22  29  37  46  56  67  79  92 106 121
Bin-C    | 16  19  22  25  37  41  45  49  53  57  61  65
Bin-V    |  3   3   3   3   4   4   4   4   4   4   4   4

N        |  25   36   49   64   81  100  121  144  169  196  225  256
---------+-----------------------------------------------------------
Native-C | 301  631 1177 2017 3241 4951 7261  10k  14k  19k  25k  33k
Bin-C    | 126  217  295  385  568  701  848 1153 1353 1569 1801 2049
Bin-V    |   5    6    6    6    7    7    7    8    8    8    8    8

Best Regards,
Blue.

[Mathimagics]

Hi blue

If we we encode from the bottom up, rather than top-down, then as soon as we get to a point where there are less than 6 variables in play, we switch to binomial mode for the balance, that would explain the difference I think (forgive the VB6 format in my pesudo-code):

Code: Select all

Enum1ofN(vList):
   NC = 0
   For J = 1 To N - 1 Step 2
      V1 = vList(J)
      V2 = vList(J + 1)
      Encode ChooseFrom2  ' 4 clauses for V1, V2 (+1 CV = control vbl)
      NC = NC + 1       
      cList(NC) = CV
      CV = CV + 1
      Next
   
   If (N Mod 2) Then       ' ungrouped item, just carry it over to next level
      NC = NC + 1
      cList(NC) = vList(N)
      End If
         
   If NC < 6 Then             
      Encode NaiveChooseFromN   '  (NC * (NC - 1) \ 2) + 1 clauses
   Else
      Enum1ofN cList, NC        '  handle CV's + carried over Vn's
      End If


[blue]

Hi Jim,

If we we encode from the bottom up, rather than top-down, then as soon as we get to a point where there are less than 6 variables in play, we switch to binomial mode for the balance, that would explain the difference I think (forgive the VB6 format in my pesudo-code):

Interesting ... "thank you".
The explanation must be "as you've said".

FWIW: I don't read VB (or VB6), but "that not withstanding", I think I understand everything except what happens in the line:

Code: Select all

Encode ChooseFrom2  ' 4 clauses for V1, V2 (+1 CV = control vbl)

The questions I have, are:

• Is the "+1 CV = control variable", the same one, or different from the one that appears in the "cList(NC) = CV" line ? (A table showing the number of "contol variables" for each N, would be a nice addition).
• In detail, what are the "4 clauses for V1, V2 (+1 CV = control vbl)" ?
• [ In particular, are they binary/"2 literal" clauses, or something else ... 3 literals, maybe ? ] [added: "binary" probably isn't the right word here, since it might be taken to imply "one or the other, but not both"]

To guard against the possiblity that I've misread things, are these statements true ?

• The line "Encode NaiveChooseFromN ' (NC * (NC - 1) \ 2) + 1 clauses", is the last to execute, in the encoding.
• It is essentially replacing the "strong link" clause: 'one of these N variables/"or 'literals' (in the more general sense)", must be true' ... with a clause like "one of the variables from these K groups (of variables/literals), must be true" ... where K satisfies "3 <= K <= 5" ... and adding that ... "Oh, by the way, the (K) individual groups are (pairwise) disjoint".
• The first (K-1) groups, have size 2^J for some J, and the last group contain "whatever is left over" ... <= 2^J literals, in particular.
• The pseudocode is (likely?) missing the issue of "what if the initial N is already <= 5 ?"

I have a "deep" question in mind here, too, that would presumably be answered in the above:

• Suppose one of the original N variables/"or 'literals' ...", was set to 'true' in the solving process. What are the relevant details in the sequence of events that would follow, that would lead to the (N-1) remaining cases, being set to 'false' -- assuming they haven't already set to 'false' ?

TIA, for your time.

Cheers,
Blue.

[Mathimagics]

TIA, for your time.

Very happy to oblige in your case!

Remember this? (from Jigsaw Solver thread):

I only learned CNF today (or was that yesterday?), but one of the papers I'm working up to is this:
Efficient encoding for selecting 1 of N
which appears to be just what you were discussing.

If you take a quick butcher's at p2/3 you will probably have answers to most of your questions. That plus a listing given below of the actual clauses generated for two simple cases.

I simply assumed that we were all using the same technique! Hence the brevity of my pseudo-code ...

The control variables, what the paper refers to as "commander variables", are simply allocated by sequence starting from SN^3, where SN is the Sudoku grid size. "CV = CV +1" is simply the allocator.

In these examples I use SN = 9. The first listing shows the naive (binomial) encoding for "X[2,3] = one of {2,4,7}". I'll use decimal mapping for the grid variables, for ease of reading, and omit the trailing 0's:

Code: Select all

 232  234  237
-232 -234
-232 -237
-234 -237


Normally I'd start control variables from 729, but here I've used 1000. Here's the binary encoding for "X[2,3] = one of {1,3,4,7,8,9}". There are 3 groups of 2, the number in parentheses indcates the corresponding "rule" given in the paper:

Code: Select all

c
c group 1
c
 -231 -233          (1)
-1001  231 233      (2)
 1001 -231          (3)
 1001 -233          (3)
c
c group 2
c
 -234 -237          (1)
-1002  234 237      (2)
 1002 -234          (3)
 1002 -237          (3)
c
c group 3
c
 -238 -239          (1)
-1003  238 239      (2)
 1003 -238          (3)
 1003 -239          (3)
c
c  3 groups, 3 CV's, exactly one of which must be true  (rule 4)
c
 1001  1002  1003
-1001 -1002
-1001 -1003
-1002 -1003


That should be 16 clauses all up ...

[Mathimagics]

The pseudocode is (likely?) missing the issue of "what if the initial N is already <= 5 ?"

Well spotted. I just wanted to be sure you were paying attention!

I have one version (text CNF generator) in which the caller does the naive encoding and only calls the routine above with N >= 6.

Version 2, which sets up the CNF array in memory for SAT-as-DLL, is much neater.

I'll defer further consideration of your other questions until you decide whether or not you still have them, OK?

[blue]

Hi Jim,

I'll defer further consideration of your other questions until you decide whether or not you still have them, OK?

Yes, good. They have all been answered ... thank you again

Remember this? (from Jigsaw Solver thread):

I only learned CNF today (or was that yesterday?), but one of the papers I'm working up to is this:

{ note by Moderator:
URL was wrong,
have now corrected "..." to "papers"
and it works fine }

Efficient encoding for selecting 1 of N
which appears to be just what you were discussing.

I tried that link, when you first posted it.
I looked back today, to see if you had changed it.
Whenever I try it, I get the message:

Document not found
The requested address (URL) was not found on this server.
You may have used an outdated link or may have typed the address incorrectly.

edit: (snip)

Happily, your previous post, has answered all of my questions.
For "Ternary encoding", I fear I'll be forever at a loss.

Cheers,
Blue.

PS: I'll post the details of the "binary encoding" that I know, next -- in case anyone is interested.
It would be interesting to compare the performance, but I suspect that the method that you outlined, would be best.
No -- I take that back. The method that you describe, must use on the order of N (or N/2) "auxiliary variables", and that makes it significantly different. (No guess from me, as to which might perform better).

Cheers,
Blue.

[blue]

A different 'binary encoding':

Details for encoding the "1 of N" clause: "exactly one of { ClauseLit(c,0), ClauseLit(c,1), ..., ClauseLit(c,N-1) } must be true"

1. If N <= 7, use the simple "binomial encoding" -- one clause for the "strong link" and N*(N-1)/2 clauses for "weak links" -- else:
2. Find the first K with N <= 2^K ... where "2^K" means "two, to the power K"
   In C/C++, this works, for reasonable N: "int K = -(int)floor(1.e-6 - log(N) / log(2));"
3. Introduce K "auxiliary variables" ... AuxVar(c,0), ..., AuxVar(c,K-1).
4. Assign a unique index in the range 0 <= 'index' < 2^K, to each literal in the clause -- easiest: assign indicies 0...(N-1).
5. Let f(n,k) represent the k'th bit in the binary representation of the index for the n'th literal in the clause ...
   
   1. 0 <= n < N, 0 <= k < K
   2. f(n,k) = 0 <=> bit 'k' is '0' in the index for literal 'n'.
   3. f(n,k) = 1 <=> bit 'k' is '1' in the index for literal 'n'.
6. For each (n, k), add the appropriate clause:
   
   1. "~ClauseLit(c,n) | ~AuxVar(c,k)" ... if f(n,k) = 0
   2. "~ClauseLit(c,n) | AuxVar(c,k)" ... if f(n,k) = 1
7. Note: the above clauses, handle the "weak links" between literals in the "1 of N" clause ... "no more than one, can be true".
8. For the "strong link", add the clause: "ClauseLit(c,0) | ClauseLit(c,1) ... | ClauseLit(c,N-1)" ... "at least one, must be true".

Why it works (without too much detail):

1. The "strong link" clause (if nothing else), would cause one of the literals in the "one of N" clause, to be set to 'True'.
2. The clauses in (6) above, would cause the auxiliary variables to be set in a way that reflects the index of that literal.
3. For any other literal in the clause, at least one of the bits in its index, would differ from the correponding bit in the index for the literal that was (just) set to 'True'.
4. The corresponding clause from (6) ... i.e. for that (other) literal, and for that (particular) bit ... would cause the (other) literal to be set to 'False'.
5. If somehow, both literals got set to 'True' -- not impossible -- then a conflict would arise, as they "try to set" the auxiliary variable for the (particular) bit (or bits), to opposing values ... and backtracking would ensue.

[Mathimagics]

I am so, so sorry! I have posted a bad document link, not once, but twice!!

For some inexplicable reason "papers" became "..." when I copied and pasted that link.

My humblest apologies ...

(Ternary should become clear, we divide the choice terms into groups of 3, rather than groups of 2).

Your method is indeed cute!

Since I have the other encoders already set up,I will add your method "BCBE" ("blue's cute binary encoding") and run some tests ...

[JasonLion]

Sometimes you need to enclose URLs in a URL command for them to work correct. Enter the URL normally, select the URL, and press the URL button along the top of the post compose area.

[blue]

For some inexplicable reason "papers" became "..." when I copied and pasted that link.

I have it now, thanks.

Since I have the other encoders already set up,I will add your method "BCBE" ("blue's cute binary encoding") and run some tests ...

It's not mine, of course. I read about it in a paper with a title similar to the one that you referenced.

[Mathimagics]

Ok, I've called it BBE (for Bitwise Binary Encoding).

I've run a series of benchmark tests comparing the 4 methods, along with "Naive" which uses the standard binomial approach in all cases. The results might come as a bit of a shock (they did surprise me!):

First of all, with a 25x25 minimal puzzle:

Code: Select all

Case 1: 25x25 (287)   
  Binary                5.52 s
  Ternary               4.84 s
  Serial                6.77 s
  BBE                   5.00 s
  Naive                 5.00 s


Next with a 36x36 in various states of reduction. Naive results are missing from some, because I (naively) only thought of including it halway through the tests, and had thrown away the intermediate grids. The value in parentheses is the number of givens:

Code: Select all

Case 2: 36x36 (670)
  Binary                2.92 s
  Ternary               2.72 s
  Serial                3.41 s
  BBE                   2.77 s

Case 3: 36x36 (668)
  Binary               10.99 s
  Ternary              10.61 s
  Serial               11.65 s
  BBE                  10.19 s
  Naive                 9.54 s

Case 4: 36x36 (666)
  Binary               30.11 s
  Ternary              28.45 s
  Serial               35.23 s
  BBE                  29.99 s

Case 5: 36x36 (664)
  Binary               46.34 s
  Ternary              34.38 s
  Serial               47.31 s
  BBE                  38.43 s

Case 6: 36x36 (662)
  Binary               64.73 s
  Ternary              58.45 s
  Serial               82.94 s
  BBE                  60.47 s

Case 7: 36x36 (660)
  Binary               77.96 s
  Ternary             102.29 s     
  Serial              111.50 s
  BBE                 100.03 s

Case 8: 36x36 (658)
  Binary              190.81 s
  Ternary             192.05 s
  Serial              230.96 s
  BBE                 176.15 s 

Case 9: 36x36 (656)
  Binary              194.92 s 
  Ternary             344.63 s
  Serial              254.77 s
  BBE                 218.15 s
  Naive               192.57 s 

Case 10: 36x36 (655)
  Binary              250.39 s
  Ternary             387.88 s
  Serial              276.20 s
  BBE                 237.56 s 
  Naive               220.57 s 

Case 11: 36x36 (653)
  Binary              278.16 s 
  Ternary             472.68 s
  Serial              542.55 s
  BBE                 360.15 s
  Naive               333.48 s 

Case 12: 36x36 (651)
  Binary              412.52 s 
  Ternary             529.70 s
  Serial              948.59 s
  BBE                 401.73 s 
  Naive               445.48 s


And some 81x81 cases:

Code: Select all

Case 13: 81x81 (3959)
  Binary              163.01 s   
  Ternary             155.77 s
  Serial              235.59 s
  BBE                 140.85 s   
  Naive               153.17 s

Case 14: 81x81 (3958)
  Binary              475.14 s   
  Ternary             397.57 s
  Serial              456.12 s
  BBE                 447.68 s   
  Naive               366.17 s

Case 15: 81x81 (3957)
  Binary              465.31 s   
  Ternary             456.88 s
  Serial              526.04 s
  BBE                 491.77 s   
  Naive               377.62 s

Case 16: 81x81 (3956)
  Binary             1014.04 s   
  Ternary            1077.58 s
  Serial             1450.82 s
  BBE                1181.87 s   
  Naive              1079.38 s 


The bottom line appears to be that (with the exception of Serial) it's generally a tossup, and Naive actually wins in more cases than not, or is second to BBE or Binary.

There appears to be a cost of having extra variables at any scale (as evidenced by Serial performance), while the number of clauses only becomes problematic at larger grid sizes, when presumably the alt encoding methods will prove to be more significant.