f2490d4a by Ulrich Schoepp

Interfaces zu SAT-Solver (Java/Haskell)

1 parent ab163f03
module Formula (
Formula(..)
) where
data Formula a =
Var a
| TT
| FF
| Neg (Formula a)
| Or (Formula a) (Formula a)
| And (Formula a) (Formula a)
| Xor (Formula a) (Formula a)
| Imp (Formula a) (Formula a)
| Iff (Formula a) (Formula a)
| BigOr [Formula a]
| BigAnd [Formula a]
deriving (Show, Eq, Ord)
Voraussetzungen:
- Haskell Platform (unter Windows besser die 32-Bit-Version)
- Paket picosat (enthält bereits den SAT-Solver Picosat).
Dieses Paket sollte sich einfach so installieren lassen:
cabal install picosat
Beispiel:
ghc Sudoku.hs
./Sudoku
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 [ BigOr [ Var (row, col, i) | i <- [1..9] ]
| row <- [0..8],
col <- [0..8] ]
one_number_each_cell =
BigAnd [ (Neg (Var (row, col, i))) `Or` (Neg (Var (row, col, j)))
| row <- [0..8],
col <- [0..8],
i <- [1..9],
j <- [1..9],
i < j ]
no_number_twice_in_row =
BigAnd [ (Neg (Var (row, col1, i))) `Or` (Neg (Var (row, col2, i)))
| row <- [0..8],
col1 <- [0..8],
col2 <- [0..8],
i <- [1..9],
col1 < col2 ]
no_number_twice_in_col =
BigAnd [ (Neg (Var (row1, col, i))) `Or` (Neg (Var (row2, col, i)))
| row1 <- [0..8],
row2 <- [0..8],
col <- [0..8],
i <- [1..9],
row1 < row2 ]
no_number_twice_in_square =
BigAnd [ (Neg (Var (row1, col1, i))) `Or` (Neg (Var (row2, col2, i)))
| 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],
i <- [1..9],
col1 < col2 || row1 < row2 ]
givens = BigAnd $ map Var
[ (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 = concat [ show i | i <- [1..9], eta ! (x, y, i) ]
line y = concat [ char x y | x <- [0..8] ]
result = concat $ [ line y ++ "\n" | y <- [0..8] ]
putStr result
module Tseitin(
Solution(..),
satisfiable
) where
import Control.Monad.State
import Data.Hashable
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap
import Formula
import qualified Picosat
import System.Mem.StableName
type Literal = Int
type Clause = [Literal]
data Solution a
= Unsatisfiable
| Satisfiable (Map a Bool)
deriving Show
-- state
data St a
= St {
names :: [Int]
, ids :: Map a Int
, vars :: Map Int a
, tseitinMemo :: HashMap (StableName (Formula a)) Int
, clauses :: [Clause]
}
type MT a m = StateT (St a) m
runWithSt :: (MonadIO m, Ord a) => MT a m b -> m b
runWithSt m = evalStateT m initSt
where initSt = St {
names = [1..]
, ids = Map.empty
, vars = Map.empty
, tseitinMemo = HashMap.empty
, clauses = []
}
-- Return a fresh variable id.
freshId :: MonadIO m => MT a m Int
freshId = do
x:xs <- gets names
modify $ \s -> s { names = xs }
return x
-- Add clause c to the list of produced clauses.
emit :: Monad m => Clause -> MT a m ()
emit c = modify (\st -> st { clauses = c:(clauses st) })
-- Get the id of variable v. If v does not have an id, associate a fresh one.
getId :: (Ord a, Eq a, Monad m) => a -> MT a m Int
getId v = do
st <- get
let x:xs = names st
case Map.lookup v (ids st) of
Just i -> return i
Nothing -> do
put $ st {
names = xs,
ids = Map.insert v x (ids st),
vars = Map.insert x v (vars st)
}
return x
-- Given a solution, return a variable assignment.
solution :: (Ord a, MonadIO m) => Picosat.Solution -> MT a m (Solution a)
solution Picosat.Unknown = error "picosat: unknown result"
solution Picosat.Unsatisfiable = return Unsatisfiable
solution (Picosat.Solution sol) = do
st <- get
let setvar x m =
let (i, b) = if x >= 0 then (x, True) else (-x, False) in
case Map.lookup i (vars st) of
Nothing -> m
Just v -> Map.insert v b m
eta = foldr setvar Map.empty sol
return $ Satisfiable eta
-- Tseitin transformation.
tseitin :: (MonadIO m, Ord a) => Formula a -> MT a m Int
tseitin f = do
memo <- gets tseitinMemo
n <- liftIO $ makeStableName f
case HashMap.lookup n memo of
Nothing -> do
x <- tseitin' f
n <- liftIO $ makeStableName f
modify $ \s -> s { tseitinMemo = HashMap.insert n x (tseitinMemo s) }
return x
Just x -> return x
tseitin' :: (MonadIO m, Ord a) => Formula a -> MT a m Int
tseitin' (Var v) =
getId v
tseitin' TT = do
x <- freshId
emit [x]
return x
tseitin' FF = do
x <- freshId
emit [-x]
return x
tseitin' (Neg phi1) = do
x1 <- tseitin phi1
x <- freshId
emit [x, x1]
emit [-x, -x1]
return x
tseitin' (Or phi1 phi2) = do
x1 <- tseitin phi1
x2 <- tseitin phi2
x <- freshId
emit [-x, x1, x2]
emit [-x1, x]
emit [-x2, x]
return x
tseitin' (And phi1 phi2) = do
x1 <- tseitin phi1
x2 <- tseitin phi2
x <- freshId
emit [-x, x1]
emit [-x, x2]
emit [x, -x1, -x2]
return x
tseitin' (Xor phi1 phi2) = do
x1 <- tseitin phi1
x2 <- tseitin phi2
x <- freshId
emit [-x, x1, x2]
emit [-x, -x1, -x2]
emit [x, x1, -x2]
emit [x, -x1, x2]
return x
tseitin' (Imp phi1 phi2) = do
x1 <- tseitin phi1
x2 <- tseitin phi2
x <- freshId
emit [-x, -x1, x2]
emit [x, x1]
emit [x, -x2]
return x
tseitin' (Iff phi1 phi2) = do
x1 <- tseitin phi1
x2 <- tseitin phi2
x <- freshId
emit [x, x1, x2]
emit [x, -x1, -x2]
emit [-x, x1, -x2]
emit [-x, -x1, x2]
return x
tseitin' (BigOr phis) = do
xs <- mapM tseitin phis
x <- freshId
_ <- forM xs (\xi -> emit [x, -xi])
emit (-x : xs)
return x
tseitin' (BigAnd phis) = do
xs <- mapM tseitin phis
x <- freshId
_ <- forM xs (\xi -> emit [-x, xi])
emit (x : [-xi | xi <- xs])
return x
-- Check phi for satisfiablity. If true, return a satisfying assignment. in the
satisfiable :: (Ord a, Eq a, Show a) => Formula a -> IO (Solution a)
satisfiable phi = runWithSt $ do
x <- tseitin phi
cs <- gets clauses
eta <- liftIO $ Picosat.solve ([x] : cs)
solution eta
Beipielprogramme:
javac -cp .:org.sat4j.core.jar beispiele/Test.java
java -cp .:org.sat4j.core.jar beispiele/Test
javac -cp .:org.sat4j.core.jar beispiele/Sudoku.java
java -cp .:org.sat4j.core.jar beispiele/Sudoku
Für die Tests auf Erfüllbarkeit wird der Sat-Solver SAT4J verwendet.
Dieser ist in der Datei org.sat4j.core.jar enthalten, welche für die
Kompilation und Ausführung im CLASSPATH stehen muss.
SAT4J kann auch wie zchaff oder minisat als eigenständiger Sat-Solver
benutzt werden, der seine Eingabe als Textdatei im DIMACS-Format erhält.
Aufruf dann:
java -jar org.sat4j.core.jar formel.dimacs
package beispiele;
import cnf.Formula;
import static cnf.CNF.*;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import org.sat4j.specs.TimeoutException;
public class Sudoku {
// Variablennamen
private static String pos(int x, int y, int z) {
return "pos(" + x + ", " + y + ", " + z + ")";
}
private static Formula sudoku(Integer[][] givens) {
List<Formula> conditions = new LinkedList<>();
// Vorgaben
for (int x = 0; x < 9; x++) {
for (int y = 0; y < 9; y++) {
if (givens[x][y] != null) {
conditions.add(var(pos(x, y, givens[x][y])));
}
}
}
// an jeder Stelle eine Zahl
for (int x = 0; x < 9; x++) {
for (int y = 0; y < 9; y++) {
List<Formula> l = new LinkedList<>();
for (int z = 1; z < 10; z++) {
l.add(var(pos(x, y, z)));
}
conditions.add(or(l));
}
}
// nicht zwei Zahlen an der gleichen Stelle
for (int x = 0; x < 9; x++) {
for (int y = 0; y < 9; y++) {
for (int z1 = 1; z1 < 10; z1++) {
for (int z2 = z1 + 1; z2 < 10; z2++) {
conditions.add(or(neg(var(pos(x, y, z1))), neg(var(pos(x, y, z2)))));
}
}
}
}
// jede Zahl hoechstens einmal in jeder Spalte
for (int x = 0; x < 9; x++) {
for (int y1 = 0; y1 < 9; y1++) {
for (int y2 = y1 + 1; y2 < 9; y2++) {
for (int z = 1; z < 10; z++) {
conditions.add(or(neg(var(pos(x, y1, z))), neg(var(pos(x, y2, z)))));
}
}
}
}
// jede Zahl hoechstens einmal in jeder Zeile
for (int y = 0; y < 9; y++) {
for (int x1 = 0; x1 < 9; x1++) {
for (int x2 = x1 + 1; x2 < 9; x2++) {
for (int z = 1; z < 10; z++) {
conditions.add(or(neg(var(pos(x1, y, z))), neg(var(pos(x2, y, z)))));
}
}
}
}
// keine Zahl in einem 3x3-Block doppelt
for (int bx = 0; bx < 3; bx++) {
for (int by = 0; by < 3; by++) {
for (int x1 = 3 * bx; x1 < 3 * bx + 3; x1++) {
for (int x2 = x1 + 1; x2 < 3 * bx + 3; x2++) {
for (int y1 = 3 * by; y1 < 3 * by + 3; y1++) {
for (int y2 = y1 + 1; y2 < 3 * by + 3; y2++) {
for (int z = 1; z < 10; z++) {
conditions.add(or(neg(var(pos(x1, y1, z))), neg(var(pos(x2, y2, z)))));
}
}
}
}
}
}
}
return and(conditions);
}
public static void main(String[] args) throws TimeoutException {
Integer b = null; // blank
Integer[][] sudoku = {
new Integer[]{6, b, b, b, 1, 7, 5, b, b},
new Integer[]{b, 8, 1, 2, b, b, b, 7, b},
new Integer[]{b, b, b, b, b, 5, b, b, b},
new Integer[]{b, 2, 9, 4, b, b, b, b, 1},
new Integer[]{b, 5, 4, b, 2, b, b, 3, b},
new Integer[]{b, b, 6, b, 7, 8, b, 5, 4},
new Integer[]{b, b, b, b, b, 9, 3, b, 7},
new Integer[]{b, b, 3, 8, b, b, 4, b, b},
new Integer[]{b, b, 5, b, b, b, b, 9, b}};
Formula f = sudoku(sudoku);
Map<Object, Boolean> trueVars = satisfiable(f);
if (trueVars == null) {
System.out.println("Nicht erfuellbar.");
} else {
// erfuellbar
for (int x = 0; x < 9; x++) {
for (int y = 0; y < 9; y++) {
for (int z = 1; z < 10; z++) {
if (trueVars.get(pos(x, y, z))) {
System.out.print(z + " ");
}
}
}
System.out.println();
}
}
}
}
package beispiele;
import cnf.Formula;
import java.io.IOException;
import java.util.Map;
import java.util.Set;
import static cnf.CNF.*;
import org.sat4j.specs.TimeoutException;
public class Test {
public static void main(String[] args) throws TimeoutException, IOException {
Formula f = or(and(var("x1"), var("x2")), and(var("x3"), var("x4")));
System.out.println("Formel f: " + f);
Map<Object, Boolean> eta = satisfiable(f);
if (eta == null) {
System.out.println("Formel f ist unerfüllbar.");
} else {
System.out.println("Formel f ist erfüllbar, "+
" z.B. durch folgende Belegung");
System.out.print(eta);
System.out.println();
}
System.out.println("\n\nZu f erfuellbarkeitsaequivalente Formel in KNF im DIMACS-Format:");
Map<Integer, Object> vars = writeDIMACS(System.out, f);
System.out.println("Bedeutung der Variablen: " + vars);
}
}
package cnf;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.TimeoutException;
import java.io.IOException;
import java.io.OutputStream;
import java.io.Writer;
import java.util.*;
/**
* Methoden zur Konstruktion von aussagenlogischen
* Formeln sowie zum Aufruf eines SAT-Solvers.
* <p>
* Diese Klasse ist das gesamte oeffentliche Interface des
* Pakets {@code cnf}. Die anderen Klassen stellen kein
* oeffentliches Interface bereit.
*/
public class CNF {
// Diese Klasse sammelt nur statische Methoden; man benoetigt
// keine Instanzen davon.
private CNF() {
}
/**
* Erzeugt die Formel, die durch eine aussagenlogische Variable
* gegeben ist.
*
* @param name Name der Variable
*/
public static Formula var(Object name) {
if (name == null) {
throw new NullPointerException("Variablenname darf nicht `null' sein!");
}
return new FormulaVar(name);
}
/**
* Erzeugt die immer wahre Formel.
*/
public static Formula tt() {
return and();
}
/**
* Erzeugt die immer falsche Formel.
*/
public static Formula ff() {
return or();
}
/**
* Erzeugt die Negation einer gegbenen Formel.
*/
public static Formula neg(Formula f) {
return new FormulaNeg(f);
}
/**
* Erzeugt die Konjunktion zweier Formeln.
*/
public static Formula and(Formula f1, Formula f2) {
List<Formula> fms = new LinkedList<>();
fms.add(f1);
fms.add(f2);
return new FormulaAnd(fms);
}
/**
* Erzeugt die Konjunktion einer Liste von Formeln.
*/
public static Formula and(List<Formula> fms) {
return new FormulaAnd(fms);
}
/**
* Erzeugt die Konjunktion einer Liste von Formeln.
*/
public static Formula and(Formula... fms) {
return new FormulaAnd(Arrays.asList(fms));
}
/**
* Erzeugt die Disjunktion zweier Formeln.
*/
public static Formula or(Formula f1, Formula f2) {
List<Formula> fms = new LinkedList<>();
fms.add(f1);
fms.add(f2);
return new FormulaOr(fms);
}
/**
* Erzeugt die Disjunktion einer Liste von Formeln.
*/
public static Formula or(List<Formula> fms) {
return new FormulaOr(fms);
}
/**
* Erzeugt die Disjunktion einer Liste von Formeln.
*/
public static Formula or(Formula... fms) {
return new FormulaOr(Arrays.asList(fms));
}
/**
* Erzeugt die Implikation zweier Formeln.
*
* @param fm1 Formel
* @param fm2 Formel
* @return Formel "fm1 => fm2"
*/
public static Formula imp(Formula fm1, Formula fm2) {
return or(neg(fm1), fm2);
}
/**
* Erzeugt die Biimplikation zweier Formeln.
*
* @param fm1 Formel
* @param fm2 Formel
* @return Formel "fm1 <=> fm2"
*/
public static Formula iff(Formula fm1, Formula fm2) {
return and(imp(fm1, fm2), imp(fm2, fm1));
}
/**
* Erzeugt das exklusive Oder zweier Formeln.
*/
public static Formula xor(Formula fm1, Formula fm2) {
return or(and(fm1, neg(fm2)), and(neg(fm1), fm2));
}
/**
* Wendet die Tseitin-Transformation an und schreibt das Ergebnis im DIMACS-Format in den {@code os}.
* Zurueckgegeben wird eine Map, welche die Zahlen im DIMACS-Text den Variablen in {@code f} zuordnet.
*/
public static Map<Integer, Object> writeDIMACS(OutputStream os, Formula f) throws IOException {
TseitinVisitor tseitinVisitor = new TseitinVisitor();
Integer x = f.accept(tseitinVisitor);
tseitinVisitor.writeResultDIMACS(os, x);
return tseitinVisitor.getVarNameMap();
}
/**
* Wandelt die uebergebene Formel in eine erfuellbarkeitsaequivalente Formel
* in CNF um und ueberprueft sie mittels des SAT-Solvers SAT4j auf Erfuellbarkeit.
* <p>
* Zurueckgegeben wird eine erfuellende Belegung von {@ f} oder {@code null},
* wenn es keine solche gibt.
*
* @param f Formel
* @return Menge der Variablen, die in einer erfuellenden Belegung
* von {@code f} wahr sind; oder {@code null} wenn {@code f}
* unerfuellbar ist.
* @throws TimeoutException
*/
public static Map<Object, Boolean> satisfiable(Formula f) throws TimeoutException {
TseitinVisitor tseitinVisitor = new TseitinVisitor();
Integer x = f.accept(tseitinVisitor);
Set<Set<Integer>> clauses = tseitinVisitor.getClauses();
ISolver solver = SolverFactory.newDefault();
solver.setExpectedNumberOfClauses(clauses.size());
try {
solver.addClause(new VecInt(new int[]{x}));
for (Set<Integer> c : clauses) {
int[] carr = new int[c.size()];
int i = 0;
for (Integer y : c) {
carr[i] = y;
i++;
}
solver.addClause(new VecInt(carr));
}
} catch (ContradictionException ex) {
return null; // unsat
}
IProblem problem = solver;
if (problem.isSatisfiable()) {
int[] model = problem.model();
Map<Object, Boolean> eta = new HashMap<>();
for (Integer y : model) {
Object var = tseitinVisitor.getVar(Math.abs(y));
if (var != null) {
eta.put(tseitinVisitor.getVar(Math.abs(y)), y > 0);
}
}
return eta;
} else {
return null;
}
}
}
package cnf;
/**
* Repraesentation aussagenlogischer Formeln.
* <p>
* Diese Klasse stellt neben {@toString}
* kein oeffentliches Interface bereit.
* Formeln koennen mit den Methoden der Klasse {@code CNF}
* konstruiert werden.
*/
public abstract class Formula {
// package-private
Formula() {}
abstract <A> A accept(FormulaVisitor<A> visitor);
/**
* Wandelt die repraesentierte Formel in einen String um.
*/
abstract public String toString();
}
package cnf;
import java.util.List;
final class FormulaAnd extends Formula {
final List<Formula> fms;
public FormulaAnd(List<Formula> fms) {
this.fms = fms;
}
<A> A accept(FormulaVisitor<A> visitor) {
return visitor.visitAnd(this);
}
@Override
public String toString() {
StringBuffer s = new StringBuffer();
s.append("and(");
String sep = "";
for(Formula f : fms) {
s.append(sep);
s.append(f.toString());
sep = ", ";
}
s.append(")");
return s.toString();
}
@Override
public boolean equals(Object obj) {
if (obj == null) {
return false;
}
if (getClass() != obj.getClass()) {
return false;
}
final FormulaAnd other = (FormulaAnd) obj;
if (this.fms != other.fms && (this.fms == null || !this.fms.equals(other.fms))) {
return false;
}
return true;
}
@Override
public int hashCode() {
int hash = 3;
hash = 73 * hash + (this.fms != null ? this.fms.hashCode() : 0);
return hash;
}
}
package cnf;
final class FormulaNeg extends Formula {
final Formula fm;
public FormulaNeg(Formula fm) {
this.fm = fm;
}
<A> A accept(FormulaVisitor<A> visitor) {
return visitor.visitNeg(this);
}
@Override
public String toString() {
return "neg(" + fm + ")";
}
@Override
public boolean equals(Object obj) {
if (obj == null) {
return false;
}
if (getClass() != obj.getClass()) {
return false;
}
final FormulaNeg other = (FormulaNeg) obj;
if (this.fm != other.fm && (this.fm == null || !this.fm.equals(other.fm))) {
return false;
}
return true;
}
@Override
public int hashCode() {
int hash = 5;
hash = 37 * hash + (this.fm != null ? this.fm.hashCode() : 0);
return hash;
}
}
package cnf;
import java.util.List;
final class FormulaOr extends Formula {
final List<Formula> fms;
public FormulaOr(List<Formula> fms) {
this.fms = fms;
}
<A> A accept(FormulaVisitor<A> visitor) {
return visitor.visitOr(this);
}
@Override
public String toString() {
StringBuffer s = new StringBuffer();
s.append("or(");
String sep = "";
for(Formula f : fms) {
s.append(sep);
s.append(f.toString());
sep = ", ";
}
s.append(")");
return s.toString();
}
@Override
public boolean equals(Object obj) {
if (obj == null) {
return false;
}
if (getClass() != obj.getClass()) {
return false;
}
final FormulaOr other = (FormulaOr) obj;
if (this.fms != other.fms && (this.fms == null || !this.fms.equals(other.fms))) {
return false;
}
return true;
}
@Override
public int hashCode() {
int hash = 7;
hash = 97 * hash + (this.fms != null ? this.fms.hashCode() : 0);
return hash;
}
}
package cnf;
final class FormulaVar extends Formula {
final Object name;
public FormulaVar(Object name) {
this.name = name;
}
<A> A accept(FormulaVisitor<A> visitor) {
return visitor.visitVar(this);
}
@Override
public String toString() {
return name.toString();
}