-1
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Are you interested in checking the satisfiability of your constraints? Are the values of "ind" all mutually exclusive? $\endgroup$ – Fabio Somenzi Dec 10 '16 at 16:13
  • $\begingroup$ @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. $\endgroup$ – ssdimmanuel Dec 10 '16 at 16:18
  • $\begingroup$ 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. $\endgroup$ – Fabio Somenzi Dec 10 '16 at 16:21
  • $\begingroup$ 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) $\endgroup$ – ssdimmanuel Dec 10 '16 at 16:22
  • $\begingroup$ 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. $\endgroup$ – Fabio Somenzi Dec 10 '16 at 16:33
0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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 ? $\endgroup$ – ssdimmanuel Dec 11 '16 at 14:34
  • $\begingroup$ 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. $\endgroup$ – Fabio Somenzi Dec 11 '16 at 15:12
  • $\begingroup$ Thanks for your suggestions. Would the expressions in my question fall under "First order logic" or am I stating it wrong ? $\endgroup$ – ssdimmanuel Dec 13 '16 at 12:32
  • $\begingroup$ Yes, that's correct. $\endgroup$ – Fabio Somenzi Dec 13 '16 at 15:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.