Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2015 / Formale Spezifikation und Verifikation / Uebungen / SortnetSAT.java


Inhaltsbereich

SortnetSAT.java

Java source code icon SortnetSAT.java — Java source code, 4 KB (4900 bytes)

Dateiinhalt

import cnf.Formula;
import cnf.Var;
import java.util.Set;
import static cnf.CNF.*;
import org.sat4j.specs.TimeoutException;
import java.util.List;
import java.util.LinkedList;

public class SortnetSAT {
    public static void main(String[] args) throws TimeoutException {
        //  int[][] net = {{1,3},{0,2},{2,3},{0,1},{1,2}};
        //  int[][] net = {{1,2},{0,1},{2,3},{0,2},{1,3}};
        //  int wires = 4;

        //  int[][] net = {{2,3},{3,4},{5,6},{6,7},{9,10},{10,11},{13,14},{14,15},{15,16},{16,17},{17,18},{18,19},{0,2},{1,3},{3,5},{4,6},{6,8},{7,9},{11,13},{12,14},{13,15},{14,16},{15,17},{16,18},{0,3},{2,5},{5,8},{7,10},{8,11},{9,12},{10,13},{11,14},{12,15},{13,16},{14,17},{15,18},{2,6},{3,7},{4,8},{5,9},{6,10},{7,11},{8,12},{9,13},{10,14},{11,15},{12,16},{14,18},{15,19},{0,7},{1,8},{4,11},{5,12},{2,15},{1,5},{2,6},{4,8},{5,9},{7,11},{8,12},{11,15},{12,16},{0,12},{0,6},{1,7},{3,9},{4,10},{6,12},{10,16},{13,19},{1,4},{2,5},{3,6},{4,7},{5,8},{6,9},{7,10},{8,11},{9,12},{10,13},{11,14},{12,15},{13,16},{16,19},{0,2},{1,3},{2,4},{3,5},{4,6},{5,7},{6,8},{7,9},{8,10},{9,11},{10,12},{11,13},{12,14},{13,15},{14,16},{15,17},{16,18},{17,19},{2,3},{4,5},{5,6},{6,7},{7,8},{9,10},{10,11},{11,12},{13,14},{16,17},{0,1},{1,2},{2,3},{3,4},{4,5},{5,6},{6,7},{8,9},{9,10},{10,11},{12,13},{14,15},{15,16},{17,18},{18,19}};
        int[][] net = {{17,18},{16,17},{14,15},{13,14},{8,9},{6,7},{2,3},{0,7},{1,8},{4,11},{6,13},{9,16},{12,19},{0,2},{1,3},{3,5},{5,7},{7,9},{8,10},{11,13},{12,14},{13,15},{14,16},{15,17},{17,19},{1,17},{2,18},{0,8},{3,11},{4,12},{6,14},{9,17},{2,6},{3,7},{4,8},{8,12},{9,13},{10,14},{11,15},{12,16},{14,18},{12,19},{10,17},{9,16},{5,12},{1,8},{0,7},{1,3},{4,6},{9,11},{12,14},{13,15},{14,16},{16,18},{17,19},{1,6},{2,7},{3,8},{4,9},{6,11},{7,12},{8,13},{10,15},{11,16},{12,17},{14,19},{0,8},{3,11},{5,13},{8,16},{0,3},{1,4},{2,5},{4,7},{5,8},{6,9},{7,10},{8,11},{9,12},{10,13},{11,14},{13,16},{14,17},{15,18},{0,6},{3,9},{2,6},{3,7},{5,9},{6,10},{8,12},{10,14},{18,19},{16,17},{15,16},{14,15},{13,14},{12,13},{11,12},{10,11},{9,10},{8,9},{7,8},{6,7},{5,6},{4,5},{3,4},{2,3},{1,2},{0,1},{1,2},{2,3},{3,4},{4,5},{5,6},{6,7},{7,8},{8,9},{9,10},{10,11},{11,12},{12,13},{13,14},{14,15},{15,16},{16,17},{17,18}};
        int wires = 20;

        int times = net.length;
        Var[][] vars = new Var[times+1][wires];
        for(int i=0; i<=times; i++){
            for(int j=0; j<wires; j++){
                vars[i][j] = freshVar();
            }
        }

        List<Formula> stepoklist = new LinkedList<Formula>();
        for(int t=0; t<times; t++){
            List<Formula> thisstep = new LinkedList<Formula>();
            for(int n=0; n<wires; n++){
                if(n==net[t][0]){
                    thisstep.add(
                                 iff(
                                     var(vars[t+1][net[t][0]]),
                                     or(
                                        var(vars[t][net[t][0]]),
                                        var(vars[t][net[t][1]])
                                        )
                                     )
                                 );
                }else if(n==net[t][1]){
                    thisstep.add(
                                 iff(
                                     var(vars[t+1][net[t][1]]),
                                     and(
                                         var(vars[t][net[t][0]]),
                                         var(vars[t][net[t][1]])
                                         )
                                     )
                                 );
                }else{
                    thisstep.add(iff(var(vars[t][n]),var(vars[t+1][n])));
                }
            }
            stepoklist.add(and(thisstep));
        }

        List<Formula> unsortlist = new LinkedList<Formula>();
        for(int n=0; n<wires-1; n++){
            unsortlist.add(and(neg(var(vars[times][n])),var(vars[times][n+1])));
        }

        Formula stepsok = and(stepoklist);
        Formula unsorted = or(unsortlist);
        Formula f = and(stepsok,unsorted);

        Set<Var> setting = satisfiable(f);
        if (setting == null) {
            System.out.println("Sortiernetzwerk ist korrekt.");
        } else {
            System.out.print("Sortiernetzwerk ist nicht korrekt.\n" +
                             "Folgende Eingabe wird nicht sortiert:\n");
            for(int n=0; n<wires; n++){
                if(setting.contains(vars[0][n])){
                    System.out.print("1");
                }else{
                    System.out.print("0");
                }
                System.out.print(" --> ");
                if(setting.contains(vars[times][n])){
                    System.out.println("1");
                }else{
                    System.out.println("0");
                }
            }
        }
    }
}

Artikelaktionen


Funktionsleiste