vodka-goo has quit ["Connection reset by by pear"]
_JusSx_ has quit ["leaving"]
Smerdyakov has joined #ocaml
joshcryer has joined #ocaml
Skal has quit [Remote closed the connection]
malc_ has quit ["leaving"]
smimou has quit ["bli"]
DeathWolf has quit []
Smerdyakov has quit ["Leaving"]
pango_ has joined #ocaml
pango has quit [Read error: 110 (Connection timed out)]
danly has joined #ocaml
Herrchen_ has joined #ocaml
Herrchen has quit [Read error: 110 (Connection timed out)]
Revision17 has quit [Remote closed the connection]
joshcryer has quit []
Herrchen_ is now known as Herrchen
Skal has joined #ocaml
descender has quit ["XML is like violence, if it doesn't solve the problem, just use more."]
Snark has joined #ocaml
zvrba has joined #ocaml
Skal has quit ["Client exiting"]
<zvrba>
hm
<zvrba>
a question about separate compilation
<zvrba>
ocamlc -c Unbound type constructor BitVector.t
<zvrba>
i.e. that is the error
<zvrba>
i strace() ocamlc and I see that it doesn't even try to open the bitvector.cmi file
<zvrba>
and the source file I'm compiling is using the BitVector
<zvrba>
how to make it work?
<zvrba>
so, this is the thing:
<zvrba>
bitvector.ml contains BitVectorSig and BitVector:BitVectorSig modules
<zvrba>
cellconstraint.ml uses the BitVector.t type...
<zvrba>
(it's abstract..)
<zvrba>
when I try to compile cellconstraint.ml I get Unbound type constructor BitVector.t
<Snark>
shouldn't it be something like BitVector.BitVectorSig.t ?
<zvrba>
nope, doesn't work
<zvrba>
it doesn't even try to open the bitVector.cmi file
rillig has joined #ocaml
<Snark>
zvrba: do you have the right -I directory flag ?
<zvrba>
everything is in the current directory, i've checked that
<zvrba>
and I've tried adding -I .
<zvrba>
no go :(
<zvrba>
i mean, how does one use A.mli within B.ml without linking
<zvrba>
so that the compiler just finds the appropriate definitions...
<zvrba>
anyway, food time.. later..
Schmurtz has joined #ocaml
smimou has joined #ocaml
malc_ has joined #ocaml
vodka-goo has joined #ocaml
malc_ has quit ["leaving"]
Smerdyakov has joined #ocaml
Submarine has joined #ocaml
<zvrba>
hm... how to best do the following thing
<zvrba>
i have a set of cells, and each cell has associated a constraint with it
<zvrba>
er.. several constraints
<zvrba>
cells contain integers
<zvrba>
and i have to check whether all constraints are satisfied for some integer
<Smerdyakov>
You're asking this at a point when you haven't written any code yet?
<zvrba>
constraints are expressed purely by their behaviour.. i.e. they have a methods "test n" which returns true/false for the number n
<zvrba>
yes :)
<Smerdyakov>
Why do you want to use methods instead of functions?
<zvrba>
i have, but not much and it's discardable :)
<zvrba>
ok
<zvrba>
concrete case: i'm making a sudoku solver
<zvrba>
er.. killer-sudoku
<zvrba>
the constraints have their mutable state
<mellum>
Sudoku is trivial. Any lame algorithm will solve it quickly.
<zvrba>
yeah, it is
<zvrba>
but i want to make a nicely-structured program :D
<zvrba>
actually, i've written solvers in C++
<Smerdyakov>
Constraints with mutable state? A constraint changes over time?
<zvrba>
yes
<Smerdyakov>
How does it change?
<zvrba>
consider the constraint "all numbers are unique in the row"
<zvrba>
since the cell is a member of exactly one row
<zvrba>
so, if I put number 7 in some cell, no other cell in the same row can have the value 7
<zvrba>
therefore, the constraint has changed
<Smerdyakov>
That sounds like a constraint on the whole board to me. Why not make it a function of the board?
<zvrba>
the killer-sudoku variant adds subregions on the board.. the sum in each subregion must equal something prespecified
<zvrba>
so i wanted to generalize to a set of constraints over the cell
<zvrba>
Smerdyakov: why not - because of quick tests. what I've done in C++ is to associate a bit vector with each row, column and 3x3 subgrid
<zvrba>
each time i try a number in the cell, I set appropriate bits
<zvrba>
when I remove it, I clear the bits
<Smerdyakov>
That's an implementation detail. It sounds like the ADT you want to implement should involve boolean functions of boards.
<zvrba>
ok..
<zvrba>
yes, I see the point
<zvrba>
:)
<zvrba>
hm..
<zvrba>
each cell affects only a subset of the board
<zvrba>
esp. in the "killer-sudoku" variant
<Smerdyakov>
And..?
<zvrba>
ok, so you're saying that the ADT should expose only the "can_put" function taking the board, position and the number, returning just true/false ?
<zvrba>
(delete only :))
<Smerdyakov>
I don't know enough about the details of the problem to suggest anything about "can_put."
<zvrba>
aha, ok :)
<zvrba>
wow, i'm amazed that you haven't heard of sudoku (no offense :))
<zvrba>
you're given a 9x9 grid
<Smerdyakov>
I have, but I've never learned the rules, and I don't expect that I'd care for the game.
<Smerdyakov>
Numbers are one of the more boring parts of math.
<zvrba>
the goal is to place digits 1-9 such that each row, column and 3x3 subgrid has all digits 1-9 (=> this implies uniqueness). some digits are initially given on the grid.
<Smerdyakov>
Yeah, sounds like absolutely not my kind of thing.
<zvrba>
:)
<Submarine>
if that interests you I've recently implemented a Sudoku solver
<zvrba>
anyway, i was trying to decouple constraints from the board
<zvrba>
Submarine: i have it too, in C++. and for killer-sudoku, and kakuro.
<Submarine>
interestingly, the n²×n² variant is NP-complete
<zvrba>
so thx, I don't want the ready-made solution. coding is the most fun part :)
<zvrba>
Submarine: which variant? i see some strange letters...
<Submarine>
n^2 x n^2
<zvrba>
ah
<Smerdyakov>
It might be fun to implement a Sudoku solver as a logic program, though.
<zvrba>
of course.. even the 9x9 variant is np complete :)
<Submarine>
er...
<Submarine>
no
<Submarine>
9x9 can be solved in unit time
<zvrba>
yeah, i've thought of using CLP in GNU prolog
<Smerdyakov>
I remember that SAT is just as hard if you know the solution is unique.
<Smerdyakov>
(Classic proof in complexity theory :-)
<zvrba>
btw, i was thinking also about making a program to calculate the puzzle "hardness" since this is a very debatable topic
<zvrba>
so i'd define hardness as the minimum lookahead level at each stage of the puzzle that derives a cell+digit
<zvrba>
this turned out to last forever in C++.. maybe i've messed something up in my implementation..
<mellum>
Smerdyakov: really? how do you prove it?
<mellum>
Smerdyakov: AFAIK, it's open whether Unique SAT is NP-complete.
Revision17 has joined #ocaml
<Smerdyakov>
mellum, it was probably for some probabilistic computation model.
<mellum>
Smerdyakov: yes, looking it up I find Unique SAT in P => RP=NP, which is probably what you mean
descender has joined #ocaml
Smerdyakov has quit ["Leaving"]
<Submarine>
arf
<Submarine>
this reminds me when I asked a question on complexity from a prof
<Submarine>
he said "oh for sure it's NP-complete"
<Submarine>
then I thought about the matter during lunch
<Submarine>
and proved it was equivalent to graph isomorphism
<Submarine>
which meant that either he was wrong, either I was a genius
<Submarine>
needless to say, he was wrong
<zvrba>
hm.. but graph isomorphism IS np complete
<zvrba>
i don't get the point
<zvrba>
isn't it?
<zvrba>
it's regarded as a hard problem..
<Submarine>
no
<Submarine>
sub-graph isomorphism is NPC
<Submarine>
graph iso afaik is an open problem
<mellum>
Thinking about it, it's not really clear what it means to say "solving sudokus is NP-complete". We know there is always exactly one solution, so what is the decision question asked?
<zvrba>
hm, maybe "NP-hard" would be a better term?
<Submarine>
I think it's to test whether there's a solution or not, perhaps knowing there <= 1 solution.
<mellum>
Submarine: but that's not really what you do when you solve the puzzles printed in newspapers.
<mellum>
zvrba: NP is defined only for decision problems, so it doesn't really change anything
<Submarine>
mellum, but the puzzles in the papers are 9x9 or at most 16x16
<Submarine>
and are solved in a fraction of a second by a simple algorithm
<zvrba>
mellum: er.. no as my teacher has explained it.. "NP-complete" is decision, "NP-hard" is actually finding the solution.. according to him
<mellum>
zvrba: That is not even wrong ;)
<zvrba>
oh well, i have lecture notes somewhere, but I'm too lazy to look up
<zvrba>
in the end, it makes no difference :)
zvrba has quit ["busy..."]
<Submarine>
no no
<Submarine>
NP-hard means that you're >= all of NP for the polynomial reduction preorder
<Submarine>
NP-complete means NP-hard AND NP
<Herrchen>
true
<Herrchen>
but there is the definition of NP-hard optimization problems
<Herrchen>
which is a trivial definition
<Herrchen>
Optimizationproblem P is NP-hard if the corresponding descision problem is NP-hard
<Herrchen>
hmm Sudokus are limited to 9x9 squares, which is finite input, so it should be solveable in constant time and thus no NP-hard optimization problem :p
<Herrchen>
hm or 16x16 squares
_JusSx_ has joined #ocaml
<flux__>
someone should write a sudoku solver that instead of giving the solution, gives a hint on how to advance
<flux__>
and gives you the reasons too
<flux__>
preferably in the simplest form possible
<simon>
flux__, the sudoku solvers I've seen are recursive until the point where all values are known. one iteration of the function should give you half of what you want.
ramkrsna is now known as rK|Spark
<flux__>
simon, well yes, but usually they discard the information how the conclusion of one step was reached?
<flux__>
and that information might be of useless form of 'because this, this, this, this, this and this wasn't possible it must be this'
<flux__>
so atleast the solver must be a constraint based one
<simon>
I haven't seen any intelligent sudoku solvers, only ones that tried every combination from one end to the other. humans solve sudokus slightly different as long as they can get away with it.
<simon>
for example, a human looks for the best entry point, a computer sudoku solver just starts with the first cell and the first number and tries from there.
<flux__>
well, some simplest form of prioritizing could be built into computer programs too, for example trying to solve first the number for which there are the most solved cells
<simon>
flux__, what you want, I suppose, is a program that can tell the most obvious thing to do next, for a human.
<flux__>
well, I don't necessarily mean the 'most obvious', but something that can be explained with the minimum number of reasoning
<flux__>
obviously such a solver would be of use only when you're stuck
<simon>
flux__, right
<flux__>
maybe you could even give the solver the other information you've gathered about potential numbers in cells
Bigb[a]ng is now known as Bigbang
<simon>
flux__, I suppose you've solved a fair amount of sudokus by hand before gaining the interest in making ocaml work them out.
<flux__>
I have, yes
<simon>
I've only solved a few, and I don't think they're very hard until a point where I believe I can simply not solve any more by deduction without testing something that could possibly turn out to be false, in which case I've tested one of, say, two to four possibilities.
<simon>
when I sat down with my first sudoku, I started by writing in small what numbers could possibly go in each cell, starting from a strategic point, then I continued to do that and it would all work out. then I tried the ones in the "hard" section, which then have less known numbers. I thought they were hard because I at one point sat with a number of empty cells and too many possibilities. I then brute-forced it, but thought that sucked.
<simon>
there's another genre of sudoku which uses mathematical symbols rather than known numbers to begin with. I believe they're extremely hard to solve.
<flux__>
well, I've played very few sudokus which need brute forcing
<flux__>
and even then I cannot be sure ;)
<simon>
flux__, maybe the ones I thought were hard simply require you to think more ahead.
<simon>
flux__, and if you can't think far enough ahead, you have to start experimenting by actually writing down numbers that aren't necessarily true.
<flux__>
that's what I almost always do except with the simplest ones
<flux__>
because once I've solved a number I can refer to the notes and quickly, without much thinking, solve a few more
<flux__>
also I have found myself considering the same situations many times without notes
<flux__>
but no, that's not actually experimenting
<flux__>
I'm just listing candidates
<simon>
flux__, right. a good notational system lets you think less.
<simon>
flux__, my friends thought my method was silly and said I'd probably get over it as soon as I get used to solving sudoku.
<flux__>
sometimes there are situations when the search tree would be very narrow
<simon>
flux__, I always do that... list candidates. I write possible numbers in the upper corner and cross them out whenever they become impossible.
<flux__>
in those cases I will try brute force, because it will speed up the process a lot
<flux__>
for example if you only have two or three different options for one cell and from there there are no choices to be made
<simon>
flux__, yeah, often you find yourself in a situation where you only have to test three or four levels before you bump into something that's not possible, in which case you can backtrack and retry with less possibilities.
<flux__>
(and where all except one leads to contradiction)
<simon>
flux__, but... have you tried any sudoku where the difficulty gives you other obstacles than just trying those two-three? and are there any better approaches in case you're only down to, say, four or five?
<flux__>
I've solved a few fives
<flux__>
fours more than that
<flux__>
that might follow the sudoku difficulty distribution of the local news paper ;)
<simon>
because there were no other choices? I find that tedious... you might as well just solve equations as a hobby then :)
<flux__>
btw, I think that the sudokus with non-numbers are soft of artificially hardened ones
<flux__>
because it is much easier to enumerate all the numbers than a set of symbols
<flux__>
s/numbers/digits/ ;)
<simon>
flux__, when you say sudokus with non-numbers, do you mean ones that uses other symbols in the cells, or ones that use mathematical operators between cells?
<flux__>
symbols other than digits
<flux__>
for example colors
<flux__>
well, I suppose characters would beok
<flux__>
but still I think digits are easier ;)
<flux__>
I haven't tried those mathematical operators-versions
<flux__>
but I do have one killer sudoku waiting on my desk, has been that way for a month ;)
<flux__>
(it has no numbers, but instead in addition to the normal constraints, it has marked areas and the sum of the area)
<simon>
I think the only interesting thing with sudoku is if there's better ways to solve them. I'm still using my initial method which I thought up instantaniously.
<flux__>
well, have you noticed that if you can, for a region (row, column, box), pick a closed set of possible numbers, you can exclude them from elsewhere in the region?
<flux__>
maybe these things are difficult to explain ;)
<flux__>
but let's say if you have decided that you have decided there must be (1, 1, 1 or 2) and (1, 2, 1 or 2), you can deduct that there cannot be 1 or 2 elsewhere in the (1, i), even though you don't know exactly how those 1 and 2 are placed?
<flux__>
oh, repetition
<flux__>
s/you have decided //2
<flux__>
similarly you can know that the box cannot have 1 or 2 elsewhere
<Herrchen>
I currently use a mechanism where I propagate information. E.g. I know that from the start in one cell is a 2, then all cells in the same row, square and column can't be that number
<Herrchen>
but in fact that is not enough
<Herrchen>
you may need further steps
<Herrchen>
thought of checking if there have to be a number N in row X in the columns Y_1,Y_2,Y_3 and if Y_1,Y_2,Y_3 belong to the same square you can deduce, that they aren't in the other cells of the same square
<Herrchen>
though many sudokus you can solve with those easy steps
<simon>
well, what I find depressing about sudoku is that either they're so easy you just solve them, or they're so hard you have to brute-force. finding any that match your own brain's capacity is mostly random.
<flux__>
you see, just for this reason there should be a better hinting software, you could possibly see that it wouldn't always require brute force ;)
<simon>
right.
<simon>
maybe I'm just being pessimistic due to sudoku's finity.
<flux__>
hmm.. infinite sudoku..
<simon>
flux__, well, at least one with a few more options for the practicioner.
Raziel has quit [Read error: 104 (Connection reset by peer)]
bzzbzz has joined #ocaml
Raziel has joined #ocaml
<flux__>
simon, if you have 'sgt-puzzles' and some means of offering images over web, I could give you hints on one sudoku puzzle I just played through ;)
<flux__>
(it took me 70 minutes (including one failure), but no brute forcing)
<flux__>
anyway, the game id is: 3x3:a6c9_7d3b1_5a2_5_7f8e2e5_8_7_3_9e4e1f8_3_2a6_9b4d7_6c1a
Bigbang is now known as Bigb[a]ng
Revision17 has quit [Read error: 104 (Connection reset by peer)]
Sylvain has joined #ocaml
Sylvain has quit ["Vision[0.8.5-0418]: i've been blurred!"]
Revision17 has joined #ocaml
pattern has left #ocaml []
pattern has joined #ocaml
rillig has quit ["exit(EXIT_SUCCESS)"]
Smerdyakov has joined #ocaml
Snark has quit [Read error: 110 (Connection timed out)]
Snark has joined #ocaml
shirogane has joined #ocaml
shirogane has quit [Remote closed the connection]
Snark has quit ["Leaving"]
shirogane has joined #ocaml
malc_ has joined #ocaml
kryptt has joined #ocaml
Smerdyakov has quit ["Leaving"]
<vincenz>
??
<flux__>
next time jeremy comes here, someone (maybe me ;-)) could tell him assert_equal has an optional argument msg
<simon>
flux__, /msg memoserv help send
malc_ has quit ["leaving"]
<Submarine>
for those who were discussing sudoku
<Submarine>
I wrote my assignment for the students