# Abschlussaufgabe 1

All required tests have been passed.

This is your current final solution.

## 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 Type of variables occuring in clauses * @param Type of literals occuring in clauses * @param Type of clauses */ public class BucketSolver, L extends Literal, C extends Clause> { private final ClauseOperations o; private final LiteralOperations 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 o, LiteralOperations 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 o, LiteralOperations lo, boolean subsumptionsCheck, boolean tautologieCheck) { this.o = o; this.lo = lo; this.subsumptionsCheck = subsumptionsCheck; this.tautologieCheck = tautologieCheck; } private void addTo(SortedMap> buckets, V v, C c) { assert buckets.containsKey(v); List clauses = buckets.get(v); if (tautologieCheck && c.isTautological()) return; if (subsumptionsCheck) { boolean cIsSubsumedByvClauses = false; List 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 clauses, StringBuilder output) { SortedMap> 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()); } V v = c.min(); addTo(buckets, v, c); } for (Map.Entry> e : buckets.entrySet()) { final V var = e.getKey(); final List vClauses = e.getValue(); final List neg = new LinkedList(); final List pos = new LinkedList(); 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 The type of clauses to be created while parsing the dimacs input. */ public class DimacsParser> { 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 o; /** * Constructs a new {@link DimacsParser}. * @param o Operations to be used to create clause instances */ public DimacsParser(ClauseOperations 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 clausesFrom(List lines) throws IllegalDimacsFileException { boolean headerRead = false; int clausesRead = 0; int vars = -1; int nrOfclauses = -1; List 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 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 lines = Files.readAllLines(file.toPath(), StandardCharsets.UTF_8); DimacsParser> parser = new DimacsParser<>(new SetClauseOperations()); List> clauses; try { clauses = parser.clausesFrom(lines); } catch (IllegalDimacsFileException ide) { System.out.println("Error! " + ide.getMessage()); return; } SetClauseOperations o = new SetClauseOperations<>(); IntLiteralOperations lo = new IntLiteralOperations(); BucketSolver> 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 "); 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 see {@link ClauseOperations} * @param see {@link ClauseOperations} * @param see {@link ClauseOperations} */ public abstract class GenericClauseOperations, L extends Literal, C extends Clause> implements ClauseOperations { @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 { /** * Constructs BoolArrayClauseOperations. */ public BoolArrayClauseOperations() { } @Override public BoolArrayClause union(BoolArrayClause c1, BoolArrayClause c2) { return new BoolArrayClause(c1, c2); } @Override public BoolArrayClause fromCollection(Collection 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 { 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 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 occurences(Integer v) { assert v > 0; ArrayList 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 fv() { LinkedList 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 toSet() { Collection 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 Type of variables a literal is formed from. * @param Type of literals. */ public interface LiteralOperations, L extends Literal> { /** * @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 Type of variables occuring in clauses * @param Type of literals occuring in clauses */ public interface Clause, L extends Literal> { /** * @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 occurences(V v); /** * @return all variables occuring in the clause */ Collection 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 { /** * 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 { 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 Type of variables occuring in clauses * @param Type of literals occuring in clauses */ public class SetClause, L extends Literal> implements Clause { private final Set literals = new HashSet(); private V min = null; /** * Constructs a clause from the given literals. * @param literals literals */ public SetClause(Collection literals) { this.literals.addAll(literals); findMin(); } /** * Constructs the union of two other clauses. * @param c1 a clause * @param c2 a clause */ SetClause(SetClause c1, SetClause c2) { literals.addAll(c1.literals); literals.addAll(c2.literals); findMin(); } private void findMin() { if (literals.isEmpty()) { min = null; } else { PriorityQueue sortedLiterals = new PriorityQueue<>(literals.size(), new Comparator() { 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 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 occurences(V v) { final List occs = new ArrayList<>(literals.size()); for (L l : literals) { if (l.variable().equals(v)) occs.add(l); } return occs; }; @Override public Collection fv() { Set 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 other = (SetClause) 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 see {@link ClauseOperations} * @param see {@link ClauseOperations} */ public class SetClauseOperations, L extends Literal> extends GenericClauseOperations> { /** * Constructs new {@link SetClauseOperations}. */ public SetClauseOperations() { } @Override public SetClause fromCollection(Collection literals) { return new SetClause<>(literals); } @Override public SetClause union(SetClause c1, SetClause c2) { return new SetClause<>(c1, c2); } @Override public boolean subsumes(SetClause c1, SetClause 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 Type of variables occuring in clauses * @param Type of literals occuring in clauses * @param Type of clauses */ public interface ClauseOperations, L extends Literal, C extends Clause> { /** * * @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 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 Type of variables a literal is formed from. * @param The Selftype of the Literal */ public interface Literal, 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(); } ```