• Log InLog In
  • Register
Liquid`
Team Liquid Liquipedia
EDT 01:26
CEST 07:26
KST 14:26
  • Home
  • Forum
  • Calendar
  • Streams
  • Liquipedia
  • Features
  • Store
  • EPT
  • TL+
  • StarCraft 2
  • Brood War
  • Smash
  • Heroes
  • Counter-Strike
  • Overwatch
  • Liquibet
  • Fantasy StarCraft
  • TLPD
  • StarCraft 2
  • Brood War
  • Blogs
Forum Sidebar
Events/Features
News
Featured News
TL Team Map Contest #5: Presented by Monster Energy2Code S RO8 Preview: herO, Zoun, Bunny, Classic7Code S RO8 Preview: Rogue, GuMiho, Solar, Maru3BGE Stara Zagora 2025: Info & Preview27Code S RO12 Preview: GuMiho, Bunny, SHIN, ByuN3
Community News
Code S RO8 Results + RO4 Bracket (2025 Season 2)4BGE Stara Zagora 2025 - Replay Pack2Weekly Cups (June 2-8): herO doubles down1[BSL20] ProLeague: Bracket Stage & Dates9GSL Ro4 and Finals moved to Sunday June 15th13
StarCraft 2
General
The SCII GOAT: A statistical Evaluation Code S RO8 Results + RO4 Bracket (2025 Season 2) How herO can make history in the Code S S2 finals TL Team Map Contest #5: Presented by Monster Energy Jim claims he and Firefly were involved in match-fixing
Tourneys
[GSL 2025] Code S: Season 2 - Ro8 - Group A [GSL 2025] Code S: Season 2 - Ro8 - Group B RSL: Revival, a new crowdfunded tournament series SOOPer7s Showmatches 2025 Sparkling Tuna Cup - Weekly Open Tournament
Strategy
[G] Darkgrid Layout Simple Questions Simple Answers [G] PvT Cheese: 13 Gate Proxy Robo
Custom Maps
[UMS] Zillion Zerglings
External Content
Mutation # 477 Slow and Steady Mutation # 476 Charnel House Mutation # 475 Hard Target Mutation # 474 Futile Resistance
Brood War
General
BGH auto balance -> http://bghmmr.eu/ BW General Discussion FlaSh Witnesses SCV Pull Off the Impossible vs Shu StarCraft & BroodWar Campaign Speedrun Quest Will foreigners ever be able to challenge Koreans?
Tourneys
[Megathread] Daily Proleagues [BSL20] ProLeague Bracket Stage - Day 4 [BSL20] ProLeague Bracket Stage - Day 3 [ASL19] Grand Finals
Strategy
I am doing this better than progamers do. [G] How to get started on ladder as a new Z player
Other Games
General Games
Stormgate/Frost Giant Megathread Path of Exile Nintendo Switch Thread Beyond All Reason What do you want from future RTS games?
Dota 2
Official 'what is Dota anymore' discussion
League of Legends
Who’s Getting the Effortless-Chic Look Just Right?
Heroes of the Storm
Simple Questions, Simple Answers Heroes of the Storm 2.0
Hearthstone
Heroes of StarCraft mini-set
TL Mafia
TL Mafia Community Thread Vanilla Mini Mafia
Community
General
Things Aren’t Peaceful in Palestine US Politics Mega-thread UK Politics Mega-thread Russo-Ukrainian War Thread Vape Nation Thread
Fan Clubs
Maru Fan Club Serral Fan Club
Media & Entertainment
Korean Music Discussion [Manga] One Piece
Sports
NHL Playoffs 2024 TeamLiquid Health and Fitness Initiative For 2023 2024 - 2025 Football Thread Formula 1 Discussion
World Cup 2022
Tech Support
Computer Build, Upgrade & Buying Resource Thread
TL Community
The Automated Ban List
Blogs
A Better Routine For Progame…
TrAiDoS
StarCraft improvement
iopq
Heero Yuy & the Tax…
KrillinFromwales
I was completely wrong ab…
jameswatts
Need Your Help/Advice
Glider
Trip to the Zoo
micronesia
Customize Sidebar...

Website Feedback

Closed Threads



Active: 27146 users

[R] I need a name - Page 3

Blogs > berated-
Post a Reply
Prev 1 2 3 All
BroOd
Profile Blog Joined April 2003
Austin10831 Posts
April 28 2008 21:50 GMT
#41
Truedoku
ModeratorSIRL and JLIG.
azndsh
Profile Blog Joined August 2006
United States4447 Posts
Last Edited: 2008-04-28 22:23:12
April 28 2008 22:22 GMT
#42
On April 28 2008 23:57 berated- wrote:
Show nested quote +
On April 28 2008 14:18 azndsh wrote:
aren't sudoku SAT solvers extremely inefficient? unless you formulate the problem way differently from what I have in mind


That's really kind of irrelevant to the project. I'm taking a boolean satisfiability class and we have to do a final project related to boolean equations. Considering I'm not a total badass, I knew I wasn't going to come up with the next great thing such as WalkSAT or Davis Putnam or GSAT, any of the SAT solving techniques that were monumental upon release. So I was left with two options, I could either find some current research and write an 8 page paper on it, or I could code up an algorithm.

Reading conference papers didn't strike me as overly fun, so I went with a coding project. I could then do something like just pass a boolean equation to an algorithm and try to solve it, which would have got the job done but is a little bland. So I sought out something that would at least be enjoyable.

As for the original question, my first response would have to be no. Using DP, a true sudoku puzzle ( one with only one answer and requiring no search techniques ) would actually require only unit propagation while solving the algorithm. Of course, you would have to define what it is inefficient compared to. Its obviously better than a try all possibilities solution. Are there other algorithms out there that might do better? I have no idea. I wasnt studying Sudoku, I was studying boolean equations, so I apologize that I can't give you a better answer.

I guess you would have to make that judgment call:

My technique ( learned from the work of others who have already done this - I'm just an undergrad, I can't be doing monumental work in my field ):

There are 729 variables - one for every possible number in every possible cell. These are represented by a 3 digit string - the row, the column, and the number.

So 111 refers to a one being in the upper left most box, and will be a 1 if there is a 1 there, 0 otherwise. A - in front represents that the boolean is negated. so -111 refers to Not a 1 in the upper left hand box

Then you have to generate the equation, it will be in CNF form -

So the first thing to check is that there is a 1-9 in every cell.
so, 111 v 112 v 113 v 114 v 115 v 116 v 117 v 118 v 119
but then you need to make sure there aren't more than one
so
-111 v -112, -111 v -113 . . . etc

Repeat for rows, columns, and boxes.

And solve.

Edit: Okay, well yes I would say that having a SAT solver for a 9x9 sudoku puzzle is a little over the top. I knew that it was for a 9x9, but I guess I didn't realy realize how much over the top it was. Of course, it doesn't help that I'm using a lot of java classes - trying to really modularize my code to make it easier to understand and write.

Using strictly ints and try all possibilities it takes java about 64 ms to solve a sudoku puzzle. Using my sat solver it takes about 400ms to solve - however, the largest time with my solver is keeping track of which variables I flipped and which ones I didn't, because I have to store and reset the variables while backtracking.

It might be kind of interesting to mod my program and then try to see some results. I've seen some sat solvers that use strictly ints ( as i described the 111 stuff above, all that is ints while i use 4 different wrapper classes to keep the method writing short). I think that if I were go get my program working in that state, and then we compared the run times you would see a lot closer of a contest.

Where I think the SAT solver would really shine would be on the larger puzzles for a generalized sudoku puzzle of size nxn. I would guess that even at 16x16 the sat solver ( if done properly with int values instead of classes ) would already start to out due the try all possibilities approach.

Once again though, I had fun with the project and truly believe it will still get me an A, so I'm not too worried about the efficiency. Hope this explain things a little better, and thanks for the thought provoking question.



yeah... with 729 variables and thousands of restrictions, it seems like it would take a very long amount of time for non-trivial puzzles. I only ask because we were each asked to make a SAT solver and puzzle generator in one of my CS classes. We even had a competition to see who had the best solver in the end. One really simple and effective heuristic is to assume that all your variables are false at the beginning, which in this case is true 8/9 of the time.

I ended up doing a 4x4 version of sudoku puzzles, but that was relatively straightforward and ran very quickly.
berated-
Profile Blog Joined February 2007
United States1134 Posts
April 29 2008 00:11 GMT
#43
On April 29 2008 07:22 azndsh wrote:
Show nested quote +
On April 28 2008 23:57 berated- wrote:
On April 28 2008 14:18 azndsh wrote:
aren't sudoku SAT solvers extremely inefficient? unless you formulate the problem way differently from what I have in mind


That's really kind of irrelevant to the project. I'm taking a boolean satisfiability class and we have to do a final project related to boolean equations. Considering I'm not a total badass, I knew I wasn't going to come up with the next great thing such as WalkSAT or Davis Putnam or GSAT, any of the SAT solving techniques that were monumental upon release. So I was left with two options, I could either find some current research and write an 8 page paper on it, or I could code up an algorithm.

Reading conference papers didn't strike me as overly fun, so I went with a coding project. I could then do something like just pass a boolean equation to an algorithm and try to solve it, which would have got the job done but is a little bland. So I sought out something that would at least be enjoyable.

As for the original question, my first response would have to be no. Using DP, a true sudoku puzzle ( one with only one answer and requiring no search techniques ) would actually require only unit propagation while solving the algorithm. Of course, you would have to define what it is inefficient compared to. Its obviously better than a try all possibilities solution. Are there other algorithms out there that might do better? I have no idea. I wasnt studying Sudoku, I was studying boolean equations, so I apologize that I can't give you a better answer.

I guess you would have to make that judgment call:

My technique ( learned from the work of others who have already done this - I'm just an undergrad, I can't be doing monumental work in my field ):

There are 729 variables - one for every possible number in every possible cell. These are represented by a 3 digit string - the row, the column, and the number.

So 111 refers to a one being in the upper left most box, and will be a 1 if there is a 1 there, 0 otherwise. A - in front represents that the boolean is negated. so -111 refers to Not a 1 in the upper left hand box

Then you have to generate the equation, it will be in CNF form -

So the first thing to check is that there is a 1-9 in every cell.
so, 111 v 112 v 113 v 114 v 115 v 116 v 117 v 118 v 119
but then you need to make sure there aren't more than one
so
-111 v -112, -111 v -113 . . . etc

Repeat for rows, columns, and boxes.

And solve.

Edit: Okay, well yes I would say that having a SAT solver for a 9x9 sudoku puzzle is a little over the top. I knew that it was for a 9x9, but I guess I didn't realy realize how much over the top it was. Of course, it doesn't help that I'm using a lot of java classes - trying to really modularize my code to make it easier to understand and write.

Using strictly ints and try all possibilities it takes java about 64 ms to solve a sudoku puzzle. Using my sat solver it takes about 400ms to solve - however, the largest time with my solver is keeping track of which variables I flipped and which ones I didn't, because I have to store and reset the variables while backtracking.

It might be kind of interesting to mod my program and then try to see some results. I've seen some sat solvers that use strictly ints ( as i described the 111 stuff above, all that is ints while i use 4 different wrapper classes to keep the method writing short). I think that if I were go get my program working in that state, and then we compared the run times you would see a lot closer of a contest.

Where I think the SAT solver would really shine would be on the larger puzzles for a generalized sudoku puzzle of size nxn. I would guess that even at 16x16 the sat solver ( if done properly with int values instead of classes ) would already start to out due the try all possibilities approach.

Once again though, I had fun with the project and truly believe it will still get me an A, so I'm not too worried about the efficiency. Hope this explain things a little better, and thanks for the thought provoking question.



yeah... with 729 variables and thousands of restrictions, it seems like it would take a very long amount of time for non-trivial puzzles. I only ask because we were each asked to make a SAT solver and puzzle generator in one of my CS classes. We even had a competition to see who had the best solver in the end. One really simple and effective heuristic is to assume that all your variables are false at the beginning, which in this case is true 8/9 of the time.

I ended up doing a 4x4 version of sudoku puzzles, but that was relatively straightforward and ran very quickly.


While it does take a long time relatively, under half a second to solve a sudoku puzzle is still pretty fast imo. As far as the competition part, that sounds awesome. They have a national sat competition every year that my prof has been to. Of course the people who enter those are the people that created most of the algorithms that we studied this year.

I talked to my professor about holding one at our school when he got to teach his boolean SAT course again, but considering our honors seminar class has 2 people in it, I doubt it would be much fun. Plus I'm graduating so I wouldn't even get to stay around to enjoy it.
minus_human
Profile Blog Joined November 2006
4784 Posts
April 29 2008 00:13 GMT
#44
sudoku=> songoku

[image loading]
Prev 1 2 3 All
Please log in or register to reply.
Live Events Refresh
OSC
00:00
OSC Elite Rising Star #15
TBD vs ArTLIVE!
Liquipedia
Replay Cast
00:00
uThermal 2v2 Circuit: May
Liquipedia
OSC
21:00
Mid Season Playoffs
ArT vs ReBellioN
HonMonO vs Ziomek
Shameless vs LunaSea
MilkiCow vs GgMaChine
Moja vs HiGhDrA
Jumy vs TBD
Demi vs NightPhoenix
Solar vs Cham
Liquipedia
[ Submit Event ]
Live Streams
Refresh
StarCraft 2
Nina 285
Livibee 134
StarCraft: Brood War
Leta 361
JulyZerg 212
ToSsGirL 52
Nal_rA 26
Counter-Strike
Stewie2K1127
Other Games
summit1g9427
C9.Mang01440
shahzam1238
ViBE211
Organizations
Dota 2
PGL Dota 2 - Secondary Stream4281
StarCraft 2
Blizzard YouTube
StarCraft: Brood War
BSLTrovo
sctven
[ Show 17 non-featured ]
StarCraft 2
• Berry_CruncH293
• Light_VIP 117
• practicex 40
• IndyKCrew
• AfreecaTV YouTube
• sooper7s
• intothetv
• Kozan
• LaughNgamezSOOP
• Migwel
StarCraft: Brood War
• RayReign 86
• STPLYoutube
• ZZZeroYoutube
• BSLYoutube
League of Legends
• Doublelift5515
• Stunt393
Other Games
• Scarra1614
Upcoming Events
WardiTV Invitational
5h 34m
HiGhDrA vs Nicoract
MaNa vs HiGhDrA
HiGhDrA vs Reynor
Nicoract vs Reynor
MaNa vs Nicoract
MaNa vs Reynor
MaxPax vs Spirit
Krystianer vs Spirit
OSC
7h 34m
BSL 2v2 ProLeague S3
13h 34m
Korean StarCraft League
21h 34m
SOOP
1d 3h
sOs vs Percival
CranKy Ducklings
1d 4h
WardiTV Invitational
1d 5h
Cheesadelphia
1d 9h
CSO Cup
1d 11h
BSL: ProLeague
1d 12h
Hawk vs UltrA
Sziky vs spx
TerrOr vs JDConan
[ Show More ]
GSL Code S
2 days
Rogue vs herO
Classic vs GuMiho
Sparkling Tuna Cup
2 days
BSL: ProLeague
2 days
Bonyth vs Dewalt
Cross vs Doodle
MadiNho vs Dragon
Replay Cast
2 days
Wardi Open
3 days
Replay Cast
3 days
Replay Cast
4 days
RSL Revival
4 days
Cure vs Percival
ByuN vs Spirit
RSL Revival
5 days
herO vs sOs
Zoun vs Clem
Replay Cast
5 days
The PondCast
6 days
RSL Revival
6 days
Serral vs SHIN
Solar vs Cham
Replay Cast
6 days
Liquipedia Results

Completed

CSL Season 17: Qualifier 2
BGE Stara Zagora 2025
Heroes 10 EU

Ongoing

JPL Season 2
BSL 2v2 Season 3
BSL Season 20
KCM Race Survival 2025 Season 2
NPSL S3
Rose Open S1
CSL 17: 2025 SUMMER
2025 GSL S2
BLAST.tv Austin Major 2025
ESL Impact League Season 7
IEM Dallas 2025
PGL Astana 2025
Asian Champions League '25
BLAST Rivals Spring 2025
MESA Nomadic Masters
CCT Season 2 Global Finals
IEM Melbourne 2025
YaLLa Compass Qatar 2025
PGL Bucharest 2025

Upcoming

Copa Latinoamericana 4
CSLPRO Last Chance 2025
CSLPRO Chat StarLAN 3
K-Championship
SEL Season 2 Championship
Esports World Cup 2025
HSC XXVII
Championship of Russia 2025
Murky Cup #2
Esports World Cup 2025
BLAST Bounty Fall 2025
BLAST Bounty Fall Qual
IEM Cologne 2025
FISSURE Playground #1
TLPD

1. ByuN
2. TY
3. Dark
4. Solar
5. Stats
6. Nerchio
7. sOs
8. soO
9. INnoVation
10. Elazer
1. Rain
2. Flash
3. EffOrt
4. Last
5. Bisu
6. Soulkey
7. Mini
8. Sharp
Sidebar Settings...

Advertising | Privacy Policy | Terms Of Use | Contact Us

Original banner artwork: Jim Warren
The contents of this webpage are copyright © 2025 TLnet. All Rights Reserved.