Improved brute force SAT solver in Java

Question

(See the previous 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.

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

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

which is (along other possible assignments) \$(x_0, x_1, x_2) = (0, 0, 0).\$

Now I have incorporated all the good points stated by Imus, and I have this:

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 implements Comparable<BinaryVariable> {

    private final int id;
    private boolean assignment = false;

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

    public void setFalse() {
        this.assignment = false;
    }

    public void setTrue() {
        this.assignment = true;
    }

    public void setAssignment(boolean assignment) {
        this.assignment = assignment;
    }

    public boolean isFalse() {
        return assignment == false;
    }

    public boolean isTrue() {
        return assignment == true;
    }

    public boolean getAssignment() {
        return assignment;
    }

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

    @Override
    public int compareTo(BinaryVariable o) {
        return Integer.compare(id, o.id);
    }
}

Clause.java

package net.coderodde.sat;

import java.util.Set;
import java.util.TreeSet;

/**
 * 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 {

    /**
     * The set of variables present in this clause.
     */
    private final Set<BinaryVariable> positiveBinaryVariableSet = 
            new TreeSet<>();

    /**
     * The set of negated variables in this clause.
     */
    private final Set<BinaryVariable> negatedBinaryVariableSet = 
            new TreeSet<>();

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

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

    /**
     * Checks whether the input assignment satisfies this clause.
     * 
     * @return {@code true} if the assignment satisfies this clause, and 
     *         {@code false} otherwise.
     */
    public boolean isSatisfied() {
        for (BinaryVariable positiveBinaryVariable : 
                positiveBinaryVariableSet) {
            if (positiveBinaryVariable.isTrue()) {
                return true;
            }
        }

        for (BinaryVariable negativeBinaryVariable :
                negatedBinaryVariableSet) {
            if (negativeBinaryVariable.isFalse()) {
                return true;
            }
        }

        return false;
    }

    @Override
    public String toString() {
        StringBuilder sb = new StringBuilder();
        Set<BinaryVariable> allBinaryVariables = 
                new TreeSet<>(positiveBinaryVariableSet);

        allBinaryVariables.addAll(negatedBinaryVariableSet);

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

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

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

            sb.append(binaryVariable);
        }

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

    Set<BinaryVariable> getBinaryVariableSet() {
        Set<BinaryVariable> binaryVariableSet = 
                new TreeSet<>(positiveBinaryVariableSet);
        binaryVariableSet.addAll(negatedBinaryVariableSet);
        return binaryVariableSet;
    }
}

Formula.java

package net.coderodde.sat;

import java.util.ArrayList;
import java.util.List;
import java.util.Set;
import java.util.TreeSet;

/**
 * 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.
     * 
     * @return {@code true} if the assignment satisfies this formula; 
     *         {@code false} otherwise.
     */
    public boolean isSatisfied() {
        for (Clause clause : clauseList) {
            if (!clause.isSatisfied()) {
                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();
    }

    List<BinaryVariable> getAllBinaryVariablesAsList() {
        Set<BinaryVariable> binaryVariableSet = new TreeSet<>();

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

        return new ArrayList<>(binaryVariableSet);
    }
}

SATSolver.java

package net.coderodde.sat;

public interface SATSolver {

    public boolean findNextSatisfyingAssignment();
}

BruteForceSATSolver.java

package net.coderodde.sat;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

public final class BruteForceSATSolver implements SATSolver {

    private boolean searchExceeded = false;
    private final Formula formula;
    private final List<BinaryVariable> binaryVariableList = new ArrayList<>();
    private final Map<BinaryVariable, Boolean> previousState = new HashMap<>();

    public BruteForceSATSolver(Formula formula) {
        this.formula = formula;
        this.binaryVariableList.addAll(formula.getAllBinaryVariablesAsList());
        getInitialState();
    }

    @Override
    public boolean findNextSatisfyingAssignment() {
        if (searchExceeded) {
            return false;
        }

        restoreState();

        do {
            if (formula.isSatisfied()) {
                saveState();
                incrementSavedState();

                if (isFirstState()) {
                    // Once here, we have tried all possible assignments to the
                    // binary variables. Mark the state as "exhausted":
                    searchExceeded = true;
                    return true;
                }

                return true;
            }
        } while (assignmentIncremented());

        searchExceeded = true;
        return false;
    }

    private boolean isFirstState() {
        for (BinaryVariable binaryVariable : binaryVariableList) {
            if (previousState.get(binaryVariable)) {
                return false;
            }
        }

        return true;
    }

    private boolean assignmentIncremented() {
        for (BinaryVariable binaryVariable : binaryVariableList) {
            if (binaryVariable.isFalse()) {
                binaryVariable.setTrue();
                return true;
            } else {
                binaryVariable.setFalse();
            }
        }

        return false;
    }

    private void incrementSavedState() {
        for (BinaryVariable binaryVariable : binaryVariableList) {
            if (binaryVariable.isFalse()) {
                previousState.put(binaryVariable, Boolean.TRUE);
                return;
            } else {
                previousState.put(binaryVariable, Boolean.FALSE);
            }
        }
    }

    private void getInitialState() {
        for (BinaryVariable binaryVariable : binaryVariableList) {
            previousState.put(binaryVariable, Boolean.FALSE);
        }
    }

    private void saveState() {
        for (BinaryVariable binaryVariable : binaryVariableList) {
            previousState.put(binaryVariable, binaryVariable.getAssignment());
        }
    }

    private void restoreState() {
        for (Map.Entry<BinaryVariable, Boolean> entry 
                : previousState.entrySet()) {
            entry.getKey().setAssignment(entry.getValue());
        }
    }
}

Demo.java

import net.coderodde.sat.BinaryVariable;
import net.coderodde.sat.BruteForceSATSolver;
import net.coderodde.sat.Clause;
import net.coderodde.sat.Formula;
import net.coderodde.sat.SATSolver;

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

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

        clause2.addNegatedBinaryVariable(var1);
        clause2.addPositiveBinaryVariable(var3);

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

        System.out.println("Solution(s) to " + formula + " is/are:");
        SATSolver solver = new BruteForceSATSolver(formula);
        BinaryVariable[] variableArray = { var1, var2, var3 };

        while (solver.findNextSatisfyingAssignment()) {
            System.out.println(toAssignmentString(variableArray));
        }


        solver.findNextSatisfyingAssignment();
    }

    private static String 
        toAssignmentString(BinaryVariable... binaryVariableArray) {
        StringBuilder sb = new StringBuilder();
        String separator = "";

        for (BinaryVariable binaryVariable : binaryVariableArray) {
            sb.append(separator);
            separator = ", ";
            sb.append(binaryVariable.toString())
              .append(" = ")
              .append(binaryVariable.getAssignment());
        }

        return sb.toString();
    }
}

For the formula \$(x_0 \vee \neg x_1) \wedge (\neg x_0 \vee x_2)\$ I get the output:

Solution(s) to [(x_0 or not x_1) and (not x_0 or x_2)] is/are:
x_0 = false, x_1 = false, x_2 = false
x_0 = false, x_1 = false, x_2 = true
x_0 = true, x_1 = false, x_2 = true
x_0 = true, x_1 = true, x_2 = true

Critique request

As always, tell me anything that comes to mind.

Answer 1

Overall it looks great. I like how you implemented comparable to make use of the implicit sorting in a TreeSet.

I see you also corrected the formula to really be in CNF now.

I also like that you added a helper method to print the assignment:

System.out.println(toAssignmentString(variableArray));

A small suggestion here is to change that helper function to directly print it. So your call looks like:

while (solver.findNextSatisfyingAssignment()) {
    printAssignmen(variableArray));
}

Not that it was wrong by any means though.

You now have both isTrue() / isFalse() and getAssignment(). Not what I had in mind and I was a bit surprised to see this, wondering if I worded it wrong in my suggestion on the previous iteration. Then I noticed you're using them all, so it seems worth it here.

---

There is only 1 thing in your code that I don't understand. And I believe I'm also (at least partially) the one responsible for this. That is the choice to keep the previousState.

I believe the reasoning behind this is that between calls you don't know if someone else might have changed the assignments to the variables and you feel responsible to ensure the state is back to where you left it after the previous search.

Instead of enforcing this from inside the class you can also comment on how the solver is supposed to work. And put the responsibility of having the correct state on the one using this class, instead of inside the class itself.

Adding a bit of documentation might have been enough to solve most of your problems (and make the entire state saving inside the solver obsolete).

/**
* This solver assumes all variables start with assignment false.
* Then it tries to change the variables in order until a solution is found,
* or if they're all back to false, indicating the end of a full search.
*/

Now we can remove the saved state from the solver and make it it's sole responsibility of searching for the next valid state.

But first let me put some pointers in your findNextSatisfyingAssignment() method to point to some weird choices. I'll number them so I can adress them below.

public boolean findNextSatisfyingAssignment() {
    if (searchExceeded) { <- (1) Why the word Exceeded?
        return false;
    }

    restoreState(); <- (2.1) not my responsibility

    do {
        if (formula.isSatisfied()) {
            saveState(); <- (2.2) Still not my responsibility
            incrementSavedState(); <- (3) increment saved state instead of current?

            if (isFirstState()) { <- (4) ending condition
                // Once here, we have tried all possible assignments to the
                // binary variables. Mark the state as "exhausted":
                searchExceeded = true;
                return true; <- (5) remove this line, works exactly the same
            }

            return true;
        }
    } while (assignmentIncremented());

    searchExceeded = true;
    return false;
}

Point (1): The name searchExceeded. I'm not native english myself so I had to look up the meaning of "exceeded" to know if I'm missing an interpretation. But it only confirmed that it doesn't exactly cover what you mean here. I believe "searchExhausted" is a bit better, but the entire variable becomes obsolete with the comment block I suggested. We stop searching if all variables are looped back to false. If you call the next search after that, this class will just assume it to be the first time and start searching from the start again. Nothing wrong with that :)

Point (2): Restoring and saving previous state is no longer the responsibility of this class. It could still be useful though, but I would put it into it's own class instead. (I'll come back to this later).

Point (3): Now this doesn't feel right at all. The variable previousState sounds like a backup of a previous state that you can restore if needed. Here you abuse it to make sure your while loop doesn't get stuck when calling the method again after a succesful search. This feels more like a hack than a solution.

Point (5): whether or not isFirstState() was true or not, we will return true. No need to put it inside the if as well. We can just go out of the if and then return true below.

Point (4): No no, I didn't forget this one, I'm just going to need some more room for it, so I kept it for last.
This actually reeds as:

if(previousState only contains false){
    mark as nothing left to find
}

As I suggested earlier I want the ending condition to be:

if(current variables are all assigned to false){
    stop searching and return
}

We know that the findNextSatisfyingAssignment() will return false and end the while loop when all variables are assigned to false. So we don't need to check for it explicitly inside the loop. There is only one edge case we need to take care of. Since I'm planning to increment first when entering the findNext... we didn't check if the starting state (everything false) was actually a solution yet. But we can do so after the while loop.

My suggested implementation becomes:

@Override
public boolean findNextSatisfyingAssignment() {
    while (incrementAssignment()){
        if (formula.isSatisfied()) {
            return true;
        }
    }
    //Loop ended with all variables assigned false, 
    //this might still be a valid solution.
    return formula.isSatisfied();
}

This almost looks too simple to be true, doesn't it?

Notice that I also changed the name of assignmentIncremented() to incrementAssignment(). This is because assignmentIncremented() sounds too much like it's a boolean getter. Similar to isIncremented(). Convention says that getters do not change state. The name incrementAssignment() clearly states that the assignment will be incremented by that method. It just also conveniently returns a boolean to know if it was succesful or not.

---

The last thing I promissed was to get back to saving the state. I don't think we need it but won't deny that it can be useful.

Instead of forcing it inside the solver class I would put it in it's own class. One that takes a list of variables and saves them as a state. This state can then later be used to return the variables to the assignment they had when the state was saved.

The class will look something like this:

public class SaveState {
    Map<BinaryVariable,Boolean> state = new HashMap<BinaryVariable, Boolean>();

    public SaveState(BinaryVariable... variables){
        for(BinaryVariable var : variables){
            state.put(var, var.getAssignment();
        }
    }

    public void restoreToThisState(){
        //first attempt at java 8 without IDE. Correct syntax if needed.
        state.foreach((var, assignment) -> var.setAssignment(assignment));
    }
}

How and when to use it I'll leave up to you. As I said, for your current solver I don't think saving the state is needed :)