BAT
Bit-level Analysis Tool, version 2

BAT Examples

The following are two simple examples to help you get the basic idea on how to define and solve problems using BAT. Many more complicated examples can be found on our benchmarks page.

ALU

The BAT input file for this example can be found here. 

((:functions
  (maj (1) ((a 1) (b 1) (c 1))
       (or (and a b)
	   (and b c)
	   (and a c)))
  (fa (2) ((a 1) (b 1) (cin 1))
      (cat (maj a b cin)
	   (xor a b cin)))
  (mux-4 (1) ((in0 1) (in1 1) (in2 1) (in3 1) (sel 2))
	 (local ((nsel0 (not (sel 0)))
		 (nsel1 (not (sel 1))))
		(or (and in0 nsel0 nsel1)
		    (and in1 (sel 0) nsel1)
		    (and in2 nsel0 (sel 1))
		    (and in3 (sel 0) (sel 1)))))
  (alu-slice (2) ((a 1) (b 1) (cin 1) (bnegate 1) (op 2))
	     (local ((nb (xor bnegate b))
		     (res0 (and a nb))
		     (res1 (or a nb))
		     (((cout 1) (res2 1)) (fa a nb cin)))
		    (cat cout
			 (mux-4 res0 res1 res2 1u op))))
  (alu-2-bit (4) ((a 2) (b 2) (bnegate 1) (op 2))
	     (local ((c 2))
		    (((t0 (c 0))
		      (alu-slice (a 0) (b 0) bnegate bnegate op))
		     ((t1 (c 1))
		      (alu-slice (a 1) (b 1) t0 bnegate op))
		     (zero (= c 0)))
		    (cat t1 c zero))))
 (:vars (i1 2) (i2 2) (bn 1) (op 2) (out 2) (cout 1) (zero 1))
 (:init (and (= out 0)
	     (= cout 1b1)
	     (= zero 1b0)))
 (:trans (= (cat (next cout)
		 (next out)
		 (next zero))
	    (alu-2-bit i1 i2 bn op)))
 (:spec (AG (<-> zero (not cout)))))

This example describes an ALU. We cover pieces of this code in the documentation. The functions section takes a list of function definitions. In this example, we define 5 functions. A function definition starts with the function name. Our first function is called maj. The second element in the definition is the type. This is a list containing 1 positive integer for a bit vector function (maj, for example returns a 1-bit bit vector), 2 positive integers if the return type is a memory, and a list of 1 integer lists and 2 integer lists if there are multiple values returned. For example ((1) (8 4)) would specify that the function returns a 1-bit bit vector and a memory with 8 4-bit words.

The third part of a function definition is its arguments. This is just a list of variable definitions just like the ones in the :vars section. In the case of maj, the inputs are 3 1-bit bit vectors, a, b, and c. The final element of a function definition is the body. Its return type must be compatible with that of the function.

In our example, the maj function calculates the majority function on the inputs, fa is a full adder that returns the carry out bit and the sum bit, alu-slice is a 1-bit piece of the alu, and alu-2-bit is the 2-bit alu constructed out of the alu slices. The :vars section includes inputs i1 and i2, an output out, the negation bit (whether i2 should be negated in the case of addition), the operation code, the carry out bit, and the zero bit. The :init specifies that initial states must have an out of 0, a cout of 1, and a zero of 0. The transition relation sets the next values of cout, out, and zero according to the outputs of the alu-2-bit function. The :spec checks that zero is true if and only if cout is not.

Two Stage Pipeline Machine

The BAT input file for this example can be found here.

We now present an example of a 2-bit 2 stage pipeline machine. In the machine spec, we give definitions for the ISA and RTL level models of the 2 stage pipelined machine, and we check that the pipelined machine refines the ISA machine. We will formulate this as a :forall problem. That is, we will present BAT with a formula over a given set of user-defined functions and variables and ask BAT to determine if it is true for all inputs. Let's start with the variable definitions: 

((mastate 7) (rf 4 2) (imem 4 7))

We briefly walk through this example. The machine state is represented by 3 variables, declared in the :vars section: mastate, rf, and imem. The varaiable mastate represents most pieces of the state concatenated together, including the program counter. The register file is represented by rf and the instruction memory is imem. Now let's look at the functions.

((getppc (2) ((mastate 7))
	 (bits mastate 0 1))
 (getewdest (2) ((mastate 7))
	    (bits mastate 2 3))
 (getewresult (2) ((mastate 7))
	      (bits mastate 4 5))
 (getewregwrite (1) ((mastate 7))
		(bits mastate 6 6))
 (src1 (2) ((inst 7))
       (bits inst 5 6))
 (src2 (2) ((inst 7))
       (bits inst 3 4))
 (dest (2) ((inst 7))
       (bits inst 1 2))
 (getregwrite (1) ((inst 7))
	      (bits inst 0 0))
 (nextspc (2) ((pc 2))
	  (bits (+ pc 1u) 0 1))
 (nextsrf (4 2) ((inst 7) (regwrite 1) (rf 4 2) (result 2))
	  (if regwrite
	      (set rf (dest inst) result)
	    rf))
 (step-isa ((2) (4 2) (4 7))
	   ((pc 2) (rf 4 2) (imem 4 7))
	   (local ((inst (get imem pc))
		   (regwrite (getregwrite inst))
		   (arg1 (get rf (src1 inst)))
		   (arg2 (get rf (src2 inst)))
		   (result (bits (+ arg1 arg2) 0 1)))
		  (mv (nextspc pc)
		      (nextsrf inst regwrite rf result)
		      imem)))
 (nextppc (2) ((pc 2)) (bits (+ pc 1u) 0 1))
 (nextprf (4 2) ((rf 4 2) (ewregwrite 1) (ewresult 2) (ewdest 2))
	  (if ewregwrite
	      (set rf ewdest ewresult)
	    rf))
 (step-ma ((7) (4 2) (4 7))
	  ((mastate 7) (rf 4 2) (imem 4 7))
	  (local ((ppc (getppc mastate)) (ewdest (getewdest mastate))
		  (ewregwrite (getewregwrite mastate))
		  (ewresult (getewresult mastate)) (inst (get imem ppc))
		  (arg1_tmp (get rf (src1 inst)))
		  (arg2_tmp (get rf (src2 inst)))
		  (arg1 (if (and ewregwrite (= ewdest (src1 inst)))
			    ewresult
			  arg1_tmp))
		  (arg2 (if (and ewregwrite (= ewdest (src2 inst)))
			    ewresult
			  arg2_tmp))
		  (result (bits (+ arg1 arg2) 0 1)))
		 (mv (cat (getregwrite inst)
			  result
			  (dest inst)
			  (nextppc ppc))
		     (nextprf rf ewregwrite ewresult ewdest)
		     imem)))
 (flush-ma ((7) (4 2) (4 7))
	   ((mastate 7) (rf 4 2) (imem 4 7))
	   (local
	    ((ppc (getppc mastate))
	     (ewdest (getewdest mastate))
	     (ewregwrite (getewregwrite mastate))
	     (ewresult (getewresult mastate))
	     (inst (get imem ppc))
	     (arg1_tmp (get rf (src1 inst)))
	     (arg2_tmp (get rf (src2 inst)))
	     (arg1
	      (if (and ewregwrite (= ewdest (src1 inst)))
		  ewresult
		arg1_tmp))
	     (arg2
	      (if (and ewregwrite (= ewdest (src2 inst)))
		  ewresult
		arg2_tmp))
	     (result (bits (+ arg1 arg2) 0 1)))
	    (mv (cat 1b0 result (dest inst) ppc)
		(nextprf rf ewregwrite ewresult ewdest)
		imem))))

The first 4 functions simply access the pieces of the mastate. For example, getppc gets the program counter, which are in bits 0 to 1 of the mastate. The next 4 functions are used to decode an instruction. They take the instruction as input and produce the source and destination addresses and a control signal that indicates if the instruction should update the register file.

The nextspc and nextsrf show how to update the pc and rf for the ISA model. The step-isa function steps the ISA model. It takes the pc, register file, and instruction memory, and returns the new pc, register file, and instruction memory. Using the local construct, it sets the variable inst to be instruction at the address pointed to by the pc. The regwrite variable is set to the appropriate piece of the instruction. The two arguments are fetched from the rf according to the addresses given in the instruction. The result is just set to the sum of the two arguments (with the high bit chopped off). Finally, the new pc, new rf, and the imem are returned using mv.

The next 3 functions describe how the RTL model is stepped. The step-ma function takes in the mastate, rf, and imem, and returns the new values for each. Its behavior is similar to that of the step-isa function. It gets the pieces of the mastate, loads the appropriate instruction and input values and computes the new values for each piece of the state.

Finally, we have a function that is very similar to the step-ma function, called flush-ma. This function is used to flush an MA state by completing the partially executed instruction in the pipeline latch without fetching any new instruction. Finally, here is the formula we want to check:

(local (((w1 s-rf s-imem) (flush-ma mastate rf imem)) (s-pc (getppc w1))
	((u-pc u-rf u-imem) (step-isa s-pc s-rf s-imem))
	((v v-rf v-imem) (step-ma mastate rf imem))
	((v1 v1-rf v1-imem) (flush-ma v v-rf v-imem)))
       (and (= (getppc v1) u-pc) (= v1-rf u-rf)))

We set w1, s-rf, and s-imem to be the result of flushing the RTL machine in its initial state. Then s-pc is set to the pc out of w1. This gives us all the pieces of the ISA state -- s-pc, s-rf, and s-imem -- that correspond to the current RTL state. Next, u-pc, u-rf, and u-imem are declared to be the result of stepping the current ISA state.

We then step the original RTL machine and flush again, giving us v1, v1-rf, and v1-imem. We then check that the pc of v1 is equal to u-pc and that v1-rf is equal to u-rf.

Decimal Counter

The following example is a BAT model of a 2 digit decimal counter. The model describes the circuit for incrementing the decimal counter. Each digit of the decimal counter is represented using a 4-bit unsigned bit-vector. A valid value of a 4-bit unsigned bit-vector representing a digit can only range between 0 and 9. The property checked is that if each of the digits of the decimal counter are valid, then the digits should remain valid after the decimal counter is incremented. 


:forall

((x 8)) 

((inc4 ((4) (1)) ((x 4))
  (local ((xu (cat 0b0 x)))
   (if (< xu 9) (mv (mod+ x 1) 0b0) (mv 0 0b1))))
 
 (inc_digit ((4) (1)) ((x 4) (c 1)) (if c (inc4 x) (mv x 0b0)))
 
 (valid_digits (1) ((x 8))
  (and (< (cat 0b0 (bits x 0 3)) 10) (< (cat 0b0 (bits x 4 7)) 10)))
 
 (inc_digits (8) ((x 8))
  (local
   ((((x0 4) (c0 1)) (inc4 (bits x 0 3)))
    (((x1 4) (c1 1)) (inc_digit (bits x 4 7) c0)))
   (cat x1 x0)))) 


(-> (valid_digits x) (valid_digits (inc_digits x)))

The state of the decimal counter is represented by a variable x, which is a bit vector of size 8. Each decimal digit is represented using 4 bits. The lower four bits of x and the higher four bits of x represent the first and the second digit of the decimal counter, respectively. 

((x 8))

The BAT functions used to model the circuit that increments the decimal counter is described next. The inc4 function increments a digit represented using a 4-bit bit-vector and returns two values that include the incremented digit and a carry bit. If the value of the input digit is less than 9, then inc4 returns an incremented digit and a carry bit with value 0. If the value of the input digit is not less than 9, then inc4 returns a digit with value 0 and a carry bit with value 1. 

(inc4 ((4) (1)) ((x 4))
  (local ((xu (cat 0b0 x)))
   (if (< xu 9) (mv (mod+ x 1) 0b0) (mv 0 0b1))))

The inc_digit function takes a digit and a carry bit as input. If the carry bit has a value of 1, inc_digit returns an incremented digit and the carry obtained by incrementing the input digit using the inc4 function. If the value of the input carry bit is 0, then the input digit and input carry are returned. 

(inc_digit ((4) (1)) ((x 4) (c 1)) (if c (inc4 x) (mv x 0b0)))

The inc_digits function is used to increment the decimal counter. The inc_digits function takes the entire state of the decimal counter as input. The first digit is incremented using the inc_digit function and the carry generated is used to increment the second digit. 

 
(inc_digits (8) ((x 8))
  (local
   ((((x0 4) (c0 1)) (inc4 (bits x 0 3)))
    (((x1 4) (c1 1)) (inc_digit (bits x 4 7) c0)))
   (cat x1 x0)))

The valid_digits function checks if each digit of the decimal counter is valid, i.e., if the value of each digit is less than 10. 

(valid_digits (1) ((x 8))
  (and (< (cat 0b0 (bits x 0 3)) 10) (< (cat 0b0 (bits x 4 7)) 10)))

The formula corresponding to the correctness property of the decimal counter is given below. The formula states that if the digit of any state of the decimal counter is valid as given by the valid_digits function, then these digits will remain valid after being incremented using the inc_digits functions. 

(-> (valid_digits x) (valid_digits (inc_digits x)))

The example was generated using a simple Lisp program that is given below. The top-level function of the lisp program gen_dec_counter can be used to generate the BAT model for a decimal counter with any number of digits. The number of digits is given as input to the gen_dec_counter function. The BAT decimal counter example was based on an ACL2 decimal counter example that we obtained from Erik Reeber and Warren Hunt. We would like to thank Erik and Warren for the ACL2 decimal counter example. 

(defun gen-valid_digits (n)
  (loop for i from 0 below (* 4 n) by 4
	collect `(< (cat 0b0 (bits x ,i ,(+ i 3))) 10) into lst
	finally (return `(valid_digits (1) ((x ,(* 4 n)))
				       (and ,@lst)))))

(defun xi (i)
  (read-from-string (format nil "x~D" i)))

(defun ci (i)
  (read-from-string (format nil "c~D" i)))

(defun gen-inc_digits (n)
  (loop for i from 1 below n
	for xi = (xi i)
	for i4 = (* i 4)
	collect `(((,xi 4) (,(ci i) 1))
		  (inc_digit (bits x ,i4 ,(+ i4 3))
			     ,(ci (1- i))))
	  into bindings
	collect xi into cat-args
	finally (return `(inc_digits (,(* 4 n)) ((x ,(* 4 n)))
				     (local ,(cons '(((x0 4) (c0 1)) (inc4 (bits x 0 3)))
						   bindings)
					    (cat ,@(reverse (cons 'x0 cat-args))))))))

(defun gen_dec_counter (n)
  (print :forall)
  (print `((x ,(* 4 n))))
  (print `((inc4 ((4) (1)) ((x 4))
		 (local ((xu (cat 0b0 x)))
			(if (< xu 9)
			    (mv (mod+ x 1)
				0b0)
			  (mv 0 0b1))))
	   (inc_digit ((4) (1)) ((x 4) (c 1))
		      (if c (inc4 x) (mv x 0b0)))
	   ,(gen-valid_digits n)
	   ,(gen-inc_digits n)))
  (print '(-> (valid_digits x) (valid_digits (inc_digits x))))
  nil)

Sudoku Solver

 The following example shows how BAT can be used to solve Sudoku problems. We wrote lisp code that generates a BAT file that can be used to solve Sudoku problems. The idea was to generate 91 variable, B11, ..., B99 (Bij stands for Board position i, j). Each variable is constrainted to be a 5-bit bit-vector between 1 and 9. The lisp code is shown first, and then the BAT code it generates follows. To solve a particular Sudoku problem, just enter the constraints for the board positions with fixed values where indicated. We include a problem from http://dingo.sbs.arizona.edu/~sandiway/sudoku/examples.html whose description is:

These puzzles are not fun anymore. I wonder if they are tractable for non-computer puzzle solving. At some steps, they seem to require long chains of inference just to eliminate a single value.

This is solved in about 1/10 of a second (wall clock time).

The lisp code is: 

; Generate the list of variables from the declarations
(defun gen-vars () (mapcar #'car (gen-var-decls)))

; Generate the different function
(defun gen-different ()
  (loop for i from 1 to 9
        collect `(,(read-from-string (format nil "X~D" i)) 5) into vars
        collect
        (loop for j from (1+ i) to 9
              collect `(not (= ,(read-from-string (format nil "X~D" i))
                               ,(read-from-string (format nil "X~D" j)))))
        into body
        finally (return `(different (1) ,vars ,(cons 'and (reduce #'append body))))))

(defun different-row-col (row?)
  (loop for i from 1 to 9
        collect 
        (loop for j from 1 to 9
              collect
              (read-from-string (format nil "B~D~D" (if row? i j) (if row? j i))))
        into row-diff
        finally (return (mapcar #'(lambda (x) (cons 'different x)) row-diff))))

(defun different-block ()
  (loop for i from 0 to 2
        collect 
        (loop for j from 0 to 2
              collect
              (loop for r from (1+ (* i 3)) to (* (1+ i) 3)
                    collect
                    (loop for c from (1+ (* j 3)) to (* (1+ j) 3)
                          collect
                          (read-from-string (format nil "B~D~D" r c)))
                    into r-l
                    finally (return (reduce #'append r-l)))
              into j-l
              finally (return (mapcar #'(lambda (x) (cons 'different x)) j-l)))
        into i-l
        finally (return (reduce #'append i-l))))

(defun sudoku ()
  (print :exists)
  (print (gen-var-decls))
  (print `((in-range (1) ((x 5)) (and (<= 1 x) (<= x 9)))
           ,(gen-different)))
  (print `(and ,@(mapcar #'(lambda (x) `(in-range ,x)) (gen-vars))
               ,@(different-row-col t)
               ,@(different-row-col nil)
               ,@(different-block)))
  nil)

(sudoku)

The BAT file generated is 

:exists

((B11 5) (B12 5) (B13 5) (B14 5) (B15 5) (B16 5) (B17 5) (B18 5) (B19 5)
 (B21 5) (B22 5) (B23 5) (B24 5) (B25 5) (B26 5) (B27 5) (B28 5) (B29 5)
 (B31 5) (B32 5) (B33 5) (B34 5) (B35 5) (B36 5) (B37 5) (B38 5) (B39 5)
 (B41 5) (B42 5) (B43 5) (B44 5) (B45 5) (B46 5) (B47 5) (B48 5) (B49 5)
 (B51 5) (B52 5) (B53 5) (B54 5) (B55 5) (B56 5) (B57 5) (B58 5) (B59 5)
 (B61 5) (B62 5) (B63 5) (B64 5) (B65 5) (B66 5) (B67 5) (B68 5) (B69 5)
 (B71 5) (B72 5) (B73 5) (B74 5) (B75 5) (B76 5) (B77 5) (B78 5) (B79 5)
 (B81 5) (B82 5) (B83 5) (B84 5) (B85 5) (B86 5) (B87 5) (B88 5) (B89 5)
 (B91 5) (B92 5) (B93 5) (B94 5) (B95 5) (B96 5) (B97 5) (B98 5) (B99 5))

((IN-RANGE (1) ((X 5)) (AND (<= 1 X) (<= X 9)))
 (DIFFERENT (1)
            ((X1 5) (X2 5) (X3 5) (X4 5) (X5 5) (X6 5) (X7 5) (X8 5) (X9 5))
            (AND (NOT (= X1 X2)) (NOT (= X1 X3)) (NOT (= X1 X4))
                 (NOT (= X1 X5)) (NOT (= X1 X6)) (NOT (= X1 X7))
                 (NOT (= X1 X8)) (NOT (= X1 X9)) (NOT (= X2 X3))
                 (NOT (= X2 X4)) (NOT (= X2 X5)) (NOT (= X2 X6))
                 (NOT (= X2 X7)) (NOT (= X2 X8)) (NOT (= X2 X9))
                 (NOT (= X3 X4)) (NOT (= X3 X5)) (NOT (= X3 X6))
                 (NOT (= X3 X7)) (NOT (= X3 X8)) (NOT (= X3 X9))
                 (NOT (= X4 X5)) (NOT (= X4 X6)) (NOT (= X4 X7))
                 (NOT (= X4 X8)) (NOT (= X4 X9)) (NOT (= X5 X6))
                 (NOT (= X5 X7)) (NOT (= X5 X8)) (NOT (= X5 X9))
                 (NOT (= X6 X7)) (NOT (= X6 X8)) (NOT (= X6 X9))
                 (NOT (= X7 X8)) (NOT (= X7 X9)) (NOT (= X8 X9))))) 

(AND (IN-RANGE B11) (IN-RANGE B12) (IN-RANGE B13) (IN-RANGE B14) (IN-RANGE B15)
     (IN-RANGE B16) (IN-RANGE B17) (IN-RANGE B18) (IN-RANGE B19) (IN-RANGE B21)
     (IN-RANGE B22) (IN-RANGE B23) (IN-RANGE B24) (IN-RANGE B25) (IN-RANGE B26)
     (IN-RANGE B27) (IN-RANGE B28) (IN-RANGE B29) (IN-RANGE B31) (IN-RANGE B32)
     (IN-RANGE B33) (IN-RANGE B34) (IN-RANGE B35) (IN-RANGE B36) (IN-RANGE B37)
     (IN-RANGE B38) (IN-RANGE B39) (IN-RANGE B41) (IN-RANGE B42) (IN-RANGE B43)
     (IN-RANGE B44) (IN-RANGE B45) (IN-RANGE B46) (IN-RANGE B47) (IN-RANGE B48)
     (IN-RANGE B49) (IN-RANGE B51) (IN-RANGE B52) (IN-RANGE B53) (IN-RANGE B54)
     (IN-RANGE B55) (IN-RANGE B56) (IN-RANGE B57) (IN-RANGE B58) (IN-RANGE B59)
     (IN-RANGE B61) (IN-RANGE B62) (IN-RANGE B63) (IN-RANGE B64) (IN-RANGE B65)
     (IN-RANGE B66) (IN-RANGE B67) (IN-RANGE B68) (IN-RANGE B69) (IN-RANGE B71)
     (IN-RANGE B72) (IN-RANGE B73) (IN-RANGE B74) (IN-RANGE B75) (IN-RANGE B76)
     (IN-RANGE B77) (IN-RANGE B78) (IN-RANGE B79) (IN-RANGE B81) (IN-RANGE B82)
     (IN-RANGE B83) (IN-RANGE B84) (IN-RANGE B85) (IN-RANGE B86) (IN-RANGE B87)
     (IN-RANGE B88) (IN-RANGE B89) (IN-RANGE B91) (IN-RANGE B92) (IN-RANGE B93)
     (IN-RANGE B94) (IN-RANGE B95) (IN-RANGE B96) (IN-RANGE B97) (IN-RANGE B98)
     (IN-RANGE B99) (DIFFERENT B11 B12 B13 B14 B15 B16 B17 B18 B19)
     (DIFFERENT B21 B22 B23 B24 B25 B26 B27 B28 B29)
     (DIFFERENT B31 B32 B33 B34 B35 B36 B37 B38 B39)
     (DIFFERENT B41 B42 B43 B44 B45 B46 B47 B48 B49)
     (DIFFERENT B51 B52 B53 B54 B55 B56 B57 B58 B59)
     (DIFFERENT B61 B62 B63 B64 B65 B66 B67 B68 B69)
     (DIFFERENT B71 B72 B73 B74 B75 B76 B77 B78 B79)
     (DIFFERENT B81 B82 B83 B84 B85 B86 B87 B88 B89)
     (DIFFERENT B91 B92 B93 B94 B95 B96 B97 B98 B99)
     (DIFFERENT B11 B21 B31 B41 B51 B61 B71 B81 B91)
     (DIFFERENT B12 B22 B32 B42 B52 B62 B72 B82 B92)
     (DIFFERENT B13 B23 B33 B43 B53 B63 B73 B83 B93)
     (DIFFERENT B14 B24 B34 B44 B54 B64 B74 B84 B94)
     (DIFFERENT B15 B25 B35 B45 B55 B65 B75 B85 B95)
     (DIFFERENT B16 B26 B36 B46 B56 B66 B76 B86 B96)
     (DIFFERENT B17 B27 B37 B47 B57 B67 B77 B87 B97)
     (DIFFERENT B18 B28 B38 B48 B58 B68 B78 B88 B98)
     (DIFFERENT B19 B29 B39 B49 B59 B69 B79 B89 B99)
     (DIFFERENT B11 B12 B13 B21 B22 B23 B31 B32 B33)
     (DIFFERENT B14 B15 B16 B24 B25 B26 B34 B35 B36)
     (DIFFERENT B17 B18 B19 B27 B28 B29 B37 B38 B39)
     (DIFFERENT B41 B42 B43 B51 B52 B53 B61 B62 B63)
     (DIFFERENT B44 B45 B46 B54 B55 B56 B64 B65 B66)
     (DIFFERENT B47 B48 B49 B57 B58 B59 B67 B68 B69)
     (DIFFERENT B71 B72 B73 B81 B82 B83 B91 B92 B93)
     (DIFFERENT B74 B75 B76 B84 B85 B86 B94 B95 B96)
     (DIFFERENT B77 B78 B79 B87 B88 B89 B97 B98 B99)

; Enter the constraints for your specific Sudoku problem here
     
     (= B12 2)
     (= B24 6)
     (= B29 3)
     (= B32 7)
     (= B33 4)
     (= B35 8)
     (= B46 3)
     (= B49 2)
     (= B52 8)
     (= B55 4)
     (= B58 1)
     (= B61 6)
     (= B64 5)
     (= B75 1)
     (= B77 7)
     (= B78 8)
     (= B81 5)
     (= B86 9)
     (= B98 4)

     )