I’ve worked on a couple projects recently where I needed to be able to do some lightweight propositional expression manipulation in Java. Specifically, I wanted to be able to:

- Let a user input simple logical expressions, and parse them into Java data structures
- Evaluate the truth of the statement given values for each variable
- Incrementally update the expression as values are assigned to the variables
- If the statement given some variable assignments is not definitively true or false, show which terms remain.
- Perform basic simplification of redundant terms (full satisfiability is of course NP hard, so this would only include basic simplification)

I couldn’t find a Java library which made this particularly easy; a couple stackoverflow questions I found didn’t have any particularly easy solutions. I decided to take a shot at implementing a basic library. The result is on GitHub as the jbool_expressions library.

(most of the rest of this is copied from the README, so feel free to read it there.)

Using the library, a basic propositional expression is built out of the types *And, Or, Not, Variable* and *Literal*. All of these extend the base type *Expression*. An *Expression* can be built programatically:

Expression expr = And.of(
Variable.of("A"),
Variable.of("B"),
Or.of(Variable.of("C"), Not.of(Variable.of("C"))));
System.out.println(expr);

or by parsing a string:

Expression expr =
ExprParser.parse("( ( (! C) | C) & A & B)");
System.out.println(expr);

The expression is the same either way:

((!C | C) & A & B)

We can do some basic simplification to eliminate the redundant terms:

Expression simplified = RuleSet.simplify(expr);
System.out.println(expr);

to see the redundant terms are simplified to “true”:

(A & B)

We can assign a value to one of the variables, and see that the expression is simplified after assigning “A” a value:

Expression halfAssigned = RuleSet.assign(
simplified,
Collections.singletonMap("A", true)
);
System.out.println(halfAssigned);

We can see the remaining expression:

B

If we assign a value to the remaining variable, we can see the expression evaluate to a literal:

Expression resolved = RuleSet.assign(
halfAssigned,
Collections.singletonMap("B", true)
);
System.out.println(resolved);

true

All expressions are immutable (we got a new expression back each time we performed an operation), so we can see that the original expression is unmodified:

System.out.println(expr);

((!C | C) & A & B)

Expressions can also be converted to sum-of-products form:

Expression nonStandard = PrefixParser.parse(
"(* (+ A B) (+ C D))"
);
System.out.println(nonStandard);
Expression sopForm = RuleSet.toSop(nonStandard);
System.out.println(sopForm);

((A | B) & (C | D))
((A & C) | (A & D) | (B & C) | (B & D))

You can build the library yourself or grab it via maven:

<dependency>
<groupId>com.bpodgursky</groupId>
<artifactId>jbool_expressions</artifactId>
<version>1.3</version>
</dependency>

Happy to hear any feedback / bugs / improvements etc. I’d also be interested in hearing how other people have dealt with this problem, and if there are any better libraries out there.