Represent a business rule as a constraint model to find the solution set

Question

In my enterprise application I have business rules like :

1. ((AMOUNT < 20000.00) || ((AMOUNT >= 20000.00) && (RISKEXPOSURE == 'N')))
2. (ind = A1 || ind = A2 || ind = A3 || ind = S1 || ind = S2 || ind = S9)

The rule, as you can see, is made of business expressions ex: (AMOUNT < 20000.00). The rules could have any number of business conditions joined by boolean operators && and ||. The identifiers AMOUNT, RISKEXPOSURE and ind are the business variables (which could vary from 1 to n based on the business domain).

My requirement is to find those expressions when true make the entire rule true. For ex: for business rule #1 - the whole rule will be true if: (AMOUNT < 20000.00) is true or ((AMOUNT >= 20000.00) && (RISKEXPOSURE == 'N')) is true hence my output should be:

Solution #1: (AMOUNT < 20000.00)

Solution #2: ((AMOUNT >= 20000.00) && (RISKEXPOSURE == 'N'))

Similarly for Business rule #2:

Solution #1:ind = A1

Solution #2:ind = A2

Solution #3:ind = A3

Solution #4:ind = S1

Solution #5:ind = S2

Solution #6:ind = S9

---

What I tried:

Since each business expression can be either true or false, I changed my business rule #1 as (A || ( B && C ) ). I used the propositional logic library from Tweetyproject. This gives me results but I cannot enforce a constraint such as an XOR. In my example A and B are mutually exclusive but my output possible results. Representing the rule in truth table form, I get all the following true conditions

011 ,100 ,101 ,110 ,111

However my result should be only 100, 011

This lead me to look for alternatives and the answer here suggested a constraint solver. I have been reading about the Choco Solver. But I am not sure how my business rule can be represented in a model acceptable by the solver. Any help is greatly appreciated.

Answer 1

Simple solution can be to implement algorithm which find all combinations of boolean values of a given size. Then for each expression calculate the entire expression by the values in combination and the opposite value of your expression. If in every combination the whole expression calculation with the values in the combination row and with the opposite value for your expressions are different, the this expression is this which you need. I will try to explain it easily.

You have expression (A || ( B && C ) )= BIG Then you find combinations of possible values: e.g

[[001],[010],[011]...[111]]

For each of them replace the values in to your BIG expression and compare the result the expression calculated by the opposite value of expression you want - [101] with [001] | [110] with [010] and for each combinations the result is difference you find the expression. Then switch to next index and do this again

Answer 2

I would recommend you to look at SMT solving. It naturally allows solving the stated problem. You introduce any reasonable amount of constraints (both integer and Boolean) and variables. Basically, it tries to satisfy an equation given some constraints. It will find first satisfying assignment to your task.

Links to explore:

1. Z3
2. CVC4
3. yices2

Be aware that runtime and performance are heavily dependant on the problem itself: constraints, constants, exact values.