Brute force SAT solver in Java

Question

(See the next iteration.)

I have this small library for solving the SAT (satisfiability problem) via brute force: we are given a boolean formula, which is a conjuction (and) of clauses. Each clause is a disjunction (or) of variables or their negatives. Also, each clause may be negated.

Given a formula, we want to compute such assignments to binary variables, that the formula is evaluated to true.

For example, my demonstration program finds the assignment to

\$(\neg x_1 \vee x_2) \wedge \neg (x_2 \vee \neg x_3),\$

which is \$(x_1, x_2, x_3) = (0, 0, 1).\$

BinaryVariable.java

package net.coderodde.sat;

/**
 * This class represents a binary variable.
 * 
 * @author Rodion "rodde" Efremov
 * @version 1.6 (Mar 30, 2017)
 */
public final class BinaryVariable {

    /**
     * The ID of this binary variable.
     */
    private final int id;

    public BinaryVariable(int id) {
        this.id = id;
    }

    @Override
    public int hashCode() {
        return id;
    }

    @Override
    public boolean equals(Object o) {
        if (o == null) {
            return false;
        }

        if (o == this) {
            return true;
        }

        if (!getClass().equals(o.getClass())) {
            return false;
        }

        return id == ((BinaryVariable) o).id;
    }

    @Override
    public String toString() {
        return "x_" + id;
    }
}

Clause.java

package net.coderodde.sat;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

/**
 * This class represents a clause that holds a disjunction of variables or their
 * respective negations.
 * 
 * @author Rodion "rodde" Efremov
 * @version 1.6 (Mar 30, 2017)
 */
public final class Clause {

    /**
     * List of variables present in this clause.
     */
    private final List<BinaryVariable> binaryVariableList = new ArrayList<>();

    /**
     * The set of variables that are negated.
     */
    private final Set<BinaryVariable> negatedBinaryVariableSet = 
            new HashSet<>();

    /**
     * Indicates whether this entire clause is negated.
     */
    private final boolean negated;

    /**
     * Constructs an empty clause.
     * 
     * @param negated whether this clause is negated or not.
     */
    public Clause(boolean negated) {
        this.negated = negated;
    }

    /**
     * Constructs an empty, non-negated clause.
     */
    public Clause() {
        this(false);
    }

    /**
     * Adds a non-negated variable to this clause.
     * 
     * @param binaryVariable the variable to add.
     */
    public void addBinaryVariable(BinaryVariable binaryVariable) {
        addBinaryVariable(binaryVariable, false);
    }

    /**
     * Adds a possible negated variable to this clause.
     * 
     * @param binaryVariable the variable to add.
     * @param negated indicates whether the variable is to be negated.
     */
    public void addBinaryVariable(BinaryVariable binaryVariable, boolean negated) {
        binaryVariableList.add(binaryVariable);

        if (negated) {
            negatedBinaryVariableSet.add(binaryVariable);
        }
    }

    /**
     * Checks whether the input assignment satisfies this clause.
     * 
     * @param assignment the assignment map.
     * @return {@code true} if the assignment satisfies this clause, and 
     *         {@code false} otherwise.
     */
    public boolean isSatisfied(Map<BinaryVariable, Boolean> assignment) {
        for (BinaryVariable binaryVariable : binaryVariableList) {
            if (negatedBinaryVariableSet.contains(binaryVariable)) {
                if (assignment.get(binaryVariable).equals(Boolean.FALSE)) {
                    return !negated;
                }
            } else {
                if (assignment.get(binaryVariable).equals(Boolean.TRUE)) {
                    return !negated;
                }
            }
        }

        return negated;
    }

    @Override
    public String toString() {
        StringBuilder sb = new StringBuilder();

        if (negated) {
            sb.append("not ");
        }

        sb.append("(");
        String separator = "";

        for (BinaryVariable binaryVariable : binaryVariableList) {
            sb.append(separator);
            separator = " or ";

            if (negatedBinaryVariableSet.contains(binaryVariable)) {
                sb.append("not ");
            }

            sb.append(binaryVariable);
        }

        sb.append(")");
        return sb.toString();
    }

    Set<BinaryVariable> getAllBinaryVariables() {
        return new HashSet<>(binaryVariableList);
    }
}

Formula.java

package net.coderodde.sat;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

/**
 * This class represents a formula in conjuctive normal form (CNF for short).
 * 
 * @author Rodion "rodde" Efremov
 * @version 1.6 (Mar 30, 2017)
 */
public final class Formula {

    /**
     * The list of clauses belonging to this formula.
     */
    private final List<Clause> clauseList = new ArrayList<>();

    /**
     * Adds a clause to this formula.
     * 
     * @param clause the clause to add.
     */
    public void addClause(Clause clause) {
        clauseList.add(clause);
    }

    /**
     * Checks whether the input assignment satisfies the entire formula.
     * 
     * @param assignment the binary variable assignment.
     * @return {@code true} if the assignment satisfies this formula; 
     *         {@code false} otherwise.
     */
    public boolean isSatisfied(Map<BinaryVariable, Boolean> assignment) {
        for (Clause clause : clauseList) {
            if (!clause.isSatisfied(assignment)) {
                return false;
            }
        }

        return true;
    }

    @Override
    public String toString() {
        StringBuilder sb = new StringBuilder("[");
        String separator = "";

        for (Clause clause : clauseList) {
            sb.append(separator);
            separator = " and ";
            sb.append(clause);
        }

        return sb.append("]").toString();
    }

    Set<BinaryVariable> getAllBinaryVariables() {
        Set<BinaryVariable> binaryVariableSet = new HashSet<>();

        for (Clause clause : clauseList) {
            binaryVariableSet.addAll(clause.getAllBinaryVariables());
        }

        return binaryVariableSet;
    }
}

SATSolver.java

package net.coderodde.sat;

import java.util.Map;

public interface SATSolver {

    public Map<BinaryVariable, Boolean> 
        findSatisfyingAssignment(Formula formula);
}

BruteForceSATSolver.java

package net.coderodde.sat;

import java.util.HashMap;
import java.util.Map;
import java.util.Set;

public final class BruteForceSATSolver implements SATSolver {

    @Override
    public Map<BinaryVariable, Boolean> 
        findSatisfyingAssignment(Formula formula) {
        Set<BinaryVariable> binaryVariableSet = formula.getAllBinaryVariables();
        Map<BinaryVariable, Boolean> assignment = 
                createInitialAssignment(binaryVariableSet);
        do {
            if (formula.isSatisfied(assignment)) {
                return assignment;
            }
        } while (assignmentIncremented(assignment));

        return null;
    }

    private Map<BinaryVariable, Boolean> 
        createInitialAssignment(Set<BinaryVariable> binaryVariableSet) {
        Map<BinaryVariable, Boolean> assignment =
                new HashMap<>(binaryVariableSet.size());

        for (BinaryVariable binaryVariable : binaryVariableSet) {
            assignment.put(binaryVariable, Boolean.FALSE);
        }

        return assignment;
    }

    private boolean 
        assignmentIncremented(Map<BinaryVariable, Boolean> assignment) {

        for (Map.Entry<BinaryVariable, Boolean> entry : assignment.entrySet()) {
            if (entry.getValue().equals(Boolean.FALSE)) {
                entry.setValue(Boolean.TRUE);
                return true;
            } else {
                entry.setValue(Boolean.FALSE);
            }
        }

        return false;
    }
}

Demo.java

import java.util.Map;
import net.coderodde.sat.BinaryVariable;
import net.coderodde.sat.BruteForceSATSolver;
import net.coderodde.sat.Clause;
import net.coderodde.sat.Formula;

public class Demo {

    public static void main(String[] args) {
        BinaryVariable var1 = new BinaryVariable(0);
        BinaryVariable var2 = new BinaryVariable(1);
        BinaryVariable var3 = new BinaryVariable(2);

        Clause clause1 = new Clause();
        Clause clause2 = new Clause(true);

        // (not var1 or var2) and not(var2 or not var3)

        clause1.addBinaryVariable(var1, true);
        clause1.addBinaryVariable(var2, false);

        clause2.addBinaryVariable(var2, false);
        clause2.addBinaryVariable(var3, true);

        Formula formula = new Formula();
        formula.addClause(clause1); 
        formula.addClause(clause2);

        System.out.println("Solution to " + formula + " is:");

        Map<BinaryVariable, Boolean> assignment = 
                new BruteForceSATSolver().findSatisfyingAssignment(formula);

        System.out.println(assignment);
    }
}

The output for the above demo is

Solution to [(not x_0 or x_1) and not (x_1 or not x_2)] is:
{x_0=false, x_1=false, x_2=true}

As always, any critique is much appreciated.

Answer 1

First note that in a CNF a clause cannot be negated. This is because a Clause ¬ (A ∨ B) is equal to ¬A ∧ ¬B. But let's ignore this and assume we're talking about a more lenient Formula instead.

Next your BinaryVariable could just as well be a normal String.
Replace all BinaryVariable with String and assign the variables as String var1 = "X_1" and it should still work.

Instead of doing that I suggest to actually put the assignment of the BinaryVariable inside the class. So add a boolean field and some methods and the class looks like this:

public final class BinaryVariable {
    //note: removed redundant comment
    private final int id;

    //not static since the solver will change this assignment
    private boolean assignment = false;

    public BinaryVariable(int id) {
        this.id = id;
    }

    public void setFalse(){
        assignment = false;
    }

    public void setTrue(){
        assignment = true;
    }

    public boolean isTrue(){
        return assignment;
    }

    @Override
    public int hashCode() {...}

    @Override
    public boolean equals(Object o) {...}

    @Override
    public String toString() {
        return "x_" + id;
    }
}

Instead of the methods setTrue() and setFalse() you can also use the method assign(boolean value). This works just as well.

Now your isSatisfied method in the Clause class can be changed to this:

public boolean isSatisfied() {
    for (BinaryVariable binaryVariable : binaryVariableList) {
        if (negatedBinaryVariableSet.contains(binaryVariable)) {
            if (!binaryVariable.isTrue()) {
                return !negated;
            }
        } else {
            if (binaryVariable.isTrue()) {
                return !negated;
            }
        }
    }

    return negated;
}

There's 2 things I still don't like here.
The first is the !binaryVariable.isTrue(). That ! is so easy to miss. This one is just my personal preference but if we can add an isFalse() method to BinaryVariable to make this easier to read.

public boolean isFalse(){
    return !assignment;
}

The next thing I don't like is that we store the negated BinaryVariables in 2 lists. This can be easily improved by removing the positive ones from the binaryVariableList. This requires the following changes in the Clause class:

 /**
 * List of non-negated variables present in this clause.
 */
private final List<BinaryVariable> positiveBinaryVariables = new ArrayList<>();

/**
 * List of negated variables present in this clause.
 */
private final List<BinaryVariable> negatedBinaryVariables = new ArrayList<>();

 /**
 * Adds a non-negated variable to this clause.
 * 
 * @param binaryVariable the variable to add.
 */
public void addBinaryVariable(BinaryVariable binaryVariable) {
    positiveBinaryVariables.add(binaryVariable);
}

/**
 * Adds a negated variable to this clause.
 */
public void addNegatedBinaryVariable(BinaryVariable binaryVariable) {
    negatedBinaryVariableSet.add(binaryVariable);
}

public boolean isSatisfied() {
    for (BinaryVariable binaryVariable : negatedBinaryVariables) {
        if (binaryVariable.isFalse()) {
            return !negated;
        }
    }
    for(BinaryVariable binaryVariable : positiveBinaryVariables) {
        if (binaryVariable.isTrue()) {
            return !negated;
        }
    }
    return negated;
}

public Set<BinaryVariable> getAllBinaryVariables() {
    Set<BinaryVariable> result = new HashSet<>();
    result.addAll(positiveBinaryVariables);
    result.addAll(negatedBinaryVariables);
    return result;
}

I also think that you had a bug for the clause A ∧ (A ∨ ¬A).

Notice that I also changed this:

clause1.addBinaryVariable(var1, true);
clause1.addBinaryVariable(var2, false);

to

clause1.addNegatedBinaryVariable(var1);
clause1.addPostivieBinaryVariable(var2);

which I think is a lot less confusing.

That same confusion happens in

Clause clause1 = new Clause();
Clause clause2 = new Clause(true);

Which of these corresponds to the ¬ clause?

Let's add a method to Clause to fix this

public static Clause newNegatedClause(){
    return new Clause(true);
}

and for consistency sake also:

public static Clause newNormalClause(){
    return new Clause(false);
}

now the public Clause() constructor can be removed and the other one can be made private since we no longer use it from outside the class.
The clause assignments then turn into:

Clause clause1 = Clause.newNormalClause();
Clause clause2 = Clause.newNegatedClause();

Which I think are less confusing

Now the only thing left is to update the solver to use the internal assignments of the BinaryVariables.

public final class BruteForceSATSolver implements SATSolver {
    @Override
    public boolean findSatisfyingAssignment(Formula formula){
        Set<BinaryVariable> binaryVariableSet = formula.getAllBinaryVariables();
        do{
            if(formula.isSatisfied()) {
                return true;
        } while(assignmentIncremented(binaryVariableSet));

        return false;
    }

    private boolean assignmentIncremented(binaryVariableSet){
        for(BinaryVariable var : binaryVariableSet){
            if(var.isFalse()){
                var.setTrue();
                return true;
            } else {
                var.setFalse();
            }
        }
        return false;
    }
}

Notice how we no longer need the initialisation here? Since we put the variable assignment to false by default.

I also changed the return type to a boolean to show if a solution is found or not.

This does mean that we can no longer just print the map like you did before to show what assignments we made. Instead we need to loop over them:

for(BinaryVariable var : formula.getAllBinaryVariables()){
    System.out.println(var + " = " + var.getAssignment());
}

I believe this change also has the fun side effect that if a formula has more than one solution you can find it by running assignmentIncremented(formula.getAllBinaryVariables())and then findSatisfyingAssignment(formula) again. (need to make that increment method public though).

---

DISCLAIMER: I did not actually try any of the code in this post. So you might have to make some minor changes to actually make it run correctly. Most of it should work though.