Convert Business conditions to Boolean expressions

Question

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

Answer 1

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.