Abschlussaufgabe 1

All required tests have been passed.

This is your current final solution.

Results

CheckStyle : passed

Java - Compiler : passed

Grundlegende Funktionale Tests : passed

Files

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
package sat.bucket;

import java.util.Collection;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.SortedMap;
import java.util.TreeMap;

import sat.Clause;
import sat.ClauseOperations;
import sat.Literal;
import sat.LiteralOperations;

/**
 * Implementation of the Bucket SAT solvinf algorithm.
 * @author martin
 * @version 1.0
 *
 * @param <V> Type of variables occuring in clauses
 * @param <L> Type of literals occuring in clauses
 * @param <C> Type of clauses
 */
public class BucketSolver<V extends Comparable<V>, L extends Literal<V, L>, C extends Clause<V, L>> {
	private final ClauseOperations<V, L, C> o;
	private final LiteralOperations<V, L> lo;
	private final boolean subsumptionsCheck;
	private final boolean tautologieCheck;
	
	/**
	 * Creates a new {@link BucketSolver}. Subsumption- and tautologiecheck are enabled.
	 * @param o Operations on clauses.
	 * @param lo Operation on literals.
	 */
	public BucketSolver(ClauseOperations<V, L, C> o, LiteralOperations<V, L> lo) {
		this(o, lo, true, true);
	}
	
	/**
	 * Creates a new {@link BucketSolver}.
	 * @param o Operations on clauses.
	 * @param lo Operation on literals.
	 * @param subsumptionsCheck iff true, subsumptioncheck will be enabled
	 * t@param tautologieCheck iff true, tautologiecheck will be enabled.
	 */
	public BucketSolver(ClauseOperations<V, L, C> o,
		                LiteralOperations<V, L> lo,
		                boolean subsumptionsCheck,
		                boolean tautologieCheck) {
		this.o = o;
		this.lo = lo;
		this.subsumptionsCheck = subsumptionsCheck;
		this.tautologieCheck = tautologieCheck;
	}
	
	
	private void addTo(SortedMap<V, List<C>> buckets, V v, C c) {
		assert buckets.containsKey(v);
		List<C> clauses = buckets.get(v);
		
		if (tautologieCheck && c.isTautological()) return;
		
		if (subsumptionsCheck) {
			boolean cIsSubsumedByvClauses = false;
			List<C> subsumedByC = new LinkedList<>();
			for (C c0 : clauses) {
				if (o.subsumes(c0, c)) cIsSubsumedByvClauses = true;
				if (o.subsumes(c, c0))  subsumedByC.add(c0);
			}
			assert !(cIsSubsumedByvClauses && !subsumedByC.isEmpty());
			if (!cIsSubsumedByvClauses) clauses.add(c);
			clauses.removeAll(subsumedByC);
		} else {
			clauses.add(c);
		}
	}
	
	/**
	 * The Bucket solving algorithm.
	 * @param clauses clauses to be checked for satisfiability.
	 * @param output stringbuffer to which a log of the algorithms steps will be appended.
	 * @return true if the clauses are satisfiable, false otherwise.
	 */
	public boolean satisfieable(Collection<C> clauses, StringBuilder output) {
		SortedMap<V, List<C>> buckets = new TreeMap<>();
		
		for (C c : clauses) {
			if (c.isEmpty()) {
				output.append("UNSAT");
				return false;
			}
			for (V v : c.fv()) {
				if (!buckets.containsKey(v)) buckets.put(v, new LinkedList<C>());
			}
			V v = c.min();
			addTo(buckets, v, c);
		}

		for (Map.Entry<V, List<C>> e :  buckets.entrySet()) {
			
			final V var = e.getKey();
			final List<C> vClauses = e.getValue();
			final List<C> neg = new LinkedList<C>();
			final List<C> pos = new LinkedList<C>();
			
			output.append("Processing Bucket " + var + System.lineSeparator());
			
			for (C c : vClauses) {
				if (c.containsNegative(var)) neg.add(c);
				else                         pos.add(c);
			}
			
			for (C cneg : neg) {
				for (C cpos: pos) {
					C resolvant = o.resolve(cneg, cpos, lo.asNegative(var), lo.asPositive(var));
					output.append(cneg + "*" + cpos + "=" + resolvant + System.lineSeparator());
					
					if (resolvant.isEmpty()) {
						output.append("UNSAT" + System.lineSeparator());
						return false; 
					}
					assert (var.compareTo(resolvant.min()) < 0 
					     || cneg.contains(lo.asPositive(var))
					     || cpos.contains(lo.asNegative(var)));
					final V min = resolvant.min();
					addTo(buckets, min, resolvant);
				}
			}
		}
		output.append("SAT" + System.lineSeparator());
		return true;
	}

}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
package sat.ui;

/**
 * Exception, to be raised when parsing an invalid Dimacs input file.
 * @author martin
 * @version 1.0
 *
 */
public class IllegalDimacsFileException extends Exception {
	private static final long serialVersionUID = 1L;
	
	/**
	 * Constructs a new {@link IllegalDimacsFileException}.
	 * @param message the error message
	 */
	public IllegalDimacsFileException(String message) {
		super(message);
	}
	
}
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
package sat.ui;


import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

import sat.Clause;
import sat.ClauseOperations;
import sat.literals.IntLiteral;

/**
 * Parser for Dimacs Files.
 * @author martin
 * @version 1.0
 *
 * @param <C> The type of clauses to be created while parsing the dimacs input.
 */
public class DimacsParser<C extends Clause<Integer, IntLiteral>> {
	
	private static final String HEADER  = "p cnf ([0-9]+) ([0-9]+) *";
	private static final String COMMENT = "c .*";
	private static final String CLAUSE  = "((-?[0-9]+) ?)+ *"; 
	private static final String EMPTY  = "^$";
	
	private static final Pattern HEADER_PATTERN = Pattern.compile(HEADER);
	
	private final ClauseOperations<Integer, IntLiteral, C> o;
	
	/**
	 * Constructs a new {@link DimacsParser}.
	 * @param o Operations to be used to create clause instances
	 */
	public DimacsParser(ClauseOperations<Integer, IntLiteral, C> o) {
		this.o = o;
	}
	
	/**
	 * Parses Dimacs input.
	 * @param lines the Dimacs input files lines.
	 * @return a List of clauses, one each for every clause line in the input.
	 * @throws IllegalDimacsFileException if the input is invalid.
	 */
	public List<C> clausesFrom(List<String> lines) throws IllegalDimacsFileException {
		
		boolean headerRead = false;
		int clausesRead = 0;
		int vars = -1;
		int nrOfclauses = -1;
		
		List<C> clauses = null;
		
		for (String line : lines) {
			if (!(line.matches(HEADER)
		       || line.matches(COMMENT)
		       || line.matches(CLAUSE)
		       || line.matches(EMPTY))) {
				throw new IllegalDimacsFileException("couldbt parse line: " + line);
			}
			
			Matcher hm = HEADER_PATTERN.matcher(line);
			if (hm.matches()) {
				if (headerRead) throw new IllegalDimacsFileException("header already read");
				vars    = Integer.parseInt(hm.group(1));
				nrOfclauses = Integer.parseInt(hm.group(2));
				clauses = new ArrayList<>(nrOfclauses);
				headerRead = true;
				
			}
			
			if (line.matches(CLAUSE)) {
				if (!headerRead) throw new IllegalDimacsFileException("read clause before header");
				if (clausesRead >= nrOfclauses) {
					throw new IllegalDimacsFileException("too many clauses read");
				}
				
				String[] tokens = line.split(" ");
				if (!tokens[tokens.length - 1].equals("0")) {
					throw new IllegalDimacsFileException("no clause line terminator \"0\"");
				}
				
				List<IntLiteral> literals = new LinkedList<>();
				for (int i = 0; i < tokens.length - 1; i++) {
					int literal = 0;
					try {
						literal = Integer.parseInt(tokens[i]);
					} catch (NumberFormatException nfe) {
						throw new IllegalDimacsFileException("Illegal literal: " + tokens[i]);
					}
					if (Math.abs(literal) > vars || literal == 0) {
						throw new IllegalDimacsFileException("Illegal literal: " + literal);
					}
					literals.add(new IntLiteral(literal));
				}
				clauses.add(o.fromCollection(literals));
				clausesRead++;
				headerRead = true;
			}
		}
		
		if (!headerRead) throw new IllegalDimacsFileException("no dimacs header found");
		return clauses;
	}
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
package sat.ui;

import java.io.File;
import java.io.IOException;
import java.nio.charset.StandardCharsets;
import java.nio.file.Files;
import java.util.List;

import sat.bucket.BucketSolver;
import sat.literals.IntLiteral;
import sat.literals.IntLiteralOperations;
import sat.set.SetClause;
import sat.set.SetClauseOperations;


/**
 * The SAT solvers main program. Reads a boolean formula from a dimacs file.
 * @author martin
 * @version 1.0
 *
 */
abstract class DimacsMain {
	private DimacsMain() {
	}

	private static void runOn(String fileName) throws IOException {
		runOn(new File(fileName));
	}
	
	private static void runOn(File file) throws IOException {
		List<String> lines = Files.readAllLines(file.toPath(), StandardCharsets.UTF_8);
		DimacsParser<SetClause<Integer, IntLiteral>> parser
		 = new DimacsParser<>(new SetClauseOperations<Integer, IntLiteral>());
		
		List<SetClause<Integer, IntLiteral>> clauses;
		try {
			clauses = parser.clausesFrom(lines);			
		} catch (IllegalDimacsFileException ide) {
			System.out.println("Error! " + ide.getMessage());
			return;
		}

		
		SetClauseOperations<Integer, IntLiteral> o = new SetClauseOperations<>();
		IntLiteralOperations lo = new IntLiteralOperations();
		BucketSolver<Integer, IntLiteral, SetClause<Integer, IntLiteral>> solver = new BucketSolver<>(o, lo);
		StringBuilder output = new StringBuilder();
		solver.satisfieable(clauses, output);
		System.out.println(output);
	}
	
	/**
	 * The solvers main entry point.
	 * @param args arguments.
	 * @throws IOException 
	 */
	public static void main(String[] args) throws IOException {
		if (args.length != 1) System.out.println("Error! Usage: DimacsMain <cnf_file>");
		try {
			runOn(args[0]);
		} catch (IOException io) {
			System.out.println("Error! reading from " + args[0]);
		}
		
	}
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
package sat;

/**
 * Implementation of resolve(), depending on the remaining clause operations.
 * @author martin
 * @version 1.0
 *
 * @param <V> see {@link ClauseOperations}
 * @param <L> see {@link ClauseOperations}
 * @param <C> see {@link ClauseOperations}
 */
public abstract class GenericClauseOperations<V extends Comparable<V>,
                                              L extends Literal<V, L>,
                                              C extends Clause<V, L>>
                      implements ClauseOperations<V, L, C> {

	
	@Override
	public C resolve(C c1, C c2, V v) {
		if (!c1.contains(v) || !c2.contains(v)) throw new IllegalArgumentException();
		L l1 = null;
		L l2 = null;
		for (L l : c1.occurences(v)) {
			if (c2.contains(l.not())) {
				l1 = l;
				l2 = l1.not();
			}
		}
		if (l1 == null || l2 == null) throw new IllegalArgumentException();
		
		C resolvant = union(c1, c2);
		resolvant.remove(l1);
		resolvant.remove(l2);
		return resolvant;
	};
	
	@Override
	public C resolve(C c1, C c2, L l1, L l2) {
		if (!c1.contains(l1) || !c2.contains(l2)) throw new IllegalArgumentException();
		C resolvant = union(c1, c2);
		resolvant.remove(l1);
		resolvant.remove(l2);
		return resolvant;
	};
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
package sat.boolarray;

import java.util.Collection;


import sat.GenericClauseOperations;
import sat.literals.IntLiteral;

/**
 * Operations on {@link BoolArrayClause}. See {@link ClauseOperations}.
 * @author martin
 * @version 1.0
 */
public class BoolArrayClauseOperations extends GenericClauseOperations<Integer, IntLiteral, BoolArrayClause>  {

	/**
	 * Constructs BoolArrayClauseOperations.
	 */
	public BoolArrayClauseOperations() {
	}
	
	@Override
	public BoolArrayClause union(BoolArrayClause c1, BoolArrayClause c2) {
		return new BoolArrayClause(c1, c2);
	}

	@Override
	public BoolArrayClause fromCollection(Collection<IntLiteral> literals) {
		return new BoolArrayClause(literals);
	}

	@Override
	public boolean subsumes(BoolArrayClause c1, BoolArrayClause c2) {
		return c1.subssumes(c2);
	}

}
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
package sat.boolarray;

import java.util.ArrayList;
import java.util.Collection;
import java.util.LinkedList;

import sat.Clause;
import sat.literals.IntLiteral;
/**
 * A Clause, represented by arrays of boolean.
 * @author martin
 * @version 1.0
 *
 */
public final class BoolArrayClause implements Clause<Integer, IntLiteral> {

	private boolean[] positive;
	private boolean[] negative;
	private int highestvar;
	
	/**
	 * Constructs the union of two other clauses.
	 * @param c1 a clause
	 * @param c2 a clause
	 */
	BoolArrayClause(BoolArrayClause c1, BoolArrayClause c2) {
		highestvar = Math.max(c1.highestvar, c2.highestvar);
		positive = new boolean[highestvar + 1];
		negative = new boolean[highestvar + 1];
		
		for (int i = 1; i <= c1.highestvar; i++) {
			positive[i]  = c1.positive[i];
			negative[i]  = c1.negative[i];
		}
		for (int i = 1; i <= c2.highestvar; i++) {
			positive[i] |= c2.positive[i];
			negative[i] |= c2.negative[i];
		}
	}
	
	/**
	 * Constructs a clause from the given literals.
	 * @param literals literals
	 */
	public BoolArrayClause(Collection<IntLiteral> literals) {
		highestvar = 0;
		for (IntLiteral l : literals) {
			highestvar = Math.max(l.variable(), highestvar);
		}
		positive = new boolean[highestvar + 1];
		negative = new boolean[highestvar + 1];
		
		for (IntLiteral l : literals) {
			boolean[] lookup = l.sign() ? positive : negative;
			lookup[l.variable()] = true;		
		}
	}
	
	
	
	@Override
	public boolean containsNegative(Integer v) {
		assert v > 0;
		return negative[v];
	}

	@Override
	public boolean contains(Integer v) {
		assert v > 0;
		return negative[v] || positive[v];
	}

	@Override
	public boolean contains(IntLiteral l) {
		boolean[] lookup = l.sign() ? positive : negative;
		return lookup[l.variable()];
	}

	@Override
	public Integer min() {
		for (int i = 1; i <= highestvar; i++) {
			if (positive[i] || negative[i]) return i;
		}
		return null;
	}

	@Override
	public Collection<IntLiteral> occurences(Integer v) {
		assert v > 0;
		ArrayList<IntLiteral> occs = new ArrayList<>(2);
		if (positive[v]) occs.add(new IntLiteral(v));
		if (negative[v]) occs.add(new IntLiteral(-v));
		return occs;
	}

	@Override
	public Collection<Integer> fv() {
		LinkedList<Integer> fvs = new LinkedList<>();
		for (int i = 1; i <= highestvar; i++) {
			if (positive[i] || negative[i]) fvs.add(i);
		}
		return fvs;
	}
	@Override
	public void remove(IntLiteral l) {
		boolean[] lookup = l.sign() ? positive : negative;
		lookup[l.variable()] = false;
	}

	@Override
	public boolean isTautological() {
		for (int i = 1; i <= highestvar; i++) {
			if (positive[i] && negative[i]) return true;
		}
		return false;
	}
	
	@Override
	public boolean isEmpty() {
		for (int i = 1; i <= highestvar; i++) {
			if (positive[i] || negative[i]) return false;
		}
		return true;
	}
	
	@Override
	public String toString() {
		StringBuilder sb = new StringBuilder("{");
		boolean first = true;
		String sign = "";
		for (boolean[] literals : new boolean[][] {positive, negative}) {
			for (int i = 1; i <= highestvar; i++) {
				if (literals[i]) {
					if (first) {
						first = false;
					} else {
						sb.append(", ");
					}
					sb.append(sign + i);
				}
			}
			sign = "-";
		}
		sb.append("}");
		return sb.toString();
	}
		
	@Override
	public boolean equals(Object obj) {
		if (!(obj instanceof BoolArrayClause)) return false;
		BoolArrayClause other = (BoolArrayClause) obj;
		return this.subssumes(other);
	}
	
	/**
	 * @param other another clause
	 * @return true iff this clause is subsumed by the other clause
	 */
	boolean subssumes(BoolArrayClause other) {
			int i;
			for (i = 1; i <= Math.min(this.highestvar, other.highestvar); i++) {
				if (this.positive[i] && !other.positive[i]
				 || this.negative[i] && !other.negative[i]) return false; 
			}
			for (; i <= this.highestvar; i++) {
				if (this.positive[i] || this.negative[i]) return false;
				
			}
			return true;
	}
	
	@Deprecated
	private Collection<IntLiteral> toSet() {
		Collection<IntLiteral> literals = new LinkedList<>();
		
		for (int i = 1; i <= highestvar; i++) {
			if (positive[i]) literals.add(new IntLiteral(i));
			if (negative[i]) literals.add(new IntLiteral(-i));
		}
		return literals;
	}

}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
package sat;

/**
 * Operations on Literals.
 * @author martin
 * @version 1.0
 *
 * @param <V> Type of variables a literal is formed from.
 * @param <L> Type of literals.
 */
public interface LiteralOperations<V extends Comparable<V>, L extends Literal<V, L>> {
	/**
	 * @param v a variable
	 * @return the variable as a positive literal
	 */
	L asPositive(V v);

	/**
	 * @param v a variable
	 * @return the variable as a negative literal
	 */
	L asNegative(V v);
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
package sat;

import java.util.Collection;
/**
 * A Clause.
 * @author martin
 * @version 1.0
 *
 * @param <V> Type of variables occuring in clauses
 * @param <L> Type of literals occuring in clauses
 */
public interface Clause<V extends Comparable<V>, L extends Literal<V, L>> {
	
	/**
	 * @param v a variable
	 * @return true iff the clause contains the literal ¬v
	 */
	boolean containsNegative(V v);
	
	/**
	 * @param v a variable
	 * @return true iff the clause contains the literal ¬v or v
	 */
	boolean contains(V v);
	
	/**
	 * @param l a literal
	 * @return true iff the clause contains the literal l
	 */
	boolean contains(L l);
	
	/**
	 * @return the least variable v such that v or ¬v occurs in the clause.
	 */
	V min();
	
	/**
	 * @param v a variable
	 * @return all occurences (positive or negative) of v
	 */
	Collection<L> occurences(V v);
	
	/** 
	 * @return all variables occuring in the clause
	 */
	Collection<V> fv();
	
	/**
	 * removes a literal from the clause.
	 * @param l a literal
	 */
	void remove(L l);
	
	/**
	 * @return true iff the clause contains literals v and ¬v for some variable v
	 */
	boolean isTautological();
	
	/**
	 * @return true iff the clause is the empty clause
	 */
	boolean isEmpty();
	
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
package sat.literals;

import sat.LiteralOperations;

/**
 * Operations on {@link IntLiteral}. See {@link LiteralOperations}.
 * @author martin
 * @version 1.0
 */
public class IntLiteralOperations implements LiteralOperations<Integer, IntLiteral> {
	
	/**
	 * Constructs new {@link IntLiteralOperations}.
	 */
	public IntLiteralOperations() {	
	}
	
	@Override
	public IntLiteral asNegative(Integer v) {
		return new IntLiteral(-Math.abs(v));
	}
	
	@Override
	public IntLiteral asPositive(Integer v) {
		return new IntLiteral(Math.abs(v));
	}
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
package sat.literals;

import sat.Literal;

/**
 * Literals, represented by Intger.
 * @author martin
 * @version 1.0
 *
 */
public final class IntLiteral implements Literal<Integer, IntLiteral> {
	private int lit;

	
	/**
	 * Constructs a new Literal from lit.
	 * @param lit an integer !=0. If positive, represents a positive literal. Otherwise: a negative literal.
	 */
	public IntLiteral(int lit) {
		if (lit == 0) throw new IllegalArgumentException();
		this.lit = lit;
	}

	
	@Override
	public IntLiteral not() {
		return new IntLiteral(-lit);
	}
	
	@Override
	public boolean sign() {
		return (lit > 0);
	}
	
	@Override
	public Integer variable() {
		return Math.abs(lit);
	}
	
	@Override
	public String toString() {
		return Integer.toString(lit);
	}
	
	@Override
	public int hashCode() {
		return lit;
	}


	@Override
	public boolean equals(Object obj) {
		if (!(obj instanceof IntLiteral))
			return false;
		IntLiteral other = (IntLiteral) obj;
		return lit == other.lit;
	}



}
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
package sat.set;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Comparator;
import java.util.HashSet;
import java.util.List;
import java.util.PriorityQueue;
import java.util.Set;

import sat.Clause;
import sat.Literal;
/**
 * A Clause, represented by {@link Set}s.
 * @author martin
 * @version 1.0
 *
 * @param <V> Type of variables occuring in clauses
 * @param <L> Type of literals occuring in clauses
 */
public class SetClause<V extends Comparable<V>, L extends Literal<V, L>> implements Clause<V, L> {
	private final Set<L> literals = new HashSet<L>();
	private V min = null;
	
	/**
	 * Constructs a clause from the given literals.
	 * @param literals literals
	 */
	public SetClause(Collection<L> literals) {
		this.literals.addAll(literals);
		findMin();
	}
	
	/**
	 * Constructs the union of two other clauses.
	 * @param c1 a clause
	 * @param c2 a clause
	 */
	SetClause(SetClause<V, L> c1, SetClause<V, L> c2) {
		literals.addAll(c1.literals);
		literals.addAll(c2.literals);
		findMin();
	}
	
	private void findMin() {
		if (literals.isEmpty()) {
			min = null;
		} else {
			PriorityQueue<L> sortedLiterals = new PriorityQueue<>(literals.size(), new Comparator<L>() {
				public int compare(L l1, L l2) {
					return l1.variable().compareTo(l2.variable());
				};
			});
			sortedLiterals.addAll(literals);
			min = sortedLiterals.peek().variable();
		}
	}
	
	/**
	 * @param other another clause
	 * @return true iff this clause is subsumed by the other clause
	 */
	boolean subsumes(SetClause<V, L> other) {
		return other.literals.containsAll(this.literals);
	}
	
	@Override
	public boolean contains(V v) {
		for (L l : literals) {
			if (l.variable().equals(v)) return true;
		}
		return false;
	};

	@Override
	public boolean containsNegative(V v) {
		for (L l : literals) {
			if (l.variable().equals(v) && !l.sign()) return true;
		}
		return false;
	};
	
	
	@Override
	public boolean contains(L l) {
		return literals.contains(l);
	};
	
	@Override
	public Collection<L> occurences(V v) {
		final List<L> occs = new ArrayList<>(literals.size());
		for (L l : literals) {
			if (l.variable().equals(v)) occs.add(l);
		}
		return occs;
	};
	
	@Override
	public Collection<V> fv() {
		Set<V> fvs = new HashSet<>();
		for (L l : literals) {
			fvs.add(l.variable());
		}
		return fvs;
	}
	
	@Override
	public void remove(L l) {
		literals.remove(l);
		findMin();
	};
	
	@Override
	public String toString() {
		return literals.toString().replace('[', '{').replace(']', '}');
	}
	
	@Override
	public int hashCode() {
		return literals.hashCode();
	}
	
	@Override
	public boolean equals(Object o) {
		if (!(o instanceof SetClause)) return false;
		@SuppressWarnings("unchecked")
		SetClause<V, L> other = (SetClause<V, L>) o;
		return literals.equals(other.literals);
	}
	
	@Override
	public V min() {
		return min;
	}
	
	@Override
	public boolean isTautological() {
		for (L l : literals) {
			if (literals.contains(l.not())) return true;
		}
		return false;
	}
	
	@Override
	public boolean isEmpty() {
		return literals.isEmpty();
	}
	

}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
package sat.set;

import java.util.Collection;


import sat.GenericClauseOperations;
import sat.Literal;

/**
 * 
 * @author martin
 * @version 
 *
 * @param <V> see {@link ClauseOperations}
 * @param <L> see {@link ClauseOperations}
 */
public class SetClauseOperations<V extends Comparable<V>,
                                 L extends Literal<V, L>> 
             extends GenericClauseOperations<V, L, SetClause<V, L>> {
	
	/**
	 * Constructs new {@link SetClauseOperations}.
	 */
	public SetClauseOperations() {
	}
	
	@Override
	public SetClause<V, L> fromCollection(Collection<L> literals) {
		return new SetClause<>(literals);
	}
	@Override
	public SetClause<V, L> union(SetClause<V, L> c1, SetClause<V, L> c2) {
		return new SetClause<>(c1, c2);
	}
	
	@Override
	public boolean subsumes(SetClause<V, L> c1, SetClause<V, L> c2) {
		return c1.subsumes(c2);
	}
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
package sat;

import java.util.Collection;


/**
 * Operations on clauses, as needed by {@link BucketSolver}.
 * @author martin
 * @version 1.0
 *
 * @param <V> Type of variables occuring in clauses
 * @param <L> Type of literals occuring in clauses
 * @param <C> Type of clauses
 */
public interface ClauseOperations<V extends Comparable<V>, L extends Literal<V, L>, C extends Clause<V, L>> {
	/**
	 * 
	 * @param c1 a clause
	 * @param c2 a clause
	 * @return the union of the two clauses
	 */
	C union(C c1, C c2);
	
	/**
	 * @param literals some literals
	 * @return a clause consisting of the given literals
	 */
	C fromCollection(Collection<L> literals);
	
	/**
	 * @param c1 a clause
	 * @param c2 a clause
	 * @param v the variable to be resolved. Must occur positively in one of the clauses,
	 *          and negatively in the other.
	 * @return the resolvant of c1 and c2 via v
	 */
	C resolve(C c1, C c2, V v);
	
	/**
	 * 
	 * @param c1 a clause
	 * @param c2 a clause
	 * @param l1 a literal, the inverse of l2. must occur in c1.
	 * @param l2 a literal, the inverse of l1. must occur in c2.
	 * @return the resolvant of c1 and c2 via v
	 */
	C resolve(C c1, C c2, L l1, L l2);
	
	/**
	 * @param c1 a clause
	 * @param c2 a clause
	 * @return true iff c1 subsumes c2
	 */
	boolean subsumes(C c1, C c2);
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
package sat;

/**
 * A Literal.
 * @author martin
 * @version 1.0
 * 
 * @param <V> Type of variables a literal is formed from.
 * @param <Self> The Selftype of the Literal
 */
public interface Literal<V extends Comparable<V>, Self> {
	/**
	 * @return the literals inverse
	 */
	Self not();
	
	/**
	 * @return the literals sign, i.e.: whether its positive or negative
	 */
	boolean sign();
	
	/**
	 * @return the literals variable.
	 */
	V variable();
}