Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Yes. You can try the following smt2 script with yices2 [0]:

  (set-logic QF_UFNIA)
  (declare-fun x () Int)
  (declare-fun y () Int)
  (declare-fun z () Int)
  (define-fun left-side () Int
  (+ (+
    (* (* x (+ x z)) (+ x y))
    (* (* y (+ y z)) (+ x y)))
    (* (* z (+ y z)) (+ x z)))
  )
  (define-fun right-side () Int
  (* (* (*
    4
    (+ y z))
    (+ x z))
    (+ x y))
  )
  ; disallow division by zero
  (assert (not (= 0 (+ y z))))
  (assert (not (= 0 (+ x z))))
  (assert (not (= 0 (+ x y))))
  (assert (= left-side right-side))
  (check-sat)
  (get-model)
Run this by calling yices-smt2 on it.

[0]: http://yices.csl.sri.com/



You need to add:

    (assert (> z 0)) 
    (assert (> x 0)) 
    (assert (> y 0))
or it will give you negative solutions.

I am running this on my machine now. Will report back if it comes up with a solution.


Anything is possible, but I really doubt you'll find those 80 digit numbers. Maybe the sat solver includes some serious number theory though. I doubt it.


Does the `Int` datatype allow negative integers or is it non-negative only? This problem gets much more difficult if you restrict it to positive solutions only.


Int is usually signed. Unsigned int is not signed.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: