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;
	}

}

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);
	}
	
}

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;
	}
}

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]);
		}
		
	}
}

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;
	};
}

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);
	}

}

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;
	}

}

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);
}

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();
	
}

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));
	}
}

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;
	}



}

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();
	}
	

}

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);
	}
}

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);
}