8e3c8c65 by Ulrich Schoepp

Loesungen fuer Aufgaben 2-2 und 2-4

1 parent 40fc52ea
module Main where
import Data.Map ((!))
import Formula
import Tseitin
sudoku :: Formula (Int, Int, Int)
sudoku = BigAnd [ at_least, one_number_each_cell, no_number_twice_in_row
, no_number_twice_in_col, no_number_twice_in_square, givens ]
where
at_least =
BigAnd [ Var (row, col, k) `Imp` Var (row, col, k+1)
| row <- [0..8],
col <- [0..8],
k <- [1..8] ]
one_number_each_cell =
BigAnd [ Var (row, col, 9)
| row <- [0..8],
col <- [0..8] ]
no_number_twice_in_row =
BigAnd [ BigOr [(Var (row, col1, i)) `Xor` ((Var (row, col2, i))) | i <- [1..8]]
| row <- [0..8],
col1 <- [0..8],
col2 <- [0..8],
col1 < col2 ]
no_number_twice_in_col =
BigAnd [ BigOr [(Var (row1, col, i)) `Xor` ((Var (row2, col, i))) | i <- [1..8]]
| row1 <- [0..8],
row2 <- [0..8],
col <- [0..8],
row1 < row2 ]
no_number_twice_in_square =
BigAnd [ BigOr [(Var (row1, col1, i)) `Xor` ((Var (row2, col2, i))) | i <- [1..8]]
| x <- [0..2],
y <- [0..2],
row1 <- [3*x .. 3*x+2],
row2 <- [3*x .. 3*x+2],
col1 <- [3*y .. 3*y+2],
col2 <- [3*y .. 3*y+2],
col1 < col2 || row1 < row2 ]
givens = BigAnd $ map (\(i, j, k) -> Var (i, j, k) `And` (Neg $ Var (i, j, k-1)))
[ (0,0,6), (0,4,1), (0,5,7), (0,6,5), (1,1,8), (1,2,1), (1,3,2), (1,7,7)
, (2,5,5), (3,1,2), (3,2,9), (3,3,4), (3,8,1), (4,1,5), (4,2,4), (4,4,2)
, (4,7,3), (5,2,6), (5,4,7), (5,5,8), (5,7,5), (5,8,4), (6,5,9), (6,6,3)
, (6,8,7), (7,2,3), (7,3,8), (7,6,4), (8,2,5), (8,7,9)]
main :: IO ()
main = do
trueVars <- satisfiable sudoku
case trueVars of
Unsatisfiable ->
putStr "unsatisfiable"
Satisfiable eta -> do
let char x y = head [ show i | i <- [1..9], eta ! (y, x, i) ]
line y = concat [ char x y | x <- [0..8] ]
result = concat $ [ line y ++ "\n" | y <- [0..8] ]
putStr result
package beispiele;
import cnf.Formula;
import org.sat4j.specs.TimeoutException;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import static cnf.CNF.*;
public class Damen {
private static final int n = 8;
// Variablennamen
private static String dame(int x, int y) {
return "dame(" + x + ", " + y + ")";
}
private static Formula damen() {
List<Formula> conditions = new LinkedList<>();
// in jeder Spalte eine Dame
for (int x = 0; x < n; x++) {
List<Formula> l = new LinkedList<>();
for (int y = 0; y < n; y++) {
l.add(var(dame(x, y)));
}
conditions.add(or(l));
}
// jede Dame hoechstens einmal in jeder Spalte
for (int x = 0; x < n; x++) {
for (int y1 = 0; y1 < n; y1++) {
for (int y2 = y1 + 1; y2 < n; y2++) {
conditions.add(or(neg(var(dame(x, y1))), neg(var(dame(x, y2)))));
}
}
}
// jede Dame hoechstens einmal in jeder Zeile
for (int y = 0; y < n; y++) {
for (int x1 = 0; x1 < n; x1++) {
for (int x2 = x1 + 1; x2 < n; x2++) {
conditions.add(or(neg(var(dame(x1, y))), neg(var(dame(x2, y)))));
}
}
}
// Damen duerfen nicht diagonal stehen
for (int x1 = 0; x1 < n; x1++) {
for (int y1 = 0; y1 < n; y1++) {
for (int x2 = x1 + 1; x2 < n; x2++) {
for (int y2 = 0; y2 < n; y2++) {
if (x2 - x1 == Math.abs(y2 - y1)) {
conditions.add(or(neg(var(dame(x1, y1))), neg(var(dame(x2, y2)))));
}
}
}
}
}
return and(conditions);
}
public static void main(String[] args) throws TimeoutException {
Map<Object, Boolean> eta = satisfiable(damen());
if (eta == null) {
System.out.println("Nicht erfuellbar.");
} else {
// erfuellbar
for (int x = 0; x < n; x++) {
for (int y = 0; y < n; y++) {
System.out.print(eta.get(dame(x, y)) ? "D " : ". ");
}
System.out.println();
}
}
}
}
Styling with Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!