# Convert Business conditions to Boolean expressions

In my enterprise application I have business rules like :

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

Now expression #1 can be converted to a boolean expression like: (X || (!X && Y))

But I am not sure how the second expression be denoted in boolean form:

can it be like below ? : (A || B || C || D || E || F). I want to keep the number of variables as less as possible for me feed it to a boolean solver and get results quicker

• Are you interested in checking the satisfiability of your constraints? Are the values of "ind" all mutually exclusive? – Fabio Somenzi Dec 10 '16 at 16:13
• @FabioSomenzi yes I would like check the satisfiability as well. But before that need to understand how the real world business condition can be represented in the form I mentioned. And yes ind has mutually exclusive values. – ssdimmanuel Dec 10 '16 at 16:18
• In all likelihood, you want an SMT solver, rather than a Boolean satisfiability solver. Satisfiability Modulo Theories is a fancy name, and those tools are very sophisticated, but in a nutshell, they allow you to detect that $x < 10 \wedge x > 15$ cannot be satisfied. At the propositional level, $p \wedge q$ doesn't express the same condition. – Fabio Somenzi Dec 10 '16 at 16:21
• As a last step I will be checking the satisfiability of the expression preferably using a Java library (there are lots of open source libraries available) – ssdimmanuel Dec 10 '16 at 16:22
• Some SMT solvers have Java bindings. Z3 and CVC4 offer Java APIs and both are the real deal. You know your application and I don't, and it well may be that integrating a heavy piece of machinery like a full-fledged SMT solver is not viable, but I'll reiterate that propositional logic is the wrong tool for the talk you describe. Both Z3 and CVC4 have web-based interfaces that allow you to familiarize with them. – Fabio Somenzi Dec 10 '16 at 16:33

SMT solvers allow one to reason with logical combinations of arithmetic statements. Z3 has the most flexible web-based interface, with a few extensions on the standard SMT-LIB 2 format that make the task of modeling your query easier. So, I'll show what one can enter here to model and reason about yor query.

;; Trace subset of unsatisfiable constraints
(set-option :produce-unsat-cores true)

;; Declare enumerated types.
(declare-datatypes () ((Risk None Low Medium High)))
(declare-datatypes () ((Index A1 A2 A3 S1 S2 S3 S4 S5 S6 S7 S8 S9)))

;; Declare the constant symbols of our model.
(declare-const amount Real)
(declare-const risklevel Risk)
(declare-const ind Index)

;; Assert constraints on the model.  Named constraints can be traced.
(assert (! (or (< amount 20000) (and (<= 20000 amount) (= risklevel None)))
:named norisk))
(assert (! (or
(= ind A1) (= ind A2) (= ind A3)
(= ind S1) (= ind S2) (= ind S9)) :named rightindex))

;; Sanity check: Are the constraints satisfiable?
(check-sat) ; expect 'sat'
;; See if we can simplify one of the constraints. (Not much.)
(simplify (or (< amount 20000) (and (<= 20000 amount) (= risklevel None))))
;; Get values of amount, risklevel, and ind that witness satisfiability.
(get-value (amount risklevel ind))

;; Start new context.
(push)
;; Do these choices satisfy the constraints?
(assert (! (and (= amount 100000) (= risklevel Medium)) :named example))
(check-sat) ; expect 'unsat'
;; Get explanation.
(get-unsat-core)
(pop)
;; We can now check another example or simply say, 'That's all, folks!'
(exit)


Running Z3 on this input produces:

sat
(or (not (<= 20000.0 amount)) (and (<= 20000.0 amount) (= risklevel None)))
((amount 20000.0) (risklevel None) (ind A1))
unsat
(norisk example)


The last line says that the unsatisfiability of the constraints depends on a conflict between the norisk and example constraints. The rightindex constraint has nothing to do with it.

• Thanks for the answer. But on my part it would be a steep learning curve. Also I would like to implement a lightweight SMT solver. any pointers ? – ssdimmanuel Dec 11 '16 at 14:34
• If you only need to deal with conjunctions (AND) of simple arithmetic constraints, you may be able to make do with a solver for "difference logic," which in its simplest form amounts to the Bellman-Ford algorithm for shortest paths. A very accessible exposition is in Cormen, Leiserson, Rivest, and Stein. (Look for "difference constraints and shortest paths.") You could then deal with disjunctions (OR) by enumeration of the possibilities. – Fabio Somenzi Dec 11 '16 at 15:12
• Thanks for your suggestions. Would the expressions in my question fall under "First order logic" or am I stating it wrong ? – ssdimmanuel Dec 13 '16 at 12:32
• Yes, that's correct. – Fabio Somenzi Dec 13 '16 at 15:53