ORk-Forcing-Whips, ORk-Contrad-Whips and ORk-whips

Advanced methods and approaches for solving Sudoku puzzles

ORk-Forcing-Whips, ORk-Contrad-Whips and ORk-whips

Postby denis_berthier » Mon Aug 01, 2022 8:27 am

.
ORk-Forcing-Whips

I introduced ordinary Forcing-Whips (based on a bivalue relation) long ago in PBCS1
I introduced Tridagon-Forcing-Whips (based on a tridagon link) more recently here: http://forum.enjoysudoku.com/the-tridagon-rule-t39859-31.html

The more general idea of ORk-Forcing-Whips is trivial, but there are small subtleties about complexity.

When an OR relation between k candidates (Z1 Z2 ... Zk, k > 1) has been proven, if there are k partial whips (of respective lengths p1, p2, ... pk), with respective targets Z1, Z2 ... Zk, then:
- if the last (right-linking) candidate of all the k partial whips is the same, then one can assert it as True;
- if a candidate is linked to the ends (i.e. the last right-linking candidates) of all the k partial whips, then it can be eliminated.
This is a trivial case of "reasoning by cases".
(For simplicity of formulation, a direct contradiction link between two candidates is considered as a partial-whip[0])

As k streams of reasoning must be followed in parallel and complexity is more or less exponential in the length of chains, the global length of the ORk-Forcing-Whip can be defined consistently in two and only two ways:
1) either consider that the OK-k relation has been proven independently and doesn't have to be counted in the complexity of the Forcing-Whip, in which case the total length is 1 + p1 + p2 ...+ pk (the +1 for consistency with the basic forcing-whips.
2) or consider that the OK-k relation doesn't lead to any elimination and must therefore be counted in the complexity of the Forcing-Whip, in which case the total length must be (length of the ORk relation) + p1 + p2 ...+ pk.

In the definition of Tridagon-Forcing-Whips, I have adopted the second view.

In the definition of the general ORk-Forcing-Whips, I'll adopt the first view. This corresponds to an extended resolution model, where OR relations can be asserted as intermediate results (in addition to only values and candidates). This is mainly intended for use with exotic patterns that lead to ORk relations. Typically in such cases, one wants to give some priority to the exotic pattern and to what can be deduced from it (while maintaining some consistency with the complexities of the ingredients, i.e. partial-whips)
(For Tridagon-Forcing-Whips, one will be able to choose any of the two views.)

[Edit]:added ORk-Contrad-Whips in the title.
[Edit2]:added ORk-Whips in the title.
Last edited by denis_berthier on Mon Sep 19, 2022 5:34 am, edited 2 times in total.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: OR-k-Forcing-Whips

Postby denis_berthier » Thu Aug 11, 2022 5:09 am

.
OR-k-Forcing-Whips based on anti-tridagon OR-k relations

Examples can be found in the following links:
tridagon + anti-tridagon OR3- and OR4- Forcing-Whips: http://forum.enjoysudoku.com/tanngrisnir-and-tanngnjostr-ser-11-7-te3-id-19252-t40126-3.html
anti-tridagon OR4-Forcing-Whips: http://forum.enjoysudoku.com/njor-r-ser-10-4-te3-id-289988-t40129-3.html
anti-tridagon OR4-Forcing-Whips: http://forum.enjoysudoku.com/the-tridagon-rule-t39859-100.html
anti-tridagon OR5-Forcing-Whips: http://forum.enjoysudoku.com/vor-r-ser-10-7-te3-id-155557-t40135-2.html
anti-tridagon OR5-Forcing-Whips: http://forum.enjoysudoku.com/mith-s-te3-min-expand-62886-63137-t40199-2.html
anti-tridagon OR5-Forcing-Whips in a puzzle with lots of guardians: http://forum.enjoysudoku.com/the-tridagon-rule-t39859-104.html
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: OR-k-Forcing-Whips

Postby denis_berthier » Thu Aug 11, 2022 5:23 am

.
ORk-Forcing-Whips based on bivalue, trivalue... relations

An obvious special case of ORk-Forcing-Whips appears when their base relation is a mere bivalue, trivalue... relation.
Note that, in such a case, the conventional length (1 + p1 + p2 +...) of the ORk-Forcing-Whip coincides with its normal length in CSP-Rules.
Considering the importance of these special cases, I've given them their own names:
Forcing2-Whips (equivalent to the old Forcing-whips) when k=2, with associated rating FW or F2W
Forcing3-Whips when k=3, with associated rating F3W
Forcing4-Whips when k=3, with associated rating F4W....

They can be selected in the SudoRules configuration file by setting global variable ?*Forcing2-Whips * (resp. ?*Forcing3-Whips *, ?*Forcing4-Whips *,...) to TRUE.
Note the implications (necessary for consistency of the ratings): Forcing4-Whips[n] => Forcing3-Whips[n] => Forcing2-Whips[n] =>Whips[n]

A first result of these new generic rules is an addition to the comparisons of ratings in the cbg-000 collection.
See here: http://forum.enjoysudoku.com/pattern-based-constraint-satisfaction-2nd-3rd-eds-t32567-15.html
and here for all the details: https://github.com/denis-berthier/CSP-Rules-Examples/tree/main/Sudoku/cbg-000
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: OR-k-Forcing-Whips

Postby denis_berthier » Tue Sep 06, 2022 5:49 am

.
ORk-whips[1], k≥2
I should have mentioned a special (but not rare) case of ORk-Forcing-Whips that appears when each of the k partial whips has length 0.
Though still an ORk-Forcing-Whip[1], the pattern can also be considered as a mere ORk-Whip[1] (by reversing the direction we look at it), because it has the main property of whips[1]: the target is linked to all the candidates in the ORk relation.

Example (with k=2) where this is enough to solve a puzzle with SER 11.7: puzzle #6530 in mith's list of 63,137 min-expand puzzles in T&E(3).
Code: Select all
     +-------+-------+-------+
     ! . 2 3 ! . . . ! 7 . 9 !
     ! 4 5 . ! . . . ! . . . !
     ! . . 9 ! 2 . 3 ! . 4 5 !
     +-------+-------+-------+
     ! 2 9 . ! . . . ! 5 7 . !
     ! 3 . . ! . . . ! 4 . 2 !
     ! . 4 . ! . 2 . ! . 9 3 !
     +-------+-------+-------+
     ! 5 3 . ! 9 . 8 ! . . . !
     ! . 7 . ! 6 . . ! . . . !
     ! . . . ! . 4 2 ! . . . !
     +-------+-------+-------+
.23...7.945.........92.3.4529....57.3.....4.2.4..2..9353.9.8....7.6.........42...;1400;22497
SER = 11.7

Code: Select all
Resolution state after Singles and whips[1]:
   +----------------------+----------------------+----------------------+
   ! 168    2      3      ! 1458   1568   1456   ! 7      168    9      !
   ! 4      5      1678   ! 178    16789  1679   ! 12368  12368  168    !
   ! 1678   168    9      ! 2      1678   3      ! 168    4      5      !
   +----------------------+----------------------+----------------------+
   ! 2      9      168    ! 1348   1368   146    ! 5      7      168    !
   ! 3      168    15678  ! 1578   156789 15679  ! 4      168    2      !
   ! 1678   4      15678  ! 1578   2      1567   ! 168    9      3      !
   +----------------------+----------------------+----------------------+
   ! 5      3      1246   ! 9      17     8      ! 126    126    1467   !
   ! 189    7      1248   ! 6      135    15     ! 12389  12358  148    !
   ! 1689   168    168    ! 1357   4      2      ! 13689  13568  1678   !
   +----------------------+----------------------+----------------------+
193 candidates.

Code: Select all
hidden-pairs-in-a-column: c3{n2 n4}{r7 r8} ==> r8c3≠8, r8c3≠1, r7c3≠6, r7c3≠1
whip[1]: r7n6{c9 .} ==> r9c7≠6, r9c8≠6, r9c9≠6
hidden-pairs-in-a-row: r2{n2 n3}{c7 c8} ==> r2c8≠8, r2c8≠6, r2c8≠1, r2c7≠8, r2c7≠6, r2c7≠1
z-chain[3]: c9n4{r8 r7} - r7n7{c9 c5} - r7n1{c5 .} ==> r8c9≠1
z-chain[3]: c8n5{r9 r8} - r8c6{n5 n1} - b7n1{r8c1 .} ==> r9c8≠1
t-whip[4]: r7n1{c9 c5} - b8n7{r7c5 r9c4} - r9n5{c4 c8} - r9n3{c8 .} ==> r9c7≠1
t-whip[5]: r7n1{c9 c5} - b8n7{r7c5 r9c4} - r9n5{c4 c8} - r9n3{c8 c7} - c7n9{r9 .} ==> r8c7≠1
   +----------------------+----------------------+----------------------+
   ! 168    2      3      ! 1458   1568   1456   ! 7      168    9      !
   ! 4      5      1678   ! 178    16789  1679   ! 23     23     168    !
   ! 1678   168    9      ! 2      1678   3      ! 168    4      5      !
   +----------------------+----------------------+----------------------+
   ! 2      9      168    ! 1348   1368   146    ! 5      7      168    !
   ! 3      168    15678  ! 1578   156789 15679  ! 4      168    2      !
   ! 1678   4      15678  ! 1578   2      1567   ! 168    9      3      !
   +----------------------+----------------------+----------------------+
   ! 5      3      24     ! 9      17     8      ! 126    126    1467   !
   ! 189    7      24     ! 6      135    15     ! 2389   12358  48     !
   ! 1689   168    168    ! 1357   4      2      ! 389    358    178    !
   +----------------------+----------------------+----------------------+


Code: Select all
OR2-anti-tridagon[12] (type antidiag) for digits 6, 8 and 1 in blocks:
        b1, with cells: r1c1, r2c3, r3c2
        b3, with cells: r1c8, r2c9, r3c7
        b4, with cells: r6c1, r4c3, r5c2
        b6, with cells: r6c7, r4c9, r5c8
with 2 guardians: n7r2c3 n7r6c1

OR2-whip[1] based on OR2-anti-tridagon[12] for n7r2c3 and  n7r6c1:
   || n7r2c3 -
   || n7r6c1 -
 ==> r6c3≠7, r5c3≠7

The end is easy:
Code: Select all
singles ==> r6c1=7, r2c3=7, r3c5=7, r7c5=1, r8c6=5, r8c5=3, r9c4=7, r5c6=7, r5c5=9, r2c6=9, r1c5=5, r7c9=7, r8c9=4, r8c3=2, r7c3=4, r4c4=3, r4c6=4, r1c4=4, r9c8=5, r9c7=3, r2c7=2, r2c8=3, r7c7=6, r7c8=2, r8c7=9, r9c1=9
whip[1]: c1n6{r3 .} ==> r3c2≠6
hidden-single-in-a-row ==> r3c1=6
whip[1]: b2n8{r2c5 .} ==> r2c9≠8
x-wing-in-rows: n8{r1 r8}{c1 c8} ==> r5c8≠8
x-wing-in-columns: n6{c5 c9}{r2 r4} ==> r4c3≠6
finned-x-wing-in-columns: n1{c6 c7}{r6 r1} ==> r1c8≠1
biv-chain[2]: c7n1{r6 r3} - r2n1{c9 c4} ==> r6c4≠1
finned-swordfish-in-columns: n1{c8 c1 c4}{r5 r8 r1} ==> r1c6≠1
stte
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: ORk-Forcing-Whips and ORk-Contrad-Whips

Postby denis_berthier » Tue Sep 06, 2022 10:43 am

.
ORk-Contrad-Whips

When an application-specific ORk relation between k candidates has been proven, the most natural way to take advantage of it is via the generic ORk-Forcing-Whips defined in the first post of this thread.
In this case, the ORk relation serves as a natural starting point for the forcing whip.

However, there is also another way of using it to eliminate candidates. AFAIK, the first time it has been used this way is by DEFISE, in this puzzle: http://forum.enjoysudoku.com/23427-more-anti-tridagon-guardians-t40295.html

The formal definition is almost obvious:
given an ORk relation between candidates C1, C2, ... Ck, an ORk-Contradiction-Whip[n] (or ORk-Contrad-Whip[n] for short) based on the ORk relation, with target Z, is an ordinary partial-whip[n-1] W with target Z, such that each of the Ck's is linked to (at least) a right-linking candidate of W.
In such a situation, the target Z can be eliminated.

Proof: obvious. If Z was True, all the right-linking candidates would be True and there would be no possibility for any of the Ci's to be True.
Here, the ORk relation plays the same role as an n-th CSP-Variable.

Note: obviously, ORk-Forcing-Whips and ORk-Contrad-Whips could be extended to g-Whips, Braids and g-Braids.

Here is a simple example, with 2 OR2CW3 eliminations: #950 in mith's list of 63137 min-expands
Code: Select all
+-------+-------+-------+
! . 2 . ! . . . ! . . 9 !
! . . . ! . 8 9 ! 1 3 2 !
! . . . ! . . . ! 5 6 . !
+-------+-------+-------+
! 2 3 . ! 8 9 . ! 4 7 . !
! . 8 7 ! . 2 4 ! 3 9 . !
! . . . ! 3 . 7 ! . . . !
+-------+-------+-------+
! 3 . 8 ! . 7 . ! . . . !
! . 9 2 ! . 4 . ! . . . !
! 7 4 . ! . . . ! . . . !
+-------+-------+-------+
.2......9....89132......56.23.89.47..87.2439....3.7...3.8.7.....92.4....74.......;218;256011

Code: Select all
Resolution state after Singles and whips[1]:
   +----------------------+----------------------+----------------------+
   ! 14568  2      13456  ! 14567  1356   1356   ! 78     48     9      !
   ! 456    567    456    ! 4567   8      9      ! 1      3      2      !
   ! 1489   17     1349   ! 1247   13     123    ! 5      6      478    !
   +----------------------+----------------------+----------------------+
   ! 2      3      156    ! 8      9      156    ! 4      7      156    !
   ! 156    8      7      ! 156    2      4      ! 3      9      156    !
   ! 14569  156    14569  ! 3      156    7      ! 268    1258   1568   !
   +----------------------+----------------------+----------------------+
   ! 3      156    8      ! 12569  7      1256   ! 269    1245   1456   !
   ! 156    9      2      ! 156    4      13568  ! 678    158    135678 !
   ! 7      4      156    ! 12569  1356   123568 ! 2689   1258   13568  !
   +----------------------+----------------------+----------------------+
184 candidates.

Code: Select all
hidden-pairs-in-a-row: r6{n4 n9}{c1 c3} ==> r6c3≠6, r6c3≠5, r6c3≠1, r6c1≠6, r6c1≠5, r6c1≠1
   +----------------------+----------------------+----------------------+
   ! 14568  2      13456  ! 14567  1356   1356   ! 78     48     9      !
   ! 456    567    456    ! 4567   8      9      ! 1      3      2      !
   ! 1489   17     1349   ! 1247   13     123    ! 5      6      478    !
   +----------------------+----------------------+----------------------+
   ! 2      3      156    ! 8      9      156    ! 4      7      156    !
   ! 156    8      7      ! 156    2      4      ! 3      9      156    !
   ! 49     156    49     ! 3      156    7      ! 268    1258   1568   !
   +----------------------+----------------------+----------------------+
   ! 3      156    8      ! 12569  7      1256   ! 269    1245   1456   !
   ! 156    9      2      ! 156    4      13568  ! 678    158    135678 !
   ! 7      4      156    ! 12569  1356   123568 ! 2689   1258   13568  !
   +----------------------+----------------------+----------------------+

OR2-anti-tridagon[12] (type antidiag) for digits 1, 5 and 6 in blocks:
        b4, with cells: r4c3, r5c1, r6c2
        b5, with cells: r4c6, r5c4, r6c5
        b7, with cells: r9c3, r8c1, r7c2
        b8, with cells: r9c5, r8c4, r7c6
with 2 guardians: n2r7c6 n3r9c5

OR2-contrad-whip[3] based on OR2-anti-tridagon[12] for n3r9c5 and  n2r7c6:
   partial-whip[2]: r3c5{n1 n3} - r3c6{n3 n2} -
 ==> r3c1≠1

OR2-contrad-whip[3] based on OR2-anti-tridagon[12] for n3r9c5 and  n2r7c6:
   partial-whip[2]: r3c5{n1 n3} - r3c6{n3 n2} -
 ==> r3c2≠1

Code: Select all
singles ==> r3c2=7, r2c4=7, r1c7=7, r8c9=7, r9c9=3, r8c6=3, r9c6=8
whip[1]: r2n4{c3 .} ==> r1c1≠4, r1c3≠4, r3c1≠4, r3c3≠4
whip[1]: r2n5{c3 .} ==> r1c1≠5, r1c3≠5
whip[1]: r2n6{c3 .} ==> r1c1≠6, r1c3≠6
finned-x-wing-in-columns: n1{c2 c9}{r7 r6} ==> r6c8≠1
whip[1]: c8n1{r9 .} ==> r7c9≠1
   +-------------------+-------------------+-------------------+
   ! 18    2     13    ! 1456  1356  156   ! 7     48    9     !
   ! 456   56    456   ! 7     8     9     ! 1     3     2     !
   ! 89    7     139   ! 124   13    12    ! 5     6     48    !
   +-------------------+-------------------+-------------------+
   ! 2     3     156   ! 8     9     156   ! 4     7     156   !
   ! 156   8     7     ! 156   2     4     ! 3     9     156   !
   ! 49    156   49    ! 3     156   7     ! 268   258   1568  !
   +-------------------+-------------------+-------------------+
   ! 3     156   8     ! 12569 7     1256  ! 269   1245  456   !
   ! 156   9     2     ! 156   4     3     ! 68    158   7     !
   ! 7     4     156   ! 12569 156   8     ! 269   125   3     !
   +-------------------+-------------------+-------------------+

tridagon for digits 1, 5 and 6 in blocks:
        b8, with cells: r7c6 (target cell), r8c4, r9c5
        b7, with cells: r7c2, r8c1, r9c3
        b5, with cells: r4c6, r5c4, r6c5
        b4, with cells: r4c3, r5c1, r6c2
 ==> r7c6≠1,5,6

Code: Select all
singles ==> r7c6=2, r3c6=1, r3c5=3, r3c3=9, r3c1=8, r1c1=1, r1c3=3, r3c9=4, r1c8=8, r3c4=2, r6c3=4, r6c1=9, r2c1=4, r8c7=8, r6c9=8, r7c8=4, r1c4=4
finned-x-wing-in-rows: n1{r7 r6}{c2 c4} ==> r5c4≠1
singles ==> r6c5=1, r4c3=1, r5c9=1, r7c2=1
naked-pairs-in-a-row: r9{c3 c5}{n5 n6} ==> r9c8≠5, r9c7≠6, r9c4≠6, r9c4≠5
whip[1]: b9n6{r7c9 .} ==> r7c4≠6
finned-x-wing-in-columns: n5{c8 c1}{r8 r6} ==> r6c2≠5
stte


Here is a harder example, with 7 OR3/4-CW eliminations: #25911 in the same list
Code: Select all
+-------+-------+-------+
! 1 . 3 ! . . . ! . . . !
! . 5 . ! 1 . 9 ! . . 6 !
! 6 9 . ! 2 3 . ! . . . !
+-------+-------+-------+
! 2 . . ! . . . ! 4 . 8 !
! 3 6 . ! . . . ! 1 2 7 !
! . . . ! . . 2 ! . 9 5 !
+-------+-------+-------+
! 5 . 6 ! . 2 3 ! . . . !
! . . 1 ! 6 9 . ! . 5 . !
! 9 . . ! 5 . 1 ! . . . !
+-------+-------+-------+
1.3.......5.1.9..669.23....2.....4.836....127.....2.955.6.23.....169..5.9..5.1...;5250;73296
SER = 11.0

Code: Select all
Resolution state after Singles and whips[1]:
   +-------------------+-------------------+-------------------+
   ! 1     2478  3     ! 478   45678 45678 ! 25789 478   249   !
   ! 478   5     2478  ! 1     478   9     ! 2378  3478  6     !
   ! 6     9     478   ! 2     3     4578  ! 578   1478  14    !
   +-------------------+-------------------+-------------------+
   ! 2     17    579   ! 379   1567  567   ! 4     36    8     !
   ! 3     6     4589  ! 489   458   458   ! 1     2     7     !
   ! 478   1478  478   ! 3478  14678 2     ! 36    9     5     !
   +-------------------+-------------------+-------------------+
   ! 5     478   6     ! 478   2     3     ! 789   1478  149   !
   ! 478   23478 1     ! 6     9     478   ! 278   5     234   !
   ! 9     23478 2478  ! 5     478   1     ! 2678  4678  234   !
   +-------------------+-------------------+-------------------+
169 candidates.

Code: Select all
hidden-pairs-in-a-column: c3{n5 n9}{r4 r5} ==> r5c3≠8, r5c3≠4, r4c3≠7
whip[1]: r5n4{c6 .} ==> r6c4≠4, r6c5≠4
whip[1]: r5n8{c6 .} ==> r6c4≠8, r6c5≠8
z-chain[5]: c2n3{r8 r9} - b7n2{r9c2 r9c3} - r2n2{c3 c7} - r8n2{c7 c9} - r8n3{c9 .} ==> r8c2≠4, r8c2≠8, r8c2≠7
whip[5]: c8n6{r9 r4} - r4n3{c8 c4} - r6c4{n3 n7} - r7n7{c4 c2} - r4n7{c2 .} ==> r9c8≠7
   +-------------------+-------------------+-------------------+
   ! 1     2478  3     ! 478   45678 45678 ! 25789 478   249   !
   ! 478   5     2478  ! 1     478   9     ! 2378  3478  6     !
   ! 6     9     478   ! 2     3     4578  ! 578   1478  14    !
   +-------------------+-------------------+-------------------+
   ! 2     17    59    ! 379   1567  567   ! 4     36    8     !
   ! 3     6     59    ! 489   458   458   ! 1     2     7     !
   ! 478   1478  478   ! 37    167   2     ! 36    9     5     !
   +-------------------+-------------------+-------------------+
   ! 5     478   6     ! 478   2     3     ! 789   1478  149   !
   ! 478   23    1     ! 6     9     478   ! 278   5     234   !
   ! 9     23478 2478  ! 5     478   1     ! 2678  468   234   !
   +-------------------+-------------------+-------------------+

Code: Select all
OR3-anti-tridagon[12] (type diag) for digits 4, 7 and 8 in blocks:
        b1, with cells: r1c2, r2c1, r3c3
        b2, with cells: r1c4, r2c5, r3c6
        b7, with cells: r7c2, r8c1, r9c3
        b8, with cells: r7c4, r8c6, r9c5
with 3 guardians: n2r1c2 n5r3c6 n2r9c3

OR3-contrad-whip[4] based on OR3-anti-tridagon[12] for n2r9c3, n5r3c6 and  n2r1c2:
   partial-whip[3]: c3n2{r9 r2} - r1n2{c2 c7} - c7n5{r1 r3} -
 ==> r9c9≠2

OR3-contrad-whip[5] based on OR3-anti-tridagon[12] for n2r1c2, n5r3c6 and  n2r9c3:
   partial-whip[4]: r8c2{n3 n2} - c9n2{r8 r1} - r1n9{c9 c7} - c7n5{r1 r3} -
 ==> r9c2≠3

singles ==> r8c2=3, r9c9=3
whip[1]: r8n2{c9 .} ==> r9c7≠2
t-whip[5]: c2n2{r9 r1} - r2n2{c3 c7} - c7n3{r2 r6} - r6c4{n3 n7} - r4n7{c6 .} ==> r9c2≠7

OR3-contrad-whip[5] based on OR3-anti-tridagon[12] for n2r9c3, n5r3c6 and  n2r1c2:
   partial-whip[4]: r2n2{c7 c3} - r1n2{c2 c9} - r1n9{c9 c7} - c7n5{r1 r3} -
 ==> r8c7≠2

hidden-single-in-a-block ==> r8c9=2

OR3-contrad-whip[4] based on OR3-anti-tridagon[12] for n2r1c2, n5r3c6 and  n2r9c3:
   partial-whip[3]: b1n2{r1c2 r2c3} - b3n2{r2c7 r1c7} - c7n5{r1 r3} -
 ==> r1c2≠4

OR3-contrad-whip[4] based on OR3-anti-tridagon[12] for n2r1c2, n5r3c6 and  n2r9c3:
   partial-whip[3]: b1n2{r1c2 r2c3} - b3n2{r2c7 r1c7} - c7n5{r1 r3} -
 ==> r1c2≠7

OR3-contrad-whip[4] based on OR3-anti-tridagon[12] for n2r1c2, n5r3c6 and  n2r9c3:
   partial-whip[3]: r2n2{c7 c3} - r1c2{n2 n8} - b2n8{r1c4 r3c6} -
 ==> r2c7≠8

OR3-contrad-whip[4] based on OR3-anti-tridagon[12] for n2r1c2, n5r3c6 and  n2r9c3:
   partial-whip[3]: b1n2{r1c2 r2c3} - b3n2{r2c7 r1c7} - c7n5{r1 r3} -
 ==> r1c2≠8

stte


[Edit 1]:
Note 1: Both ORk-Forcing-Whips and ORk-Contrad-Whips are available in CSP-Rules / SudoRules, for k=1, 2, ...6 and n = 1...36
Note 2: ORk-Forcing-Whips and ORk-Contrad-Whips can be activated at the same time; they are built on the same partial-whips
Note 3: a first, quick evaluation, to be made more precise, shows ORk-Forcing-Whips are more powerful than ORk-Contrad-Whips (with same k and n)

[Edit2]: change the proof. This version is more in the spirit of whips (impossibility occurring in the final CSP / ORk).
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: ORk-Forcing-Whips and ORk-Contrad-Whips

Postby denis_berthier » Fri Sep 09, 2022 10:40 am

.
a reader of [PBCS] and user of CSP-Rules that prefers to remain anonymous wrote:You've always said that you don't like forcing-whips but now you are promoting ORk-Forcing-Whips. Isn't that contradictory?

Good question. And very easy to answer.

Forcing-chains in general are very inelegant, because they start with a big OR and they suppose one follows two (or more) streams of reasoning in parallel. Mathematically, they amount to reasoning by cases. With respect to T&E, they amount to having some T&E step right at the start (any OR-branching step in a chain introduces one level of T&E).

Ordinary forcing whips have no argument to make forgive this inelegance: they are not really more powerful than whips (see section 6.5.1 of [PBCS3]).

Tridagon-based ORk-Forcing-Whips are radically different:
1) in terms of resolution power (as I will soon show in the tridagon thread (http://forum.enjoysudoku.com/the-tridagon-rule-t39859.html)
2) and in terms of focus: their OR starting point is concentrated on very specific candidates (defined by the ORk relation - i.e. in the current context, the guardians of a precise and generally unique anti-tridagon pattern).
.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: ORk-Forcing-Whips, ORk-Contrad-Whips and ORk-whips

Postby denis_berthier » Mon Sep 19, 2022 5:41 am

.
ORk-whips

An ORk-whip is a pattern more general than my previously defined ORk-contrad-whips: the ORk part may appear at another place than the final (contradiction) one.
Informally speaking, an ORk-whip (based on some ORk-relation, e.g. an anti-tridagon one) is like a whip, except that some of its CSP-Variables is replaced by an ORk relation, where k-1 candidates are linked to the target or to previous right-linking candidates and the remaining one is used as a right linking-candidate for the next step.

The notation for an ORk-whip based on an ORk-relation is as follows:
- the full name is ORname-ORk-whip[n], with "n" the total length as usual, "k" the size or the OR relation and "OR name" the short name of this relation.
- I use double curly braces for the ORk part (to recall that it's not a CSP-Variable).


Example based on an anti-tridagon OR3 relation:
Trid-OR3-whip[5]: r7c1{n1 n6} - r9n6{c1 c4} - r7c6{n6 n8} - OR3{{n8r5c6 n6r3c4 | n4r1c5}} - r7c5{n4 .} ==> r7c3≠1

For a first fully developed example, see here: http://forum.enjoysudoku.com/1359-in-t-e-3-min-expands-t40363-5.html
Last edited by denis_berthier on Mon Sep 19, 2022 6:05 pm, edited 1 time in total.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: ORk-Forcing-Whips, ORk-Contrad-Whips and ORk-whips

Postby denis_berthier » Mon Sep 19, 2022 5:50 am

.
Here is an easier example, #1167 in mith's list of 63137 min-expand puzzle in T&E(3):
Code: Select all
+-------+-------+-------+
! . . . ! 4 5 . ! . 8 . !
! 4 5 . ! . . . ! 2 . 3 !
! 6 8 . ! 3 . 2 ! 4 5 . !
+-------+-------+-------+
! . . . ! . 3 4 ! 5 . 8 !
! . . . ! 6 . 5 ! . . 2 !
! . . 5 ! 8 2 . ! 6 . . !
+-------+-------+-------+
! . 7 . ! . . . ! . . 5 !
! . 9 . ! . . . ! 8 . 4 !
! . . 2 ! . . 3 ! . . . !
+-------+-------+-------+
...45..8.45....2.368.3.245.....345.8...6.5..2..582.6...7......5.9....8.4..2..3...;234;17556
SER = 11.7


Code: Select all
Resolution state after Singles (and whips[1]):
   +----------------------+----------------------+----------------------+
   ! 12379  123    1379   ! 4      5      1679   ! 179    8      1679   !
   ! 4      5      179    ! 179    16789  16789  ! 2      1679   3      !
   ! 6      8      179    ! 3      179    2      ! 4      5      179    !
   +----------------------+----------------------+----------------------+
   ! 1279   126    1679   ! 179    3      4      ! 5      179    8      !
   ! 13789  134    134789 ! 6      179    5      ! 1379   13479  2      !
   ! 1379   134    5      ! 8      2      179    ! 6      13479  179    !
   +----------------------+----------------------+----------------------+
   ! 138    7      13468  ! 129    14689  1689   ! 139    12369  5      !
   ! 135    9      136    ! 1257   167    167    ! 8      12367  4      !
   ! 158    146    2      ! 1579   146789 3      ! 179    1679   1679   !
   +----------------------+----------------------+----------------------+
189 candidates.

As usual, using the simplest-first strategy, let's first do some easy cleaning:
Code: Select all
hidden-pairs-in-a-column: c3{n4 n8}{r5 r7} ==> r7c3≠6, r7c3≠3, r7c3≠1, r5c3≠9, r5c3≠7, r5c3≠3, r5c3≠1
biv-chain[3]: r9n8{c1 c5} - b8n4{r9c5 r7c5} - r7c3{n4 n8} ==> r7c1≠8
biv-chain[3]: r9n8{c5 c1} - r7c3{n8 n4} - b8n4{r7c5 r9c5} ==> r9c5≠1, r9c5≠6, r9c5≠7, r9c5≠9
z-chain[3]: r9n7{c9 c4} - c4n5{r9 r8} - r8n2{c4 .} ==> r8c8≠7
whip[1]: b9n7{r9c9 .} ==> r9c4≠7
z-chain[3]: r7c1{n1 n3} - b9n3{r7c7 r8c8} - c8n2{r8 .} ==> r7c8≠1
z-chain[4]: r7c1{n1 n3} - r8n3{c3 c8} - r8n2{c8 c4} - r8n5{c4 .} ==> r8c1≠1
   +-------------------+-------------------+-------------------+
   ! 12379 123   1379  ! 4     5     1679  ! 179   8     1679  !
   ! 4     5     179   ! 179   16789 16789 ! 2     1679  3     !
   ! 6     8     179   ! 3     179   2     ! 4     5     179   !
   +-------------------+-------------------+-------------------+
   ! 1279  126   1679  ! 179   3     4     ! 5     179   8     !
   ! 13789 134   48    ! 6     179   5     ! 1379  13479 2     !
   ! 1379  134   5     ! 8     2     179   ! 6     13479 179   !
   +-------------------+-------------------+-------------------+
   ! 13    7     48    ! 129   14689 1689  ! 139   2369  5     !
   ! 35    9     136   ! 1257  167   167   ! 8     1236  4     !
   ! 158   146   2     ! 159   48    3     ! 179   1679  1679  !
   +-------------------+-------------------+-------------------+

OR3-anti-tridagon[12] for digits 7, 9 and 1 in blocks:
        b2, with cells: r1c6, r2c4, r3c5
        b3, with cells: r1c7, r2c8, r3c9
        b5, with cells: r6c6, r4c4, r5c5
        b6, with cells: r6c9, r4c8, r5c7
with 3 guardians: n6r1c6 n6r2c8 n3r5c7


The part with the ORk-whips;
Trid-OR3-whip[4]: c8n2{r7 r8} - b9n3{r8c8 r7c7} - OR3{{n3r5c7 n6r2c8 | n6r1c6}} - c9n6{r1 .} ==> r7c8≠6
whip[1]: r7n6{c6 .} ==> r8c5≠6, r8c6≠6
naked-pairs-in-a-block: b8{r8c5 r8c6}{n1 n7} ==> r9c4≠1, r8c4≠7, r8c4≠1, r7c6≠1, r7c5≠1, r7c4≠1
whip[1]: b8n1{r8c6 .} ==> r8c3≠1, r8c8≠1
hidden-pairs-in-a-column: c4{n1 n7}{r2 r4} ==> r4c4≠9, r2c4≠9
whip[1]: c4n9{r9 .} ==> r7c5≠9, r7c6≠9
naked-triplets-in-a-column: c5{r3 r5 r8}{n1 n9 n7} ==> r2c5≠9, r2c5≠7, r2c5≠1
z-chain[3]: b7n1{r9c1 r9c2} - c2n6{r9 r4} - r4n2{c2 .} ==> r4c1≠1
z-chain[3]: c3n1{r3 r4} - r4n6{c3 c2} - c2n2{r4 .} ==> r1c2≠1
Trid-OR3-whip[4]: b7n3{r8c1 r8c3} - r8n6{c3 c8} - OR3{{n6r2c8 n3r5c7 | n6r1c6}} - c9n6{r1 .} ==> r5c1≠3
Trid-OR3-whip[4]: c8n2{r8 r7} - b9n3{r7c8 r7c7} - OR3{{n3r5c7 n6r2c8 | n6r1c6}} - c9n6{r1 .} ==> r8c8≠6


The end is easy:
Code: Select all
singles ==> r8c3=6,r4c2=6, r4c1=2, r1c2=2, r1c3=3, r6c1≠3
hidden-pairs-in-a-row: r6{n3 n4}{c2 c8} ==> r6c8≠9, r6c8≠7, r6c8≠1, r6c2≠1
biv-chain[2]: r7n1{c7 c1} - c2n1{r9 r5} ==> r5c7≠1
biv-chain[3]: c2n1{r5 r9} - r7c1{n1 n3} - c7n3{r7 r5} ==> r5c2≠3
singles ==> r6c2=3, r6c8=4
z-chain[3]: r4n9{c8 c3} - r2n9{c3 c6} - b5n9{r6c6 .} ==> r5c8≠9
z-chain[3]: r4n9{c8 c3} - r3n9{c3 c5} - b5n9{r5c5 .} ==> r6c9≠9
t-whip[3]: r4n9{c8 c3} - r6n9{c1 c6} - r2n9{c6 .} ==> r9c8≠9, r7c8≠9
naked-pairs-in-a-block: b9{r7c8 r8c8}{n2 n3} ==> r7c7≠3
singles ==> r5c7=3, r4c8=9
whip[1]: b4n9{r6c1 .} ==> r1c1≠9
biv-chain[2]: b6n1{r6c9 r5c8} - c2n1{r5 r9} ==> r9c9≠1
finned-swordfish-in-columns: n1{c8 c2 c4}{r2 r9 r5} ==> r5c5≠1
biv-chain[3]: r4n7{c3 c4} - r5c5{n7 n9} - b4n9{r5c1 r6c1} ==> r6c1≠7
biv-chain[2]: b6n7{r6c9 r5c8} - c1n7{r5 r1} ==> r1c9≠7
biv-chain[3]: c7n7{r9 r1} - c1n7{r1 r5} - b6n7{r5c8 r6c9} ==> r9c9≠7
biv-chain[3]: r9n7{c7 c8} - r5c8{n7 n1} - c2n1{r5 r9} ==> r9c7≠1
biv-chain[3]: r2c4{n7 n1} - c5n1{r3 r8} - b8n7{r8c5 r8c6} ==> r1c6≠7, r2c6≠7
biv-chain[2]: b2n7{r3c5 r2c4} - r4n7{c4 c3} ==> r3c3≠7
x-wing-in-columns: n7{c3 c4}{r2 r4} ==> r2c8≠7
finned-x-wing-in-rows: n7{r3 r6}{c9 c5} ==> r5c5≠7
singles ==> r5c5=9,> r6c1=9
naked-pairs-in-a-block: b2{r2c4 r3c5}{n1 n7} ==> r2c6≠1, r1c6≠1
biv-chain[2]: b2n1{r3c5 r2c4} - r4n1{c4 c3} ==> r3c3≠1
stte
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: ORk-Forcing-Whips, ORk-Contrad-Whips and ORk-whips

Postby denis_berthier » Sun Jan 08, 2023 9:11 am

.
Previously, I have spoken of the ultra-persitency of ORk-relations (see the Augmented User Manual own GitHub or on ResearchGate https://www.researchgate.net/publication/365186265_Augmented_User_Manual_for_CSP-Rules-V21).

This post is about splitting ORk-relations. The idea of doing such things was more or less inspired by solutions proposed by other people in the Puzzles section of this forum. What I've done is find a generic way to express some of the ad hoc arguments made there.

First define a c-chain[n] as a sequence of n+1 different candidates C1... Cn+1 such that for each 1 ≤ i ≤ n, Ci and Ci+1 are related by a (3D) bivalue relation.
It is obvious that, if n is even then C1 and Cn+1 have the same truth value.
This is a generic definition and a generic property.

Theorem (generic): given an ORk relation between candidates Z1, ... Zk, if there is any even c-chain[n] between two of the Zi's, say Za and Zb, then the original ORk-relation can be split into two ORk-1 relations, between k-1 candidates, respectively {Z1, ... Zk}-Za and {Z1, ... Zk}-Zb.
[Edit, added]:Corollary: if k=2, both Z1 and Z2 can be asserted.

Proof: obvious

Note: "between two of the Zi's, say Za and Zb" means that C1 = Za and Cn+1 = Zb

For an example of using the theorem, see second post here: http://forum.enjoysudoku.com/51007-in-63137-t-e-3-min-expands-t40721-3.html and next post.
For an example of using the corollary, see here: http://forum.enjoysudoku.com/other-hard-one-from-mith-s-trivalue-oddagon-list-t40727-4.html.
For an example of using the theorem repeatedly in conjunction with ORk-reduction (ultra-persistency, see here: http://forum.enjoysudoku.com/1182-in-63137-list-of-t-e-3-min-expands-t40739-3.html

Note: the way such splitting is coded in CSP-Rules is still experimental.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris

Re: ORk-Forcing-Whips, ORk-Contrad-Whips and ORk-whips

Postby denis_berthier » Fri Jan 13, 2023 12:21 pm

.
a reader of this thread wrote:How do you know that c-chains of even lengths are the only way ORk-relations can be reduced?


1) ORk relations are reduced when a guardian is eliminated (this is part of their ultra-persistency in CSP-Rules ).
But your question (about my previous post) is about a totally different topic.

2) Indeed, I don't know what you claim. On the contrary, there are probably many kinds of chain patterns that could be used as a basis for reducing ORk-relations.

What I've been looking for is rules that:
- allowed to reduce the number of guardians; it appeared that trying to split ORk-relations (instead of trying to reduce them, i.e. to eliminate guardians from them) was the most natural thing to do;
- involved only generic conditions (with no ad-hoc reasoning);
- were simple enough to be integrated in the hierarchy of resolution rules (though they are not resolution rules).
The last two conditions are trivially satisfied by c-chains (a c-chain[n] being posited at level Ln, just before the ORk-chains[n] that might rely on their results).

Now, can these splitting rules take into account the different ad hoc reductions that have been proposed for anti-tridagon puzzles in the Puzzles section? I haven't checked and it's not that important here for the following reason:
my approach has always been to find universal rules/techniques that can be applied in a systematic way. They may not be the smartest ones for a particular puzzle, but they aim at being the smartest ones in the mean.
.
denis_berthier
2010 Supporter
 
Posts: 3967
Joined: 19 June 2007
Location: Paris


Return to Advanced solving techniques