WIP: SAT encodings for CSP

src/main/java/com/booleworks/logicng/csp/Csp.java

@@ -0,0 +1,164 @@
+package com.booleworks.logicng.csp;
+
+import com.booleworks.logicng.csp.predicates.CspPredicate;
+import com.booleworks.logicng.csp.terms.IntegerVariable;
+import com.booleworks.logicng.formulas.Formula;
+import com.booleworks.logicng.formulas.Variable;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.stream.Collectors;
+
+public class Csp {
+    //private int[] bases;
+    private final List<IntegerVariable> integerVariables;
+    private final List<Variable> booleanVariables;
+    private List<IntegerClause> clauses;
+    private final Map<String, IntegerVariable> integerVariableMap;
+    private final Map<String, Variable> booleanVariableMap;
+    private final CspFactory f;
+
+    private Csp(final CspFactory f) {
+        this.integerVariables = new ArrayList<>();
+        this.booleanVariables = new ArrayList<>();
+        this.clauses = new ArrayList<>();
+        this.integerVariableMap = new HashMap<>();
+        this.booleanVariableMap = new HashMap<>();
+        this.f = f;
+    }
+
+    private Csp(final Csp other) {
+        this.integerVariableMap = new HashMap<>(other.integerVariableMap);
+        this.booleanVariableMap = new HashMap<>(other.booleanVariableMap);
+        this.integerVariables = new ArrayList<>(other.integerVariables);
+        this.booleanVariables = new ArrayList<>(other.booleanVariables);
+        this.clauses = new ArrayList<>(other.clauses);
+        this.f = other.f;
+    }
+
+    public List<IntegerVariable> getIntegerVariables() {
+        return this.integerVariables;
+    }
+
+    public List<Variable> getBooleanVariables() {
+        return this.booleanVariables;
+    }
+
+    public List<IntegerClause> getClauses() {
+        return this.clauses;
+    }
+
+    public CspFactory getCspFactory() {
+        return this.f;
+    }
+
+    @Override
+    public String toString() {
+        return "IntegerCsp{" +
+                "integerVariables=" + this.integerVariables +
+                ", booleanVariables=" + this.booleanVariables +
+                ", clauses=" + this.clauses +
+                '}';
+    }
+
+    public static Csp fromFormula(final CspPredicate formula, final CspFactory cf) {
+        final Formula decomposedFormula = formula.decompose();
+        final Csp.Builder converted = CspConversion.convert(Collections.singletonList(decomposedFormula), cf);
+        return converted.build();
+    }
+
+    public static Csp fromFormulas(final Collection<CspPredicate> formulas, final CspFactory cf) {
+        final var decomposedFormulas = formulas.stream().map(CspPredicate::decompose).collect(Collectors.toList());
+        final Csp.Builder converted = CspConversion.convert(decomposedFormulas, cf);
+        return converted.build();
+    }
+
+    public static class Builder {
+        private Csp csp;
+        private int auxIntegerVariables = 0;
+        private int auxBoolVariables = 0;
+
+        public Builder(final CspFactory f) {
+            this.csp = new Csp(f);
+        }
+
+        public void addClause(final IntegerClause clause) {
+            this.csp.clauses.add(clause);
+        }
+
+        public void setClauses(final List<IntegerClause> clauses) {
+            this.csp.clauses = clauses;
+        }
+
+        public boolean addIntegerVariable(final IntegerVariable v) {
+            final String name = v.getName();
+            if (this.csp.integerVariableMap.containsKey(name)) {
+                return false;
+            } else {
+                this.csp.integerVariableMap.put(name, v);
+                this.csp.integerVariables.add(v);
+                return true;
+            }
+        }
+
+        public boolean addBooleanVariable(final Variable v) {
+            final String name = v.name();
+            if (this.csp.booleanVariableMap.containsKey(name)) {
+                return false;
+            } else {
+                this.csp.booleanVariableMap.put(name, v);
+                this.csp.booleanVariables.add(v);
+                return true;
+            }
+        }
+
+        public IntegerVariable addAuxIntVariable(final String prefix, final IntegerDomain domain) {
+            final IntegerVariable v = IntegerVariable.auxVar(prefix + (this.auxIntegerVariables + 1), domain);
+            ++this.auxIntegerVariables;
+            addIntegerVariable(v);
+            return v;
+        }
+
+        public Variable addAuxBoolVariable(final String prefix) {
+            final Variable v = this.csp.getCspFactory().getFormulaFactory().variable(prefix + (this.auxBoolVariables + 1));
+            ++this.auxBoolVariables;
+            addBooleanVariable(v);
+            return v;
+        }
+
+        public Csp buildClone() {
+            return new Csp(this.csp);
+        }
+
+        public Csp build() {
+            final Csp csp = this.csp;
+            this.csp = null;
+            return csp;
+        }
+
+        public List<IntegerVariable> getIntegerVariables() {
+            return this.csp.integerVariables;
+        }
+
+        public List<Variable> getBooleanVariables() {
+            return this.csp.booleanVariables;
+        }
+
+        public List<IntegerClause> getClauses() {
+            return this.csp.clauses;
+        }
+
+        public CspFactory getCspFactory() {
+            return this.csp.f;
+        }
+
+        @Override
+        public String toString() {
+            return this.csp.toString();
+        }
+    }
+}

src/main/java/com/booleworks/logicng/csp/CspAssignment.java

@@ -0,0 +1,80 @@
+package com.booleworks.logicng.csp;
+
+import com.booleworks.logicng.csp.terms.IntegerVariable;
+import com.booleworks.logicng.formulas.Literal;
+import com.booleworks.logicng.formulas.Variable;
+
+import java.util.Collections;
+import java.util.Map;
+import java.util.SortedSet;
+import java.util.TreeMap;
+import java.util.TreeSet;
+
+public class CspAssignment {
+    private final Map<IntegerVariable, Integer> integerAssignments = new TreeMap<>();
+    private final SortedSet<Variable> posBooleans = new TreeSet<>();
+    private final SortedSet<Literal> negBooleans = new TreeSet<>();
+
+    public CspAssignment() {}
+
+    public Map<IntegerVariable, Integer> getIntegerAssignments() {
+        return Collections.unmodifiableMap(this.integerAssignments);
+    }
+
+    public SortedSet<Variable> positiveBooleans() {
+        return Collections.unmodifiableSortedSet(this.posBooleans);
+    }
+
+    public SortedSet<Literal> negativeBooleans() {
+        return Collections.unmodifiableSortedSet(this.negBooleans);
+    }
+
+    public void addLiteral(final Literal lit) {
+        if (lit.phase()) {
+            this.posBooleans.add(lit.variable());
+        } else {
+            this.negBooleans.add(lit);
+        }
+    }
+
+    public void addPos(final Variable var) {
+        this.posBooleans.add(var);
+    }
+
+    public void addNeg(final Literal lit) {
+        this.negBooleans.add(lit);
+    }
+
+    public void addIntAssignment(final IntegerVariable var, final int value) {
+        this.integerAssignments.put(var, value);
+    }
+
+    @Override
+    public boolean equals(final Object o) {
+        if (this == o) {return true;}
+        if (o == null || getClass() != o.getClass()) {return false;}
+
+        final CspAssignment that = (CspAssignment) o;
+
+        if (!this.integerAssignments.equals(that.integerAssignments)) {return false;}
+        if (!this.posBooleans.equals(that.posBooleans)) {return false;}
+        return this.negBooleans.equals(that.negBooleans);
+    }
+
+    @Override
+    public int hashCode() {
+        int result = this.integerAssignments.hashCode();
+        result = 31 * result + this.posBooleans.hashCode();
+        result = 31 * result + this.negBooleans.hashCode();
+        return result;
+    }
+
+    @Override
+    public String toString() {
+        return "CspAssignment{" +
+                "integerAssignments=" + this.integerAssignments +
+                ", posBooleans=" + this.posBooleans +
+                ", negBooleans=" + this.negBooleans +
+                '}';
+    }
+}

src/main/java/com/booleworks/logicng/csp/CspConversion.java

@@ -0,0 +1,129 @@
+package com.booleworks.logicng.csp;
+
+import com.booleworks.logicng.csp.literals.ArithmeticLiteral;
+import com.booleworks.logicng.csp.literals.LinearLiteral;
+import com.booleworks.logicng.csp.predicates.ComparisonPredicate;
+import com.booleworks.logicng.csp.terms.IntegerVariable;
+import com.booleworks.logicng.csp.terms.Term;
+import com.booleworks.logicng.formulas.And;
+import com.booleworks.logicng.formulas.Formula;
+import com.booleworks.logicng.formulas.Literal;
+import com.booleworks.logicng.formulas.Or;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.List;
+
+public class CspConversion {
+    public static Csp.Builder convert(final List<Formula> cspFormulas, final CspFactory f) {
+        final Csp.Builder csp = new Csp.Builder(f);
+        for (final Formula cspFormula : cspFormulas) {
+            convertCspFormula(cspFormula, csp);
+        }
+        return csp;
+    }
+
+    static void convertCspFormula(final Formula cspFormula, final Csp.Builder csp) {
+        switch (cspFormula.type()) {
+            case OR:
+                convertClause((Or) cspFormula, csp);
+                break;
+            case AND:
+                convertConjunction((And) cspFormula, csp);
+                break;
+            case LITERAL:
+                convertLiteralAsClause((Literal) cspFormula, csp);
+                break;
+            case PREDICATE:
+                if (cspFormula instanceof ComparisonPredicate) {
+                    convertComparisonAsClause((ComparisonPredicate) cspFormula, csp);
+                } else {
+                    throw new IllegalArgumentException("Invalid predicate for CSP conversion: " + cspFormula.getClass());
+                }
+                break;
+            default:
+                throw new IllegalArgumentException("Invalid formula type for CSP conversion: " + cspFormula.type());
+        }
+    }
+
+    static void convertConjunction(final And conjunction, final Csp.Builder csp) {
+        for (final Formula clause : conjunction.operands()) {
+            switch (clause.type()) {
+                case OR:
+                    convertClause((Or) clause, csp);
+                    break;
+                case LITERAL:
+                    convertLiteralAsClause((Literal) clause, csp);
+                    break;
+                case PREDICATE:
+                    if (clause instanceof ComparisonPredicate) {
+                        convertComparisonAsClause((ComparisonPredicate) clause, csp);
+                    } else {
+                        throw new IllegalArgumentException("Invalid predicate for CSP conversion: " + clause.getClass());
+                    }
+                    break;
+                default:
+                    throw new IllegalArgumentException("Invalid formula type for CSP conversion:" + clause.type());
+            }
+        }
+    }
+
+    static void convertLiteralAsClause(final Literal literal, final Csp.Builder csp) {
+        csp.addBooleanVariable(literal.variable());
+        csp.addClause(new IntegerClause(Collections.singletonList(literal), Collections.emptyList()));
+    }
+
+    static void convertComparisonAsClause(final ComparisonPredicate predicate, final Csp.Builder csp) {
+        final LinearLiteral lit = convertComparison(predicate, csp);
+        csp.addClause(new IntegerClause(Collections.emptyList(), Collections.singletonList(lit)));
+    }
+
+    static void convertClause(final Or clause, final Csp.Builder csp) {
+        final List<Literal> boolVariables = new ArrayList<>();
+        final List<ArithmeticLiteral> arithVariables = new ArrayList<>();
+        for (final Formula literal : clause.operands()) {
+            switch (literal.type()) {
+                case LITERAL:
+                    csp.addBooleanVariable(((Literal) literal).variable());
+                    boolVariables.add((Literal) literal);
+                    break;
+                case PREDICATE:
+                    if (literal instanceof ComparisonPredicate) {
+                        arithVariables.add(convertComparison((ComparisonPredicate) literal, csp));
+                    } else {
+                        throw new IllegalArgumentException("Invalid predicate for CSP conversion: " + literal.getClass());
+                    }
+                    break;
+                default:
+                    throw new IllegalArgumentException("Invalid literal type for CSP conversion" + literal.type());
+            }
+        }
+        csp.addClause(new IntegerClause(boolVariables, arithVariables));
+    }
+
+    static LinearLiteral convertComparison(final ComparisonPredicate predicate, final Csp.Builder csp) {
+        final LinearLiteral.Operator op;
+        switch (predicate.getType()) {
+            case EQ:
+                op = LinearLiteral.Operator.EQ;
+                break;
+            case NE:
+                op = LinearLiteral.Operator.NE;
+                break;
+            case LE:
+                op = LinearLiteral.Operator.LE;
+                break;
+            case GE:
+                op = LinearLiteral.Operator.GE;
+                break;
+            default:
+                throw new UnsupportedOperationException("Invalid comparison type for csp conversion: " + predicate.getType());
+        }
+        assert predicate.getRight().getType() == Term.Type.ZERO;
+        final LinearExpression sum = predicate.getLeft().decompose().getLinearExpression();
+        for (final IntegerVariable variable : sum.getVariables()) {
+            csp.addIntegerVariable(variable);
+        }
+        return new LinearLiteral(sum, op);
+    }
+}