replaced http://codereview.stackexchange.com/ with https://codereview.stackexchange.com/
(See the previous iteration previous iteration.)
Now I have incorporated all the good points stated by Imus Imus, and I have this:
(See the previous iteration.)
Now I have incorporated all the good points stated by Imus, and I have this:
(See the previous iteration.)
Now I have incorporated all the good points stated by Imus, and I have this:
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).\$
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).\$
Improved brute force SAT solver in Java
(See the previous iteration.)
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.
lang-java