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
(********************************************************************)
