• Log InLog In
  • Register
Liquid`
Team Liquid Liquipedia
EDT 18:12
CEST 00:12
KST 07:12
  • 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
BGE Stara Zagora 2025: Info & Preview27Code S RO12 Preview: GuMiho, Bunny, SHIN, ByuN3The Memories We Share - Facing the Final(?) GSL47Code S RO12 Preview: Cure, Zoun, Solar, Creator4[ASL19] Finals Preview: Daunting Task30
Community News
Weekly Cups (June 2-8): herO doubles down1[BSL20] ProLeague: Bracket Stage & Dates9GSL Ro4 and Finals moved to Sunday June 15th13Weekly Cups (May 27-June 1): ByuN goes back-to-back0EWC 2025 Regional Qualifier Results26
StarCraft 2
General
The SCII GOAT: A statistical Evaluation Best Crypto Asset Recovery Service Providers CN community: Firefly accused of suspicious activities Firefly do had match fixing How does the number of casters affect your enjoyment of esports?
Tourneys
$3,500 WardiTV European League 2025 Bellum Gens Elite: Stara Zagora 2025 Sparkling Tuna Cup - Weekly Open Tournament SOOPer7s Showmatches 2025 Master Swan Open (Global Bronze-Master 2)
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/ Will foreigners ever be able to challenge Koreans? Mihu vs Korea Players Statistics BW General Discussion [BSL20] ProLeague: Bracket Stage & Dates
Tourneys
[ASL19] Grand Finals NA Team League 6/8/2025 [Megathread] Daily Proleagues [BSL20] ProLeague Bracket Stage - Day 2
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 What do you want from future RTS games? Armies of Exigo - YesYes? Nintendo Switch Thread Path of Exile
Dota 2
Official 'what is Dota anymore' discussion
League of Legends
LiquidLegends to reintegrate into TL.net
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
US Politics Mega-thread Things Aren’t Peaceful in Palestine Russo-Ukrainian War Thread Vape Nation Thread European Politico-economics QA Mega-thread
Fan Clubs
Maru Fan Club Serral Fan Club
Media & Entertainment
Korean Music Discussion [Manga] One Piece
Sports
2024 - 2025 Football Thread Formula 1 Discussion NHL Playoffs 2024
World Cup 2022
Tech Support
Computer Build, Upgrade & Buying Resource Thread
TL Community
The Automated Ban List
Blogs
Cognitive styles x game perf…
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
Poker
Nebuchad
Customize Sidebar...

Website Feedback

Closed Threads



Active: 22203 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
Next event in 1h 48m
[ Submit Event ]
Live Streams
Refresh
StarCraft 2
UpATreeSC 153
-ZergGirl 53
StarCraft: Brood War
Horang2 581
firebathero 128
yabsab 12
Dota 2
NeuroSwarm70
febbydoto17
Counter-Strike
fl0m8851
olofmeister3281
rGuardiaN145
Super Smash Bros
Mew2King54
Heroes of the Storm
Liquid`Hasu595
Other Games
summit1g9920
Grubby3229
Pyrionflax193
mouzStarbuck181
ZombieGrub106
Maynarde24
Organizations
Dota 2
PGL Dota 2 - Main Stream2510
Other Games
BasetradeTV90
StarCraft 2
Blizzard YouTube
StarCraft: Brood War
BSLTrovo
sctven
[ Show 24 non-featured ]
StarCraft 2
• Hupsaiya 62
• Adnapsc2 26
• musti20045 25
• -Miszu- 11
• Dystopia_ 5
• OhrlRock 2
• IndyKCrew
• sooper7s
• AfreecaTV YouTube
• Migwel
• intothetv
• LaughNgamezSOOP
• Kozan
StarCraft: Brood War
• Azhi_Dahaki4
• STPLYoutube
• ZZZeroYoutube
• BSLYoutube
Dota 2
• masondota22435
• Ler134
League of Legends
• TFBlade1349
• Shiphtur545
• Doublelift465
Other Games
• Scarra1279
• imaqtpie1142
Upcoming Events
Replay Cast
1h 48m
Replay Cast
11h 48m
WardiTV Invitational
12h 48m
WardiTV Invitational
12h 48m
PiGosaur Monday
1d 1h
GSL Code S
1d 11h
Rogue vs GuMiho
Maru vs Solar
Online Event
2 days
Replay Cast
2 days
GSL Code S
2 days
herO vs Zoun
Classic vs Bunny
The PondCast
2 days
[ Show More ]
Replay Cast
3 days
WardiTV Invitational
3 days
OSC
3 days
Korean StarCraft League
4 days
CranKy Ducklings
4 days
WardiTV Invitational
4 days
Cheesadelphia
4 days
GSL Code S
5 days
Sparkling Tuna Cup
5 days
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
ECL Season 49: Europe
BLAST Rivals Spring 2025
MESA Nomadic Masters
CCT Season 2 Global Finals
IEM Melbourne 2025
YaLLa Compass Qatar 2025
PGL Bucharest 2025
BLAST Open Spring 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.