3/2/08
TinyML - Lexer, Parser, Interpreter, and Type Checker in Under 700 Lines of SML
I am trying to keep my own compilers/interpreter under the 10KLoc. Yeah, well, Tiny-ML proves I am doing something wrong, I guess...
2/14/08
2/5/08
Top Quality Type Error Messages
This is a very readable phd-thesis on a practical approach to typing: "Top Quality Type Error Messages" by Bastiaan Heeren, 2005. The ideas in it now form the basis for my Hi language.
2008 Turing Award Winners
Hey, I know these people ;-).
The Association for Computing Machinery has announced the 2008 Turing Award Winners. Edmund M. Clarke, Allen Emerson, and Joseph Sifakis received the award for their work on an automated method for finding design errors in computer hardware and software.
"Model Checking is a type of "formal verification" that analyzes the logic underlying a design, much as a mathematician uses a proof to determine that a theorem is correct. Far from hit or miss, Model Checking considers every possible state of a hardware or software design and determines if it is consistent with the designer's specifications. Clarke and Emerson originated the idea of Model Checking at Harvard in 1981. They developed a theoretical technique for determining whether an abstract model of a hardware or software design satisfies a formal specification, given as a formula in Temporal Logic, a notation for describing possible sequences of events. Moreover, when the system fails the specification, it could identify a counterexample to show the source of the problem. Numerous model checking systems have been implemented, such as Spin at Bell Labs."
The Association for Computing Machinery has announced the 2008 Turing Award Winners. Edmund M. Clarke, Allen Emerson, and Joseph Sifakis received the award for their work on an automated method for finding design errors in computer hardware and software.
"Model Checking is a type of "formal verification" that analyzes the logic underlying a design, much as a mathematician uses a proof to determine that a theorem is correct. Far from hit or miss, Model Checking considers every possible state of a hardware or software design and determines if it is consistent with the designer's specifications. Clarke and Emerson originated the idea of Model Checking at Harvard in 1981. They developed a theoretical technique for determining whether an abstract model of a hardware or software design satisfies a formal specification, given as a formula in Temporal Logic, a notation for describing possible sequences of events. Moreover, when the system fails the specification, it could identify a counterexample to show the source of the problem. Numerous model checking systems have been implemented, such as Spin at Bell Labs."
1/27/08
Trivially Size-Balanced Maps
I tested my interpreter for the Hi language with a translation of the trivially size-balanced map implementation originally written in OCAML.
I developed the code when I was looking for some datastructure which would:
Years ago, I looked at one implementation by Daan Leijen, but it seemed to have a lot of overhead, and not a lot of merit in a referentially transparent language. So, I decided to go another way.
A trivially size balanced map is a structure which holds key-value pairs in an ordered binary tree.
A node in the tree is either an empty leaf node or a node which holds a key value pair, a left branch and a right branch, and the number of key value pairs in that branch. A key and value pair is stored in order in the tree by recursively traversing the tree until an empty leaf node is found. On the way up, nodes are rebalanced (rotated).
In the picture above, a rotation to the left is shown. Of course, such a rotation is only done if the right-branch I.c of the tree I.a is larger than the left-branch I.b of that tree. If we try to rotate pending the size of the branches then a rotation should be performed only if the size of the resulting branch II.a is smaller than the size of the original branch I.c. The size of I.c is 1 + size(d) + size(e) and the size of II.a is 1 + size(d) + size(b). This gives a wonderfully small and fast test: 1 + size(d) + size(b) < 1 + size(d) + size(e) which simplifies to size(b) < size(e).
The resulting data-structure has roughly size and time complexities between ordered binary trees and perfectly balanced ordered binary trees. On the good side, the size is a good estimate for the depth of a small tree. So, small trees are nearly perfectly balanced which, in most scenarios, keeps almost all trees pretty close to perfectly balanced trees (I hope).
Below the Hi code. The typechecker is still under development, so some small faults may occur in the types.
Note. I never did any formal analysis and I know of some degenerate cases. Also, I never gave much thought about double rotations. But, somehow, the thing works out pretty well with a substantially low overhead in almost all practical cases.
I developed the code when I was looking for some datastructure which would:
- allow for low-cost sharing of slightly modified versions of a mapping,
- have reasonably fast insertion and look-up algorithms,
- have a fast look-up on size,
- be very low on space overhead.
Years ago, I looked at one implementation by Daan Leijen, but it seemed to have a lot of overhead, and not a lot of merit in a referentially transparent language. So, I decided to go another way.
A trivially size balanced map is a structure which holds key-value pairs in an ordered binary tree.
A node in the tree is either an empty leaf node or a node which holds a key value pair, a left branch and a right branch, and the number of key value pairs in that branch. A key and value pair is stored in order in the tree by recursively traversing the tree until an empty leaf node is found. On the way up, nodes are rebalanced (rotated).
| I. a II. c |
| / \ / \ |
| b c -> a e |
| / \ / \ |
| d e b d |
In the picture above, a rotation to the left is shown. Of course, such a rotation is only done if the right-branch I.c of the tree I.a is larger than the left-branch I.b of that tree. If we try to rotate pending the size of the branches then a rotation should be performed only if the size of the resulting branch II.a is smaller than the size of the original branch I.c. The size of I.c is 1 + size(d) + size(e) and the size of II.a is 1 + size(d) + size(b). This gives a wonderfully small and fast test: 1 + size(d) + size(b) < 1 + size(d) + size(e) which simplifies to size(b) < size(e).
The resulting data-structure has roughly size and time complexities between ordered binary trees and perfectly balanced ordered binary trees. On the good side, the size is a good estimate for the depth of a small tree. So, small trees are nearly perfectly balanced which, in most scenarios, keeps almost all trees pretty close to perfectly balanced trees (I hope).
Below the Hi code. The typechecker is still under development, so some small faults may occur in the types.
Note. I never did any formal analysis and I know of some degenerate cases. Also, I never gave much thought about double rotations. But, somehow, the thing works out pretty well with a substantially low overhead in almost all practical cases.
import "util_list.hi"
/********************************************************************/
namespace opt (
type opt = \a => [ just a | nothing ]
)
/********************************************************************/
namespace map (
using system
type map = \a \b =>
[ empty
| node int a b (map a b) (map a b) ]
def empty_test: map a b -> bool =
[ empty -> true
| _ -> false ]
def choose: map a b -> a =
[ node n k v l r -> k ]
def maximum: map a b -> (a, b) =
[ node n k v l empty -> (k,v)
| node n k v l r -> maximum r ]
def minimum: map a b -> (a, b) =
[ node n k v empty r -> (k,v)
| node n k v l r -> minimum l ]
def size: map a b -> int =
[ empty -> 0
| node n k v l r -> n ]
def look: ::ord a => map a b -> a -> opt.opt b =
[ empty, a -> opt.nothing
| node s k v l r, a ->
if a < k then look l a
else if a > k then look r a
else opt.just v ]
def has: ::ord a => map a b -> a -> bool =
[ m, k ->
[ opt.nothing -> false
| opt.just _ -> true ] (look m k) ]
def member: ::ord a => map a b -> a -> b -> bool =
[ m, k, v ->
[ opt.nothing -> false
| opt.just w -> w == v ] (look m k) ]
def nth: ::ord a => map a b -> a -> b =
[ m, k -> [ opt.just v -> v ] (look m k) ]
def nth_total: ::ord a => a -> map a b -> b -> a =
[ m, k, d -> [ opt.just v -> v | _ -> d ] (look m k) ]
def new_node: a -> b -> map a b -> map a b -> map a b =
[ k, v, l, r -> node (1 + size l + size r) k v l r ]
def balance0: a -> b -> map a b -> map a b -> map a b =
[ k, v, l, r ->
[ node sx kx vx lx rx ->
if size l < size rx
then new_node kx vx (new_node k v l lx) rx
else new_node k v l r
| _ -> new_node k v l r ] r ]
def balance1: a -> b -> map a b -> map a b -> map a b =
[ k, v, l, r ->
[ node sx kx vx lx rx ->
if size r < size lx
then new_node kx vx lx (new_node k v rx r)
else new_node k v l r
| _ -> new_node k v l r ] l ]
def balance: a -> b -> map a b -> map a b -> map a b =
[ k, v, l, r ->
let sl = size l in
let sr = size r in
if sl < sr then balance0 k v l r
else if sl > sr then balance1 k v l r
else new_node k v l r ]
def glue: map a b -> map a b -> map a b =
[ l, r ->
[ empty, _ -> r
| _, empty -> l
| node sx kx vx lx rx, node sy ky vy ly ry ->
if (sx < sy) then balance ky vy (glue l ly) ry
else balance kx vx lx (glue rx r) ] l r ]
def change: ::ord a => a -> (opt.opt b -> opt.opt b) -> map a b -> map a b =
[ a, f, empty ->
[ opt.nothing -> empty
| opt.just v -> balance a v empty empty ]
(f opt.nothing)
| a, f, node s k v l r ->
if a < k then balance k v (change a f l) r
else if a > k then balance k v l (change a f r)
else [ opt.nothing -> glue l r
| opt.just z -> balance k z l r ] (f (opt.just v)) ]
def insert: ::ord a => a -> b -> map a b -> map a b =
[ k, v -> change k [x -> opt.just v] ]
def delete: ::ord a => a -> map a b -> map a b =
[ k -> change k [ v -> opt.nothing ] ]
def foldr: (a -> b -> c -> c) -> c -> map a b -> c =
[ f, z, empty -> z
| f, z, node s k v l r ->
foldr f (f k v (foldr f z r)) l ]
def foldl: (a -> b -> c -> c) -> c -> map a b -> c =
[ f, z, empty -> z
| f, z, node s k v l r ->
foldl f (f k v (foldl f z l)) r ]
def foldm: (a -> b -> c -> c -> c) -> c -> map a b -> c =
[ f, z, empty -> z
| f, z, node s k v l r ->
f k v (foldm f z l) (foldm f z r) ]
def fold: (a -> b -> c -> c) -> c -> map a b -> c =
foldr
def to_up_list: map a b -> list (a, b) =
[ m -> foldr [ k, v, l -> list.cons (k,v) l ] list.nil m ]
def to_down_list: map a b -> list (a, b) =
[ m -> foldl [ k, v, l -> list.cons (k,v) l ] list.nil m ]
def to_list: map a b -> list (a, b) =
to_up_list
def from_list: list (a, b) -> map a b =
[ list.nil -> empty
| list.cons (k,v) xx -> insert k v (from_list xx) ]
def domain: map a b -> a list =
[ m -> list.map [ (a,b) -> a ] (to_list m) ]
def range: map a b -> b list =
[ m -> list.map [ (a,b) -> b ] (to_list m) ]
def filter: ::ord a => (a -> b -> bool) -> map a b -> map a b =
[ p -> fold
[ k, v, m -> if p k v then insert k v m else m ]
empty ]
def partition: ::ord a =>
(a -> b -> c) -> map a b -> (c, map a b) map =
[ p, m ->
let f, p, k, v, m =
let i = p k v in
insert i (insert k v (nth_total (empty) m i)) m
in fold (f p) empty m ]
def divide: ::ord a =>
(a -> b -> bool) -> map a b -> (map a b, map a b) =
[ p, m -> let d = partition p m in
(nth_total empty d false,
nth_total empty d true) ]
def union: ::ord a => map a b -> map a b -> map a b =
[ m0, m1 ->
fold [ k, v, m -> insert k v m] m0 m1 ]
def subtract: ::ord a => map a b -> map a b -> map a b =
[ m0, m1 ->
filter [ k, v -> not (member m1 k v) ] m0 ]
def intersection: ::ord a => map a b -> map a b -> map a b =
[ m0, m1 -> filter (member m0) m1 ]
def inverse: ::ord a ::ord b => map a b -> map b a =
[ m -> let f, k, v, m0 = insert v k m0
in fold f empty m ]
def apply: ::ord c => (a -> b) -> map c a -> map c b =
[ f, m -> fold
[ k, v, m -> insert k (f v) m ] empty m ]
def compose: ::ord a ::ord c => map a b -> map c a -> map c b =
[ m0, m1 -> apply (nth m0) m1 ]
def decompose: ::ord a => map a b -> (map int b, map a int) =
[ m ->
foldr
[ k, v, (m0, m1) ->
(insert (size m0) v m0, insert k (size m0) m1) ]
(empty, empty) m
]
)
using system
def make_map: int -> map int int =
[ 0 -> map.empty
| n -> map.insert n (n+1) (make_map (n-1)) ]
def main: map int int = map.nth (map.apply [x -> x * 2 ] (make_map 10)) 5
1/18/08
1/17/08
Yet Another Sudoku Solver
I am ill at home, so I had some time to write on my own Sudoku solver.
The solver is a variant on the classical Davis, Putman, Logemann and Loveland (DPLL) binary procedure for solving boolean formulas in conjunctive normal form.
Given a Sudoku puzzle the solver constructs a propositional formula which is a conjunct of clauses. Clauses are either simple inequalities between number valued variables stating the constraints on the puzzle, or a set of disjunctive equalities stating the possible values of a variable as stated in the puzzle to solve.
The solver deterministically chooses a shortest clause of equalities and tries the formula for each of these values until a solution is found.
Given as input the puzzle
it constructs the set of following inequalities (v11 is the value of the upper-left cell and v99 is the value of the lower-right cell)
and equalities
By chasing the shortest possible clause of equalities, which normally defaults to unit propagation, variables are eliminated out of the term until a solution is found.
The program is a bit of a hack, some of the datastructures should have been chosen more directly which would have avoided a number of conversions and implicit assumptions.
The solver is a variant on the classical Davis, Putman, Logemann and Loveland (DPLL) binary procedure for solving boolean formulas in conjunctive normal form.
Given a Sudoku puzzle the solver constructs a propositional formula which is a conjunct of clauses. Clauses are either simple inequalities between number valued variables stating the constraints on the puzzle, or a set of disjunctive equalities stating the possible values of a variable as stated in the puzzle to solve.
The solver deterministically chooses a shortest clause of equalities and tries the formula for each of these values until a solution is found.
Given as input the puzzle
8 . 3 . . . . 4 .
. . 6 . . . . 9 .
. . . . 5 . . 3 .
2 7 . . 4 6 . . .
. . 5 . 9 . . . .
. . . . . 1 . . .
. . . . 8 . 3 . 5
. 9 7 4 . . . . .
. 8 . 3 2 . 9 . .
it constructs the set of following inequalities (v11 is the value of the upper-left cell and v99 is the value of the lower-right cell)
v91 != v92 * v91 != v93 * v91 != v94 * v91 != v95 * v91 != v96 * v91 != v97 * v91 != v98 *
v91 != v99 * v92 != v93 * v92 != v94 * v92 != v95 * v92 != v96 * v92 != v97 * v92 != v98 *
v92 != v99 * v93 != v94 * v93 != v95 * v93 != v96 * v93 != v97 * v93 != v98 * v93 != v99 *
v94 != v95 * v94 != v96 * v94 != v97 * v94 != v98 * v94 != v99 * v95 != v96 * v95 != v97 *
v95 != v98 * v95 != v99 * v96 != v97 * v96 != v98 * v96 != v99 * v97 != v98 * v97 != v99 *
v98 != v99 * v81 != v82 * v81 != v83 * v81 != v84 * v81 != v85 * v81 != v86 * v81 != v87 *
v81 != v88 * v81 != v89 * v82 != v83 * v82 != v84 * v82 != v85 * v82 != v86 * v82 != v87 *
v82 != v88 * v82 != v89 * v83 != v84 * v83 != v85 * v83 != v86 * v83 != v87 * v83 != v88 *
v83 != v89 * v84 != v85 * v84 != v86 * v84 != v87 * v84 != v88 * v84 != v89 * v85 != v86 *
v85 != v87 * v85 != v88 * v85 != v89 * v86 != v87 * v86 != v88 * v86 != v89 * v87 != v88 *
v87 != v89 * v88 != v89 * v71 != v72 * v71 != v73 * v71 != v74 * v71 != v75 * v71 != v76 *
v71 != v77 * v71 != v78 * v71 != v79 * v72 != v73 * v72 != v74 * v72 != v75 * v72 != v76 *
v72 != v77 * v72 != v78 * v72 != v79 * v73 != v74 * v73 != v75 * v73 != v76 * v73 != v77 *
v73 != v78 * v73 != v79 * v74 != v75 * v74 != v76 * v74 != v77 * v74 != v78 * v74 != v79 *
v75 != v76 * v75 != v77 * v75 != v78 * v75 != v79 * v76 != v77 * v76 != v78 * v76 != v79 *
v77 != v78 * v77 != v79 * v78 != v79 * v61 != v62 * v61 != v63 * v61 != v64 * v61 != v65 *
v61 != v66 * v61 != v67 * v61 != v68 * v61 != v69 * v62 != v63 * v62 != v64 * v62 != v65 *
v62 != v66 * v62 != v67 * v62 != v68 * v62 != v69 * v63 != v64 * v63 != v65 * v63 != v66 *
v63 != v67 * v63 != v68 * v63 != v69 * v64 != v65 * v64 != v66 * v64 != v67 * v64 != v68 *
v64 != v69 * v65 != v66 * v65 != v67 * v65 != v68 * v65 != v69 * v66 != v67 * v66 != v68 *
v66 != v69 * v67 != v68 * v67 != v69 * v68 != v69 * v51 != v52 * v51 != v53 * v51 != v54 *
v51 != v55 * v51 != v56 * v51 != v57 * v51 != v58 * v51 != v59 * v52 != v53 * v52 != v54 *
v52 != v55 * v52 != v56 * v52 != v57 * v52 != v58 * v52 != v59 * v53 != v54 * v53 != v55 *
v53 != v56 * v53 != v57 * v53 != v58 * v53 != v59 * v54 != v55 * v54 != v56 * v54 != v57 *
v54 != v58 * v54 != v59 * v55 != v56 * v55 != v57 * v55 != v58 * v55 != v59 * v56 != v57 *
v56 != v58 * v56 != v59 * v57 != v58 * v57 != v59 * v58 != v59 * v41 != v42 * v41 != v43 *
v41 != v44 * v41 != v45 * v41 != v46 * v41 != v47 * v41 != v48 * v41 != v49 * v42 != v43 *
v42 != v44 * v42 != v45 * v42 != v46 * v42 != v47 * v42 != v48 * v42 != v49 * v43 != v44 *
v43 != v45 * v43 != v46 * v43 != v47 * v43 != v48 * v43 != v49 * v44 != v45 * v44 != v46 *
v44 != v47 * v44 != v48 * v44 != v49 * v45 != v46 * v45 != v47 * v45 != v48 * v45 != v49 *
v46 != v47 * v46 != v48 * v46 != v49 * v47 != v48 * v47 != v49 * v48 != v49 * v31 != v32 *
v31 != v33 * v31 != v34 * v31 != v35 * v31 != v36 * v31 != v37 * v31 != v38 * v31 != v39 *
v32 != v33 * v32 != v34 * v32 != v35 * v32 != v36 * v32 != v37 * v32 != v38 * v32 != v39 *
v33 != v34 * v33 != v35 * v33 != v36 * v33 != v37 * v33 != v38 * v33 != v39 * v34 != v35 *
v34 != v36 * v34 != v37 * v34 != v38 * v34 != v39 * v35 != v36 * v35 != v37 * v35 != v38 *
v35 != v39 * v36 != v37 * v36 != v38 * v36 != v39 * v37 != v38 * v37 != v39 * v38 != v39 *
v21 != v22 * v21 != v23 * v21 != v24 * v21 != v25 * v21 != v26 * v21 != v27 * v21 != v28 *
v21 != v29 * v22 != v23 * v22 != v24 * v22 != v25 * v22 != v26 * v22 != v27 * v22 != v28 *
v22 != v29 * v23 != v24 * v23 != v25 * v23 != v26 * v23 != v27 * v23 != v28 * v23 != v29 *
v24 != v25 * v24 != v26 * v24 != v27 * v24 != v28 * v24 != v29 * v25 != v26 * v25 != v27 *
v25 != v28 * v25 != v29 * v26 != v27 * v26 != v28 * v26 != v29 * v27 != v28 * v27 != v29 *
v28 != v29 * v11 != v12 * v11 != v13 * v11 != v14 * v11 != v15 * v11 != v16 * v11 != v17 *
v11 != v18 * v11 != v19 * v12 != v13 * v12 != v14 * v12 != v15 * v12 != v16 * v12 != v17 *
v12 != v18 * v12 != v19 * v13 != v14 * v13 != v15 * v13 != v16 * v13 != v17 * v13 != v18 *
v13 != v19 * v14 != v15 * v14 != v16 * v14 != v17 * v14 != v18 * v14 != v19 * v15 != v16 *
v15 != v17 * v15 != v18 * v15 != v19 * v16 != v17 * v16 != v18 * v16 != v19 * v17 != v18 *
v17 != v19 * v18 != v19 * v19 != v29 * v19 != v39 * v19 != v49 * v19 != v59 * v19 != v69 *
v19 != v79 * v19 != v89 * v19 != v99 * v29 != v39 * v29 != v49 * v29 != v59 * v29 != v69 *
v29 != v79 * v29 != v89 * v29 != v99 * v39 != v49 * v39 != v59 * v39 != v69 * v39 != v79 *
v39 != v89 * v39 != v99 * v49 != v59 * v49 != v69 * v49 != v79 * v49 != v89 * v49 != v99 *
v59 != v69 * v59 != v79 * v59 != v89 * v59 != v99 * v69 != v79 * v69 != v89 * v69 != v99 *
v79 != v89 * v79 != v99 * v89 != v99 * v18 != v28 * v18 != v38 * v18 != v48 * v18 != v58 *
v18 != v68 * v18 != v78 * v18 != v88 * v18 != v98 * v28 != v38 * v28 != v48 * v28 != v58 *
v28 != v68 * v28 != v78 * v28 != v88 * v28 != v98 * v38 != v48 * v38 != v58 * v38 != v68 *
v38 != v78 * v38 != v88 * v38 != v98 * v48 != v58 * v48 != v68 * v48 != v78 * v48 != v88 *
v48 != v98 * v58 != v68 * v58 != v78 * v58 != v88 * v58 != v98 * v68 != v78 * v68 != v88 *
v68 != v98 * v78 != v88 * v78 != v98 * v88 != v98 * v17 != v27 * v17 != v37 * v17 != v47 *
v17 != v57 * v17 != v67 * v17 != v77 * v17 != v87 * v17 != v97 * v27 != v37 * v27 != v47 *
v27 != v57 * v27 != v67 * v27 != v77 * v27 != v87 * v27 != v97 * v37 != v47 * v37 != v57 *
v37 != v67 * v37 != v77 * v37 != v87 * v37 != v97 * v47 != v57 * v47 != v67 * v47 != v77 *
v47 != v87 * v47 != v97 * v57 != v67 * v57 != v77 * v57 != v87 * v57 != v97 * v67 != v77 *
v67 != v87 * v67 != v97 * v77 != v87 * v77 != v97 * v87 != v97 * v16 != v26 * v16 != v36 *
v16 != v46 * v16 != v56 * v16 != v66 * v16 != v76 * v16 != v86 * v16 != v96 * v26 != v36 *
v26 != v46 * v26 != v56 * v26 != v66 * v26 != v76 * v26 != v86 * v26 != v96 * v36 != v46 *
v36 != v56 * v36 != v66 * v36 != v76 * v36 != v86 * v36 != v96 * v46 != v56 * v46 != v66 *
v46 != v76 * v46 != v86 * v46 != v96 * v56 != v66 * v56 != v76 * v56 != v86 * v56 != v96 *
v66 != v76 * v66 != v86 * v66 != v96 * v76 != v86 * v76 != v96 * v86 != v96 * v15 != v25 *
v15 != v35 * v15 != v45 * v15 != v55 * v15 != v65 * v15 != v75 * v15 != v85 * v15 != v95 *
v25 != v35 * v25 != v45 * v25 != v55 * v25 != v65 * v25 != v75 * v25 != v85 * v25 != v95 *
v35 != v45 * v35 != v55 * v35 != v65 * v35 != v75 * v35 != v85 * v35 != v95 * v45 != v55 *
v45 != v65 * v45 != v75 * v45 != v85 * v45 != v95 * v55 != v65 * v55 != v75 * v55 != v85 *
v55 != v95 * v65 != v75 * v65 != v85 * v65 != v95 * v75 != v85 * v75 != v95 * v85 != v95 *
v14 != v24 * v14 != v34 * v14 != v44 * v14 != v54 * v14 != v64 * v14 != v74 * v14 != v84 *
v14 != v94 * v24 != v34 * v24 != v44 * v24 != v54 * v24 != v64 * v24 != v74 * v24 != v84 *
v24 != v94 * v34 != v44 * v34 != v54 * v34 != v64 * v34 != v74 * v34 != v84 * v34 != v94 *
v44 != v54 * v44 != v64 * v44 != v74 * v44 != v84 * v44 != v94 * v54 != v64 * v54 != v74 *
v54 != v84 * v54 != v94 * v64 != v74 * v64 != v84 * v64 != v94 * v74 != v84 * v74 != v94 *
v84 != v94 * v13 != v23 * v13 != v33 * v13 != v43 * v13 != v53 * v13 != v63 * v13 != v73 *
v13 != v83 * v13 != v93 * v23 != v33 * v23 != v43 * v23 != v53 * v23 != v63 * v23 != v73 *
v23 != v83 * v23 != v93 * v33 != v43 * v33 != v53 * v33 != v63 * v33 != v73 * v33 != v83 *
v33 != v93 * v43 != v53 * v43 != v63 * v43 != v73 * v43 != v83 * v43 != v93 * v53 != v63 *
v53 != v73 * v53 != v83 * v53 != v93 * v63 != v73 * v63 != v83 * v63 != v93 * v73 != v83 *
v73 != v93 * v83 != v93 * v12 != v22 * v12 != v32 * v12 != v42 * v12 != v52 * v12 != v62 *
v12 != v72 * v12 != v82 * v12 != v92 * v22 != v32 * v22 != v42 * v22 != v52 * v22 != v62 *
v22 != v72 * v22 != v82 * v22 != v92 * v32 != v42 * v32 != v52 * v32 != v62 * v32 != v72 *
v32 != v82 * v32 != v92 * v42 != v52 * v42 != v62 * v42 != v72 * v42 != v82 * v42 != v92 *
v52 != v62 * v52 != v72 * v52 != v82 * v52 != v92 * v62 != v72 * v62 != v82 * v62 != v92 *
v72 != v82 * v72 != v92 * v82 != v92 * v11 != v21 * v11 != v31 * v11 != v41 * v11 != v51 *
v11 != v61 * v11 != v71 * v11 != v81 * v11 != v91 * v21 != v31 * v21 != v41 * v21 != v51 *
v21 != v61 * v21 != v71 * v21 != v81 * v21 != v91 * v31 != v41 * v31 != v51 * v31 != v61 *
v31 != v71 * v31 != v81 * v31 != v91 * v41 != v51 * v41 != v61 * v41 != v71 * v41 != v81 *
v41 != v91 * v51 != v61 * v51 != v71 * v51 != v81 * v51 != v91 * v61 != v71 * v61 != v81 *
v61 != v91 * v71 != v81 * v71 != v91 * v81 != v91 * v77 != v78 * v77 != v79 * v77 != v87 *
v77 != v88 * v77 != v89 * v77 != v97 * v77 != v98 * v77 != v99 * v78 != v79 * v78 != v87 *
v78 != v88 * v78 != v89 * v78 != v97 * v78 != v98 * v78 != v99 * v79 != v87 * v79 != v88 *
v79 != v89 * v79 != v97 * v79 != v98 * v79 != v99 * v87 != v88 * v87 != v89 * v87 != v97 *
v87 != v98 * v87 != v99 * v88 != v89 * v88 != v97 * v88 != v98 * v88 != v99 * v89 != v97 *
v89 != v98 * v89 != v99 * v97 != v98 * v97 != v99 * v98 != v99 * v74 != v75 * v74 != v76 *
v74 != v84 * v74 != v85 * v74 != v86 * v74 != v94 * v74 != v95 * v74 != v96 * v75 != v76 *
v75 != v84 * v75 != v85 * v75 != v86 * v75 != v94 * v75 != v95 * v75 != v96 * v76 != v84 *
v76 != v85 * v76 != v86 * v76 != v94 * v76 != v95 * v76 != v96 * v84 != v85 * v84 != v86 *
v84 != v94 * v84 != v95 * v84 != v96 * v85 != v86 * v85 != v94 * v85 != v95 * v85 != v96 *
v86 != v94 * v86 != v95 * v86 != v96 * v94 != v95 * v94 != v96 * v95 != v96 * v71 != v72 *
v71 != v73 * v71 != v81 * v71 != v82 * v71 != v83 * v71 != v91 * v71 != v92 * v71 != v93 *
v72 != v73 * v72 != v81 * v72 != v82 * v72 != v83 * v72 != v91 * v72 != v92 * v72 != v93 *
v73 != v81 * v73 != v82 * v73 != v83 * v73 != v91 * v73 != v92 * v73 != v93 * v81 != v82 *
v81 != v83 * v81 != v91 * v81 != v92 * v81 != v93 * v82 != v83 * v82 != v91 * v82 != v92 *
v82 != v93 * v83 != v91 * v83 != v92 * v83 != v93 * v91 != v92 * v91 != v93 * v92 != v93 *
v47 != v48 * v47 != v49 * v47 != v57 * v47 != v58 * v47 != v59 * v47 != v67 * v47 != v68 *
v47 != v69 * v48 != v49 * v48 != v57 * v48 != v58 * v48 != v59 * v48 != v67 * v48 != v68 *
v48 != v69 * v49 != v57 * v49 != v58 * v49 != v59 * v49 != v67 * v49 != v68 * v49 != v69 *
v57 != v58 * v57 != v59 * v57 != v67 * v57 != v68 * v57 != v69 * v58 != v59 * v58 != v67 *
v58 != v68 * v58 != v69 * v59 != v67 * v59 != v68 * v59 != v69 * v67 != v68 * v67 != v69 *
v68 != v69 * v44 != v45 * v44 != v46 * v44 != v54 * v44 != v55 * v44 != v56 * v44 != v64 *
v44 != v65 * v44 != v66 * v45 != v46 * v45 != v54 * v45 != v55 * v45 != v56 * v45 != v64 *
v45 != v65 * v45 != v66 * v46 != v54 * v46 != v55 * v46 != v56 * v46 != v64 * v46 != v65 *
v46 != v66 * v54 != v55 * v54 != v56 * v54 != v64 * v54 != v65 * v54 != v66 * v55 != v56 *
v55 != v64 * v55 != v65 * v55 != v66 * v56 != v64 * v56 != v65 * v56 != v66 * v64 != v65 *
v64 != v66 * v65 != v66 * v41 != v42 * v41 != v43 * v41 != v51 * v41 != v52 * v41 != v53 *
v41 != v61 * v41 != v62 * v41 != v63 * v42 != v43 * v42 != v51 * v42 != v52 * v42 != v53 *
v42 != v61 * v42 != v62 * v42 != v63 * v43 != v51 * v43 != v52 * v43 != v53 * v43 != v61 *
v43 != v62 * v43 != v63 * v51 != v52 * v51 != v53 * v51 != v61 * v51 != v62 * v51 != v63 *
v52 != v53 * v52 != v61 * v52 != v62 * v52 != v63 * v53 != v61 * v53 != v62 * v53 != v63 *
v61 != v62 * v61 != v63 * v62 != v63 * v17 != v18 * v17 != v19 * v17 != v27 * v17 != v28 *
v17 != v29 * v17 != v37 * v17 != v38 * v17 != v39 * v18 != v19 * v18 != v27 * v18 != v28 *
v18 != v29 * v18 != v37 * v18 != v38 * v18 != v39 * v19 != v27 * v19 != v28 * v19 != v29 *
v19 != v37 * v19 != v38 * v19 != v39 * v27 != v28 * v27 != v29 * v27 != v37 * v27 != v38 *
v27 != v39 * v28 != v29 * v28 != v37 * v28 != v38 * v28 != v39 * v29 != v37 * v29 != v38 *
v29 != v39 * v37 != v38 * v37 != v39 * v38 != v39 * v14 != v15 * v14 != v16 * v14 != v24 *
v14 != v25 * v14 != v26 * v14 != v34 * v14 != v35 * v14 != v36 * v15 != v16 * v15 != v24 *
v15 != v25 * v15 != v26 * v15 != v34 * v15 != v35 * v15 != v36 * v16 != v24 * v16 != v25 *
v16 != v26 * v16 != v34 * v16 != v35 * v16 != v36 * v24 != v25 * v24 != v26 * v24 != v34 *
v24 != v35 * v24 != v36 * v25 != v26 * v25 != v34 * v25 != v35 * v25 != v36 * v26 != v34 *
v26 != v35 * v26 != v36 * v34 != v35 * v34 != v36 * v35 != v36 * v11 != v12 * v11 != v13 *
v11 != v21 * v11 != v22 * v11 != v23 * v11 != v31 * v11 != v32 * v11 != v33 * v12 != v13 *
v12 != v21 * v12 != v22 * v12 != v23 * v12 != v31 * v12 != v32 * v12 != v33 * v13 != v21 *
v13 != v22 * v13 != v23 * v13 != v31 * v13 != v32 * v13 != v33 * v21 != v22 * v21 != v23 *
v21 != v31 * v21 != v32 * v21 != v33 * v22 != v23 * v22 != v31 * v22 != v32 * v22 != v33 *
v23 != v31 * v23 != v32 * v23 != v33 * v31 != v32 * v31 != v33 * v32 != v33 *
and equalities
v11 = 8 *
v12 = 1 + v12 = 2 + v12 = 3 + v12 = 4 + v12 = 5 + v12 = 6 + v12 = 7 + v12 = 8 + v12 = 9 *
v13 = 3 *
v14 = 1 + v14 = 2 + v14 = 3 + v14 = 4 + v14 = 5 + v14 = 6 + v14 = 7 + v14 = 8 + v14 = 9 *
v15 = 1 + v15 = 2 + v15 = 3 + v15 = 4 + v15 = 5 + v15 = 6 + v15 = 7 + v15 = 8 + v15 = 9 *
v16 = 1 + v16 = 2 + v16 = 3 + v16 = 4 + v16 = 5 + v16 = 6 + v16 = 7 + v16 = 8 + v16 = 9 *
v17 = 1 + v17 = 2 + v17 = 3 + v17 = 4 + v17 = 5 + v17 = 6 + v17 = 7 + v17 = 8 + v17 = 9 *
v18 = 4 *
v19 = 1 + v19 = 2 + v19 = 3 + v19 = 4 + v19 = 5 + v19 = 6 + v19 = 7 + v19 = 8 + v19 = 9 *
v21 = 1 + v21 = 2 + v21 = 3 + v21 = 4 + v21 = 5 + v21 = 6 + v21 = 7 + v21 = 8 + v21 = 9 *
v22 = 1 + v22 = 2 + v22 = 3 + v22 = 4 + v22 = 5 + v22 = 6 + v22 = 7 + v22 = 8 + v22 = 9 *
v23 = 6 *
v24 = 1 + v24 = 2 + v24 = 3 + v24 = 4 + v24 = 5 + v24 = 6 + v24 = 7 + v24 = 8 + v24 = 9 *
v25 = 1 + v25 = 2 + v25 = 3 + v25 = 4 + v25 = 5 + v25 = 6 + v25 = 7 + v25 = 8 + v25 = 9 *
v26 = 1 + v26 = 2 + v26 = 3 + v26 = 4 + v26 = 5 + v26 = 6 + v26 = 7 + v26 = 8 + v26 = 9 *
v27 = 1 + v27 = 2 + v27 = 3 + v27 = 4 + v27 = 5 + v27 = 6 + v27 = 7 + v27 = 8 + v27 = 9 *
v28 = 9 *
v29 = 1 + v29 = 2 + v29 = 3 + v29 = 4 + v29 = 5 + v29 = 6 + v29 = 7 + v29 = 8 + v29 = 9 *
v31 = 1 + v31 = 2 + v31 = 3 + v31 = 4 + v31 = 5 + v31 = 6 + v31 = 7 + v31 = 8 + v31 = 9 *
v32 = 1 + v32 = 2 + v32 = 3 + v32 = 4 + v32 = 5 + v32 = 6 + v32 = 7 + v32 = 8 + v32 = 9 *
v33 = 1 + v33 = 2 + v33 = 3 + v33 = 4 + v33 = 5 + v33 = 6 + v33 = 7 + v33 = 8 + v33 = 9 *
v34 = 1 + v34 = 2 + v34 = 3 + v34 = 4 + v34 = 5 + v34 = 6 + v34 = 7 + v34 = 8 + v34 = 9 *
v35 = 5 *
v36 = 1 + v36 = 2 + v36 = 3 + v36 = 4 + v36 = 5 + v36 = 6 + v36 = 7 + v36 = 8 + v36 = 9 *
v37 = 1 + v37 = 2 + v37 = 3 + v37 = 4 + v37 = 5 + v37 = 6 + v37 = 7 + v37 = 8 + v37 = 9 *
v38 = 3 *
v39 = 1 + v39 = 2 + v39 = 3 + v39 = 4 + v39 = 5 + v39 = 6 + v39 = 7 + v39 = 8 + v39 = 9 *
v41 = 2 *
v42 = 7 *
v43 = 1 + v43 = 2 + v43 = 3 + v43 = 4 + v43 = 5 + v43 = 6 + v43 = 7 + v43 = 8 + v43 = 9 *
v44 = 1 + v44 = 2 + v44 = 3 + v44 = 4 + v44 = 5 + v44 = 6 + v44 = 7 + v44 = 8 + v44 = 9 *
v45 = 4 *
v46 = 6 *
v47 = 1 + v47 = 2 + v47 = 3 + v47 = 4 + v47 = 5 + v47 = 6 + v47 = 7 + v47 = 8 + v47 = 9 *
v48 = 1 + v48 = 2 + v48 = 3 + v48 = 4 + v48 = 5 + v48 = 6 + v48 = 7 + v48 = 8 + v48 = 9 *
v49 = 1 + v49 = 2 + v49 = 3 + v49 = 4 + v49 = 5 + v49 = 6 + v49 = 7 + v49 = 8 + v49 = 9 *
v51 = 1 + v51 = 2 + v51 = 3 + v51 = 4 + v51 = 5 + v51 = 6 + v51 = 7 + v51 = 8 + v51 = 9 *
v52 = 1 + v52 = 2 + v52 = 3 + v52 = 4 + v52 = 5 + v52 = 6 + v52 = 7 + v52 = 8 + v52 = 9 *
v53 = 5 *
v54 = 1 + v54 = 2 + v54 = 3 + v54 = 4 + v54 = 5 + v54 = 6 + v54 = 7 + v54 = 8 + v54 = 9 *
v55 = 9 *
v56 = 1 + v56 = 2 + v56 = 3 + v56 = 4 + v56 = 5 + v56 = 6 + v56 = 7 + v56 = 8 + v56 = 9 *
v57 = 1 + v57 = 2 + v57 = 3 + v57 = 4 + v57 = 5 + v57 = 6 + v57 = 7 + v57 = 8 + v57 = 9 *
v58 = 1 + v58 = 2 + v58 = 3 + v58 = 4 + v58 = 5 + v58 = 6 + v58 = 7 + v58 = 8 + v58 = 9 *
v59 = 1 + v59 = 2 + v59 = 3 + v59 = 4 + v59 = 5 + v59 = 6 + v59 = 7 + v59 = 8 + v59 = 9 *
v61 = 1 + v61 = 2 + v61 = 3 + v61 = 4 + v61 = 5 + v61 = 6 + v61 = 7 + v61 = 8 + v61 = 9 *
v62 = 1 + v62 = 2 + v62 = 3 + v62 = 4 + v62 = 5 + v62 = 6 + v62 = 7 + v62 = 8 + v62 = 9 *
v63 = 1 + v63 = 2 + v63 = 3 + v63 = 4 + v63 = 5 + v63 = 6 + v63 = 7 + v63 = 8 + v63 = 9 *
v64 = 1 + v64 = 2 + v64 = 3 + v64 = 4 + v64 = 5 + v64 = 6 + v64 = 7 + v64 = 8 + v64 = 9 *
v65 = 1 + v65 = 2 + v65 = 3 + v65 = 4 + v65 = 5 + v65 = 6 + v65 = 7 + v65 = 8 + v65 = 9 *
v66 = 1 *
v67 = 1 + v67 = 2 + v67 = 3 + v67 = 4 + v67 = 5 + v67 = 6 + v67 = 7 + v67 = 8 + v67 = 9 *
v68 = 1 + v68 = 2 + v68 = 3 + v68 = 4 + v68 = 5 + v68 = 6 + v68 = 7 + v68 = 8 + v68 = 9 *
v69 = 1 + v69 = 2 + v69 = 3 + v69 = 4 + v69 = 5 + v69 = 6 + v69 = 7 + v69 = 8 + v69 = 9 *
v71 = 1 + v71 = 2 + v71 = 3 + v71 = 4 + v71 = 5 + v71 = 6 + v71 = 7 + v71 = 8 + v71 = 9 *
v72 = 1 + v72 = 2 + v72 = 3 + v72 = 4 + v72 = 5 + v72 = 6 + v72 = 7 + v72 = 8 + v72 = 9 *
v73 = 1 + v73 = 2 + v73 = 3 + v73 = 4 + v73 = 5 + v73 = 6 + v73 = 7 + v73 = 8 + v73 = 9 *
v74 = 1 + v74 = 2 + v74 = 3 + v74 = 4 + v74 = 5 + v74 = 6 + v74 = 7 + v74 = 8 + v74 = 9 *
v75 = 8 *
v76 = 1 + v76 = 2 + v76 = 3 + v76 = 4 + v76 = 5 + v76 = 6 + v76 = 7 + v76 = 8 + v76 = 9 *
v77 = 3 *
v78 = 1 + v78 = 2 + v78 = 3 + v78 = 4 + v78 = 5 + v78 = 6 + v78 = 7 + v78 = 8 + v78 = 9 *
v79 = 5 *
v81 = 1 + v81 = 2 + v81 = 3 + v81 = 4 + v81 = 5 + v81 = 6 + v81 = 7 + v81 = 8 + v81 = 9 *
v82 = 9 *
v83 = 7 *
v84 = 4 *
v85 = 1 + v85 = 2 + v85 = 3 + v85 = 4 + v85 = 5 + v85 = 6 + v85 = 7 + v85 = 8 + v85 = 9 *
v86 = 1 + v86 = 2 + v86 = 3 + v86 = 4 + v86 = 5 + v86 = 6 + v86 = 7 + v86 = 8 + v86 = 9 *
v87 = 1 + v87 = 2 + v87 = 3 + v87 = 4 + v87 = 5 + v87 = 6 + v87 = 7 + v87 = 8 + v87 = 9 *
v88 = 1 + v88 = 2 + v88 = 3 + v88 = 4 + v88 = 5 + v88 = 6 + v88 = 7 + v88 = 8 + v88 = 9 *
v89 = 1 + v89 = 2 + v89 = 3 + v89 = 4 + v89 = 5 + v89 = 6 + v89 = 7 + v89 = 8 + v89 = 9 *
v91 = 1 + v91 = 2 + v91 = 3 + v91 = 4 + v91 = 5 + v91 = 6 + v91 = 7 + v91 = 8 + v91 = 9 *
v92 = 8 *
v93 = 1 + v93 = 2 + v93 = 3 + v93 = 4 + v93 = 5 + v93 = 6 + v93 = 7 + v93 = 8 + v93 = 9 *
v94 = 3 *
v95 = 2 *
v96 = 1 + v96 = 2 + v96 = 3 + v96 = 4 + v96 = 5 + v96 = 6 + v96 = 7 + v96 = 8 + v96 = 9 *
v97 = 9 *
v98 = 1 + v98 = 2 + v98 = 3 + v98 = 4 + v98 = 5 + v98 = 6 + v98 = 7 + v98 = 8 + v98 = 9 *
v99 = 1 + v99 = 2 + v99 = 3 + v99 = 4 + v99 = 5 + v99 = 6 + v99 = 7 + v99 = 8 + v99 = 9 *
By chasing the shortest possible clause of equalities, which normally defaults to unit propagation, variables are eliminated out of the term until a solution is found.
8 5 3 9 7 2 6 4 1
7 4 6 8 1 3 5 9 2
9 1 2 6 5 4 8 3 7
2 7 9 5 4 6 1 8 3
1 3 5 7 9 8 4 2 6
4 6 8 2 3 1 7 5 9
6 2 4 1 8 9 3 7 5
3 9 7 4 6 5 2 1 8
5 8 1 3 2 7 9 6 4
The program is a bit of a hack, some of the datastructures should have been chosen more directly which would have avoided a number of conversions and implicit assumptions.
(********************************************************************)
open Util_opt
open Util_seq
open Util_map
open Util_set
open Util_text
open Util_search
open Util_doc
open System_io
(********************************************************************)
let rec puzzle_read: text -> int list =
function tt -> match tt with
| [] -> []
| '.'::tt -> 0::puzzle_read tt
| '1'::tt -> 1::puzzle_read tt
| '2'::tt -> 2::puzzle_read tt
| '3'::tt -> 3::puzzle_read tt
| '4'::tt -> 4::puzzle_read tt
| '5'::tt -> 5::puzzle_read tt
| '6'::tt -> 6::puzzle_read tt
| '7'::tt -> 7::puzzle_read tt
| '8'::tt -> 8::puzzle_read tt
| '9'::tt -> 9::puzzle_read tt
| _ ::tt -> puzzle_read tt
let rec print_puzzle: int list -> unit =
let rec pp = function x -> function tt ->
let x = if x == 9 then 1 else x+1 in
(
if x == 1 then print_newline () else ();
match tt with
| [] -> print_newline ();
| 0::nn -> print_string ". "; pp x nn
| n::nn -> print_int n; print_string " "; pp x nn
)
in
function tt -> pp 0 tt
(********************************************************************)
type prop =
| Var of int * int | Const of int
| Eq of prop * prop | Neq of prop * prop
| Sum of prop * prop
let rec print_prop: prop -> unit =
function p -> match p with
| Const(i) -> print_int i
| Var(i,j) ->
( print_string "v";
print_int i;
print_int j )
| Eq(a, b) ->
( print_prop a;
print_string " = ";
print_prop b )
| Neq(a, b) ->
( print_prop a;
print_string " != ";
print_prop b )
| Sum(a, b) ->
( print_prop a;
print_string " + ";
print_prop b )
let rec print_props: prop list -> unit =
function pp -> match pp with
| [] -> print_newline ()
| p::pp -> print_prop p; print_string " * \n"; print_props pp
let v: int -> int -> prop =
function i -> function j -> Var(i,j)
let c: int -> prop =
function i -> Const(i)
let eq: prop -> prop -> prop =
function a -> function b -> Eq(a,b)
let neq: prop -> prop -> prop =
function a -> function b -> Neq(a,b)
let sum: prop -> prop -> prop =
function a -> function b -> Sum(a,b)
let ( ++ ) = sum
let rec prop_sum_to_list: prop -> prop list =
function p -> match p with
| Sum(a,b) -> seq_append (prop_sum_to_list a) (prop_sum_to_list b)
| _ -> [p]
let prop_sum_from_list: prop list -> prop opt =
function pp ->
if seq_empty_test pp then opt_nothing
else opt_just (seq_wrapl ( ++ ) pp)
(********************************************************************)
let xxx: (int*int) list =
[
(1,2); (1,3); (1,4); (1,5); (1,6); (1,7); (1,8); (1,9);
(2,3); (2,4); (2,5); (2,6); (2,7); (2,8); (2,9);
(3,4); (3,5); (3,6); (3,7); (3,8); (3,9);
(4,5); (4,6); (4,7); (4,8); (4,9);
(5,6); (5,7); (5,8); (5,9);
(6,7); (6,8); (6,9);
(7,8); (7,9);
(8,9)
]
let prop_row: int -> prop list = function n ->
(seq_map (function (i,j) -> neq (v n i) (v n j)) xxx)
let prop_column: int -> prop list = function n ->
(seq_map (function (i,j) -> neq (v i n) (v j n)) xxx)
let prop_rows: prop list =
seq_flatten
(seq_map (function n -> prop_row n) [1;2;3;4;5;6;7;8;9])
let prop_columns: prop list =
seq_flatten
(seq_map (function n -> prop_column n) [1;2;3;4;5;6;7;8;9])
(********************************************************************)
let yyy: ((int * int) * (int*int)) list =
[
( (1,1), (1,2) ); ( (1,1), (1,3) );
( (1,1), (2,1) ); ( (1,1), (2,2) ); ( (1,1), (2,3) );
( (1,1), (3,1) ); ( (1,1), (3,2) ); ( (1,1), (3,3) );
( (1,2), (1,3) );
( (1,2), (2,1) ); ( (1,2), (2,2) ); ( (1,2), (2,3) );
( (1,2), (3,1) ); ( (1,2), (3,2) ); ( (1,2), (3,3) );
( (1,3), (2,1) ); ( (1,3), (2,2) ); ( (1,3), (2,3) );
( (1,3), (3,1) ); ( (1,3), (3,2) ); ( (1,3), (3,3) );
( (2,1), (2,2) ); ( (2,1), (2,3) );
( (2,1), (3,1) ); ( (2,1), (3,2) ); ( (2,1), (3,3) );
( (2,2), (2,3) );
( (2,2), (3,1) ); ( (2,2), (3,2) ); ( (2,2), (3,3) );
( (2,3), (3,1) ); ( (2,3), (3,2) ); ( (2,3), (3,3) );
( (3,1), (3,2) ); ( (3,1), (3,3) );
( (3,2), (3,3) );
]
(********************************************************************)
let prop_block: (int*int) -> prop list =
function (x, y) ->
seq_map (function ((i,j),(p,q)) ->
neq (v (i+x) (j+y)) (v (p+x) (q+y))) yyy
let prop_blocks: prop list =
seq_flatten (seq_map (function p -> prop_block p)
[ (0,0);(0,3);(0,6);(3,0);(3,3);(3,6);(6,0);(6,3);(6,6) ])
(********************************************************************)
let prop_field: prop list =
seq_append (seq_append prop_rows prop_columns) prop_blocks
(********************************************************************)
let prop_unknown: int -> int -> prop =
function i -> function j ->
let f = v i j in
eq f (c 1) ++ eq f (c 2) ++ eq f (c 3) ++ eq f (c 4) ++
eq f (c 5) ++ eq f (c 6) ++ eq f (c 7) ++ eq f (c 8) ++
eq f (c 9)
let prop_known: int -> int -> int -> prop =
function i -> function j -> function n ->
eq (v i j) (c n)
let prop_from_sudoku: int list -> prop list =
let rec pfs: int -> int -> int list -> prop list =
function i -> function j -> function cc -> match cc with
| [] -> []
| c::cc ->
let p =
if c == 0 then prop_unknown i j
else prop_known i j c
in
let (i,j) = if j = 9 then (i+1, 1) else (i, j+1) in
p::pfs i j cc
in function cc -> pfs 1 1 cc
(********************************************************************)
let prop_unit_test: prop -> bool =
function p -> match p with
| Eq (Var(x0,y0), Const(c1)) -> true
| _ -> false
let rec prop_find_unit: prop list -> (prop * prop list) opt =
function pp -> match pp with
| p::pp ->
if prop_unit_test p then opt_just (p,pp)
else
let u = prop_find_unit pp in
if opt_nothing_test u then u else
let q,pp = opt_value u in
opt_just (q, p::pp)
| _ -> opt_nothing
let prop_unit_decompose: prop -> (int * int * int) =
function p -> match p with
| Eq (Var(x0,y0), Const(c1)) -> (x0,y0,c1)
| _ -> (0,0,0)
(********************************************************************)
let prop_clause_test: prop -> bool =
function p -> match p with
| Sum (_, _) -> true
| Eq (_, _) -> true
| _ -> false
let prop_clause_length: prop -> int =
function p -> seq_length (prop_sum_to_list p)
let rec prop_find_best_clause: prop list -> (prop opt * prop list) =
function pp -> match pp with
| p::pp ->
let q,pp = prop_find_best_clause pp in
if prop_clause_test p then
if opt_nothing_test q then
(opt_just p, pp)
else
let q = opt_value q in
if prop_clause_length p < prop_clause_length q
then (opt_just p, q::pp)
else (opt_just q, p::pp)
else (q,p::pp)
| _ -> (opt_nothing, [])
(********************************************************************)
let prop_ineq_test: int -> int -> int -> prop -> bool =
function i -> function j -> function c -> function p ->
match p with
| Neq(Var(x0,y0), Var(x1,y1)) ->
( x0 == i && y0 == j ) || (x1 == i && y1 == j)
| _ -> false
let prop_ineq_convert: int -> int -> int -> prop -> prop =
function i -> function j -> function c -> function p ->
match p with
| Neq(Var(x0,y0), Var(x1,y1)) ->
if x0 == i && y0 == j then
Neq(Var(x1,y1), Const(c))
else if x1 == i && y1 == j then
Neq(Var(x0,y0), Const(c))
else p
| _ -> p
let prop_split_ineq:
int -> int -> int -> prop list -> (prop list * prop list) =
function i -> function j -> function c -> function pp ->
let ll,rr = seq_divide (prop_ineq_test i j c) pp in
(seq_map (prop_ineq_convert i j c) ll, rr)
(********************************************************************)
let prop_ineq_decompose: prop -> (int * int * int) =
function p -> match p with
| Neq(Var(x0,y0), Const(c1)) -> (x0,y0,c1)
| _ -> (0,0,0)
let prop_match_eq: int -> int -> int -> prop -> bool =
function i -> function j -> function c -> function p ->
match p with
| Eq (Var(x0,y0), Const(c0)) -> x0 == i && y0 == j && c == c0
| _ -> false
let prop_propagate_ineq_clause: int -> int -> int -> prop -> prop opt =
function i -> function j -> function c -> function pp ->
let cc = prop_sum_to_list pp in
let cc = seq_filter (fun p -> not (prop_match_eq i j c p)) cc in
prop_sum_from_list cc
let prop_propagate_ineq: int -> int -> int -> prop list -> prop list opt =
function i -> function j -> function c -> function pp ->
let pp = seq_map (prop_propagate_ineq_clause i j c) pp in
let ll, pp = seq_divide opt_nothing_test pp in
if seq_empty_test ll then opt_just (seq_map opt_value pp)
else opt_nothing
let rec prop_propagate_ineqs:
prop list -> prop list -> prop list opt =
function nn -> function pp ->
match nn with
| [] -> opt_just pp
| n::nn ->
let i,j,c = prop_ineq_decompose n in
let pp = prop_propagate_ineq i j c pp in
if opt_nothing_test pp then opt_nothing
else prop_propagate_ineqs nn (opt_value pp)
(********************************************************************)
let rec prop_chase_units:
prop list -> (prop list * prop list) -> (prop list * prop list) opt =
function cc -> function (uu,pp) ->
match cc with
| [] -> opt_nothing
| u::cc ->
let i, j, c = prop_unit_decompose u in
let qq, rr = prop_split_ineq i j c pp in
let rr = prop_propagate_ineqs qq rr in
if opt_nothing_test rr then prop_chase_units cc (uu,pp)
else
let s = prop_solve (u::uu, opt_value rr) in
if opt_nothing_test s then prop_chase_units cc (uu,pp)
else s
and prop_solve:
(prop list * prop list) -> (prop list * prop list) opt =
function uu,pp ->
let cc,pp = prop_find_best_clause pp in
if opt_nothing_test cc then opt_just (uu,pp)
else
let cc = prop_sum_to_list (opt_value cc) in
prop_chase_units cc (uu, pp)
(********************************************************************)
let rec prop_value: int -> int -> prop list -> int =
let pv = function i -> function j -> function p ->
match p with
| Eq(Var(x,y), Const(c)) ->
if (x == i) && (y == j) then c else 0
| _ -> 0
in
function i -> function j -> function pp -> match pp with
| [] -> 0
| p::pp -> if pv i j p == 0 then prop_value i j pp else pv i j p
let rec prop_to_int_list: int -> int -> prop list -> int list =
function i -> function j -> function pp ->
if j > 9 then prop_to_int_list (i+1) 1 pp
else if i > 9 then []
else (prop_value i j pp::prop_to_int_list i (j+1) pp)
let prop_to_sudoku: prop list -> int list =
function pp -> prop_to_int_list 1 1 pp
(********************************************************************)
let _ =
let fn = seq_project sys_args 1 in
let pz = puzzle_read (file_read fn) in
let _ = print_string "solving:\n\n" in
let _ = print_puzzle pz in
let pp = seq_append (prop_field) (prop_from_sudoku pz) in
let _ = print_string "trying to solve term:\n\n" in
let _ = print_props pp in
let s = prop_solve ([], pp) in
if opt_nothing_test s then
print_string "no_solution\n"
else
let uu, pp = opt_value s in
let l = prop_to_sudoku uu in
let _ = print_string "found solution:\n\n" in
print_puzzle l
(********************************************************************)
Subscribe to:
Posts (Atom)
