Sugar 1 2 3 1 CSPSAT 2008 8 21
Sugar 1 2 3 Sugar Sugar (CSP) (SAT ) (encode) SAT SAT order encoding direct encoding support encoding http://bachistckobe-uacjp/sugar/ Web
Sugar 1 2 3 Sugar SAT (COP) MAX-CSP International CSP Solver Competition XCSP 21 (5000 ) SAT MiniSat, PicoSAT Cygwin Windows XP CSP Lisp 3 International CSP Solver Competition Web Sugar Windows Cygwin Web
Sugar 1 2 3 Sugar (1) Web () (bool p) (int x 1 4) (int y (0 2 5)) ; p ; x {1, 2, 3, 4} ; y {0, 2, 5} Sugar Web
Sugar 1 2 3 Sugar (2) Web abs, neg (-), add (+), sub (-), mul (*), div (/), mod (%), min, max, if eq (=), ne (!=), le (<=), lt (<), ge (>=), gt (>) not (!), and (&&), or ( ), imp (=>), xor, iff alldifferent, weightedsum, cumulative, element (or (> x (+ y 1)) (> y x)) ; (x > y + 1) (y > x) (alldifferent x y z) Sugar Web
Sugar 1 2 3 CSP 3 3 (int x_1_1 1 9) (int x_1_2 1 9) (int x_1_3 1 9) (int x_2_1 1 9) (int x_2_2 1 9) (int x_2_3 1 9) (int x_3_1 1 9) (int x_3_2 1 9) (int x_3_3 1 9) (alldifferent x_1_1 x_1_2 x_1_3 x_2_1 x_2_2 x_2_3 x_3_1 x_3_2 x_3_3) (= (+ x_1_1 x_1_2 x_1_3) 15) (= (+ x_2_1 x_2_2 x_2_3) 15) (= (+ x_3_1 x_3_2 x_3_3) 15) (= (+ x_1_1 x_2_1 x_3_1) 15) (= (+ x_1_2 x_2_2 x_3_2) 15) (= (+ x_1_3 x_2_3 x_3_3) 15) (= (+ x_1_1 x_2_2 x_3_3) 15) (= (+ x_1_3 x_2_2 x_3_1) 15)
Sugar 1 2 3 Sugar 3 3 $ sugar -vv magicsquare-3x3csp c 0 Sugar v1-14 + minisat c 0 c 0 ENCODING magicsquare-3x3csp TO /tmp/sugar17777cnf c 0 CSP : 9 integers, 0 booleans, 54 clauses, largest domain size 9 c 0 c 0 SAT : 144 SAT variables, 1709 SAT clauses, 20164 bytes c 0 c 1 SOLVING /tmp/sugar17777cnf c 1 CMD minisat /tmp/sugar17777cnf /tmp/sugar17777out c 1 c 1 DECODING /tmp/sugar17777out WITH /tmp/sugar17777map c 1 s SATISFIABLE a x_1_1 2 a x_1_2 9 a x_1_3 4 a x_2_1 7 a x_2_2 5 a x_2_3 3 a x_3_1 6 a x_3_2 1 a x_3_3 8 a c 1 c 1 CPU 075 (006 002 059 008) c 1 END Fri Aug 15 21:56:35 2008
Sugar 1 2 3 (1) Sugar Web Web
Sugar 1 2 3 (1) Sugar :-) Prolog Sugar Web Web
Sugar 1 2 3 (2)
Sugar 1 2 3
Sugar 1 2 3 Web 1 1 9 2 9 ) 9 ) 3x3 9 9 1 9 1
Sugar 1 2 3 Sugar Web i j x i j 1 9 alldifferent (int x_0_0 1 9) ; x_0_0 {1, 2,, 9} (int x_0_1 1 9) ; x_0_1 {1, 2,, 9} (int x_0_2 6 6) ; x_0_2 {6} (alldifferent x_0_0 x_0_1 x_0_8) ; 0 (alldifferent x_0_0 x_1_0 x_8_0) ; 0
Sugar 1 2 3 Sugar Web i j x i j 1 9 alldifferent (int x_0_0 1 9) ; x_0_0 {1, 2,, 9} (int x_0_1 1 9) ; x_0_1 {1, 2,, 9} (int x_0_2 6 6) ; x_0_2 {6} (alldifferent x_0_0 x_0_1 x_0_8) ; 0 (alldifferent x_0_0 x_1_0 x_8_0) ; 0
Sugar 1 2 3 Sugar Web i j x i j 1 9 alldifferent (int x_0_0 1 9) ; x_0_0 {1, 2,, 9} (int x_0_1 1 9) ; x_0_1 {1, 2,, 9} (int x_0_2 6 6) ; x_0_2 {6} (alldifferent x_0_0 x_0_1 x_0_8) ; 0 (alldifferent x_0_0 x_1_0 x_8_0) ; 0
Sugar 1 2 3 Web 1 1 9 0( ) 2 3 1
Sugar 1 2 3 Sugar Web i j x i j alldifferent (int x_1_2 1 9) (int x_1_3 1 9) (= (+ x_1_2 x_1_3) 5) (alldifferent x_1_2 x_1_3)
Sugar 1 2 3 Sugar Web i j x i j alldifferent (int x_1_2 1 9) (int x_1_3 1 9) (= (+ x_1_2 x_1_3) 5) (alldifferent x_1_2 x_1_3)
Sugar 1 2 3 Sugar Web i j x i j alldifferent (int x_1_2 1 9) (int x_1_3 1 9) (= (+ x_1_2 x_1_3) 5) (alldifferent x_1_2 x_1_3)
Sugar 1 2 3 Sugar Web i j x i j alldifferent (int x_1_2 1 9) (int x_1_3 1 9) (= (+ x_1_2 x_1_3) 5) (alldifferent x_1_2 x_1_3)
Sugar 1 2 3 Web 1 ( ) 2 4 3 4
Sugar 1 2 3 Sugar Web i j x i j {0, 1} 1 1 1 (int x_0_0 0 1) (= (+ x_0_4 x_0_6 x_1_5) 1) (<= (+ x_0_0 x_1_0 x_2_0) 1) (>= (+ x_2_3 x_1_3 x_0_3 x_2_2 x_2_1 x_2_0 x_2_4 x_2_5 x_3_3) 1)
Sugar 1 2 3 Sugar Web i j x i j {0, 1} 1 1 1 (int x_0_0 0 1) (= (+ x_0_4 x_0_6 x_1_5) 1) (<= (+ x_0_0 x_1_0 x_2_0) 1) (>= (+ x_2_3 x_1_3 x_0_3 x_2_2 x_2_1 x_2_0 x_2_4 x_2_5 x_3_3) 1)
Sugar 1 2 3 Sugar Web i j x i j {0, 1} 1 1 1 (int x_0_0 0 1) (= (+ x_0_4 x_0_6 x_1_5) 1) (<= (+ x_0_0 x_1_0 x_2_0) 1) (>= (+ x_2_3 x_1_3 x_0_3 x_2_2 x_2_1 x_2_0 x_2_4 x_2_5 x_3_3) 1)
Sugar 1 2 3 Sugar Web i j x i j {0, 1} 1 1 1 (int x_0_0 0 1) (= (+ x_0_4 x_0_6 x_1_5) 1) (<= (+ x_0_0 x_1_0 x_2_0) 1) (>= (+ x_2_3 x_1_3 x_0_3 x_2_2 x_2_1 x_2_0 x_2_4 x_2_5 x_3_3) 1)
Sugar 1 2 3 Sugar Web i j x i j {0, 1} 1 1 1 (int x_0_0 0 1) (= (+ x_0_4 x_0_6 x_1_5) 1) (<= (+ x_0_0 x_1_0 x_2_0) 1) (>= (+ x_2_3 x_1_3 x_0_3 x_2_2 x_2_1 x_2_0 x_2_4 x_2_5 x_3_3) 1)
Sugar 1 2 3 Web 1 ( ) 2 1 1 4 1x4 2x2 4x1 3 1
Sugar 1 2 3 Sugar Web k r k, c k h k, w k r k, c k, h k, w k (int r_0 0 9) (int c_0 0 9) (int h_0 (1 2 4 8)) (int w_0 (1 2 4 8)) (or (and (= h_0 1) (= w_0 8)) (and (= h_0 2) (= w_0 4)) (and (= h_0 4) (= w_0 2)) (and (= h_0 8) (= w_0 1))) (<= (+ r_0 h_0) 10) (<= (+ c_0 w_0) 10) (<= r_0 0) (< 0 (+ r_0 h_0)) (<= c_0 4) (< 4 (+ c_0 w_0)) (or (<= (+ r_0 h_0) r_1) (<= (+ r_1 h_1) r_0) (<= (+ c_0 w_0) c_1) (<= (+ c_1 w_1) c_0))
Sugar 1 2 3 Sugar Web k r k, c k h k, w k r k, c k, h k, w k (int r_0 0 9) (int c_0 0 9) (int h_0 (1 2 4 8)) (int w_0 (1 2 4 8)) (or (and (= h_0 1) (= w_0 8)) (and (= h_0 2) (= w_0 4)) (and (= h_0 4) (= w_0 2)) (and (= h_0 8) (= w_0 1))) (<= (+ r_0 h_0) 10) (<= (+ c_0 w_0) 10) (<= r_0 0) (< 0 (+ r_0 h_0)) (<= c_0 4) (< 4 (+ c_0 w_0)) (or (<= (+ r_0 h_0) r_1) (<= (+ r_1 h_1) r_0) (<= (+ c_0 w_0) c_1) (<= (+ c_1 w_1) c_0))
Sugar 1 2 3 Sugar Web k r k, c k h k, w k r k, c k, h k, w k (int r_0 0 9) (int c_0 0 9) (int h_0 (1 2 4 8)) (int w_0 (1 2 4 8)) (or (and (= h_0 1) (= w_0 8)) (and (= h_0 2) (= w_0 4)) (and (= h_0 4) (= w_0 2)) (and (= h_0 8) (= w_0 1))) (<= (+ r_0 h_0) 10) (<= (+ c_0 w_0) 10) (<= r_0 0) (< 0 (+ r_0 h_0)) (<= c_0 4) (< 4 (+ c_0 w_0)) (or (<= (+ r_0 h_0) r_1) (<= (+ r_1 h_1) r_0) (<= (+ c_0 w_0) c_1) (<= (+ c_1 w_1) c_0))
Sugar 1 2 3 Sugar Web k r k, c k h k, w k r k, c k, h k, w k (int r_0 0 9) (int c_0 0 9) (int h_0 (1 2 4 8)) (int w_0 (1 2 4 8)) (or (and (= h_0 1) (= w_0 8)) (and (= h_0 2) (= w_0 4)) (and (= h_0 4) (= w_0 2)) (and (= h_0 8) (= w_0 1))) (<= (+ r_0 h_0) 10) (<= (+ c_0 w_0) 10) (<= r_0 0) (< 0 (+ r_0 h_0)) (<= c_0 4) (< 4 (+ c_0 w_0)) (or (<= (+ r_0 h_0) r_1) (<= (+ r_1 h_1) r_0) (<= (+ c_0 w_0) c_1) (<= (+ c_1 w_1) c_0))
Sugar 1 2 3 Sugar Web k r k, c k h k, w k r k, c k, h k, w k (int r_0 0 9) (int c_0 0 9) (int h_0 (1 2 4 8)) (int w_0 (1 2 4 8)) (or (and (= h_0 1) (= w_0 8)) (and (= h_0 2) (= w_0 4)) (and (= h_0 4) (= w_0 2)) (and (= h_0 8) (= w_0 1))) (<= (+ r_0 h_0) 10) (<= (+ c_0 w_0) 10) (<= r_0 0) (< 0 (+ r_0 h_0)) (<= c_0 4) (< 4 (+ c_0 w_0)) (or (<= (+ r_0 h_0) r_1) (<= (+ r_1 h_1) r_0) (<= (+ c_0 w_0) c_1) (<= (+ c_1 w_1) c_0))
Sugar 1 2 3 Wikipedia 1 2 3 1
Sugar 1 2 3 Sugar Web i j x i j {0, 1} i k h i k j k v j k i j (int x_0_0 0 1) (int h_0_0 0 4) (iff (= x_0_0 1) (and (<= h_0_0 0) (< 0 (+ h_0_0 4)))) (< (+ h_1_0 2) h_1_1)
Sugar 1 2 3 Sugar Web i j x i j {0, 1} i k h i k j k v j k i j (int x_0_0 0 1) (int h_0_0 0 4) (iff (= x_0_0 1) (and (<= h_0_0 0) (< 0 (+ h_0_0 4)))) (< (+ h_1_0 2) h_1_1)
Sugar 1 2 3 Sugar Web i j x i j {0, 1} i k h i k j k v j k i j (int x_0_0 0 1) (int h_0_0 0 4) (iff (= x_0_0 1) (and (<= h_0_0 0) (< 0 (+ h_0_0 4)))) (< (+ h_1_0 2) h_1_1)
Sugar 1 2 3 Sugar Web i j x i j {0, 1} i k h i k j k v j k i j (int x_0_0 0 1) (int h_0_0 0 4) (iff (= x_0_0 1) (and (<= h_0_0 0) (< 0 (+ h_0_0 4)))) (< (+ h_1_0 2) h_1_1)
Sugar 1 2 3 Sugar Web i j x i j {0, 1} i k h i k j k v j k i j (int x_0_0 0 1) (int h_0_0 0 4) (iff (= x_0_0 1) (and (<= h_0_0 0) (< 0 (+ h_0_0 4)))) (< (+ h_1_0 2) h_1_1)
Sugar 1 2 3 Web 1 2 3 1 1
Sugar 1 2 3 Sugar Web i j v i j {0, 1} h i j {0, 1} (degree) 1 0 2 i j x i j x i j (int v_0_0 0 1) (int h_0_0 0 1) (int d_0_0 (0 2)) (= d_0_0 (+ v_0_0 h_0_0)) (int x_0_0 1 5) (=> (> v_0_0 0) (= x_0_0 x_1_0))
Sugar 1 2 3 Sugar Web i j v i j {0, 1} h i j {0, 1} (degree) 1 0 2 i j x i j x i j (int v_0_0 0 1) (int h_0_0 0 1) (int d_0_0 (0 2)) (= d_0_0 (+ v_0_0 h_0_0)) (int x_0_0 1 5) (=> (> v_0_0 0) (= x_0_0 x_1_0))
Sugar 1 2 3 Sugar Web i j v i j {0, 1} h i j {0, 1} (degree) 1 0 2 i j x i j x i j (int v_0_0 0 1) (int h_0_0 0 1) (int d_0_0 (0 2)) (= d_0_0 (+ v_0_0 h_0_0)) (int x_0_0 1 5) (=> (> v_0_0 0) (= x_0_0 x_1_0))
Sugar 1 2 3 Sugar Web i j v i j {0, 1} h i j {0, 1} (degree) 1 0 2 i j x i j x i j (int v_0_0 0 1) (int h_0_0 0 1) (int d_0_0 (0 2)) (= d_0_0 (+ v_0_0 h_0_0)) (int x_0_0 1 5) (=> (> v_0_0 0) (= x_0_0 x_1_0))
Sugar 1 2 3
Sugar 1 2 3 Web 1 1 2 4 3
Sugar 1 2 3 Sugar (1) Web 1 ( ) i j v i j h i j { 1, 0, 1} 0 2 (1) (int v_0_0-1 1) (int h_0_0-1 1) (= (+ (abs v_3_1) (abs h_3_1) (abs v_3_2) (abs h_4_1)) 3) (int d_1_2 (0 2)) (= d_1_2 (+ (abs v_0_2) (abs h_1_1) (abs v_1_2) (abs h_1_2))) (= (+ v_0_2 h_1_1 (neg v_1_2) (neg h_1_2)) 0)
Sugar 1 2 3 Sugar (1) Web 1 ( ) i j v i j h i j { 1, 0, 1} 0 2 (1) (int v_0_0-1 1) (int h_0_0-1 1) (= (+ (abs v_3_1) (abs h_3_1) (abs v_3_2) (abs h_4_1)) 3) (int d_1_2 (0 2)) (= d_1_2 (+ (abs v_0_2) (abs h_1_1) (abs v_1_2) (abs h_1_2))) (= (+ v_0_2 h_1_1 (neg v_1_2) (neg h_1_2)) 0)
Sugar 1 2 3 Sugar (1) Web 1 ( ) i j v i j h i j { 1, 0, 1} 0 2 (1) (int v_0_0-1 1) (int h_0_0-1 1) (= (+ (abs v_3_1) (abs h_3_1) (abs v_3_2) (abs h_4_1)) 3) (int d_1_2 (0 2)) (= d_1_2 (+ (abs v_0_2) (abs h_1_1) (abs v_1_2) (abs h_1_2))) (= (+ v_0_2 h_1_1 (neg v_1_2) (neg h_1_2)) 0)
Sugar 1 2 3 Sugar (1) Web 1 ( ) i j v i j h i j { 1, 0, 1} 0 2 (1) (int v_0_0-1 1) (int h_0_0-1 1) (= (+ (abs v_3_1) (abs h_3_1) (abs v_3_2) (abs h_4_1)) 3) (int d_1_2 (0 2)) (= d_1_2 (+ (abs v_0_2) (abs h_1_1) (abs v_1_2) (abs h_1_2))) (= (+ v_0_2 h_1_1 (neg v_1_2) (neg h_1_2)) 0)
Sugar 1 2 3 Sugar (2) Web 1
Sugar 1 2 3 Sugar (2) Web 1 1 ( ) 1
Sugar 1 2 3 Sugar (3) Web x i j y i j {0, 1} 1 (2) (int x_0_0 0 81) (int y_0_0 0 1) (iff (> d_0_0 0) (> x_0_0 0)) (iff (= x_0_0 1) (= y_0_0 1)) (=> (> v_0_0 0) (or (> x_1_0 x_0_0) (= x_1_0 1))) (=> (> h_0_0 0) (or (> x_0_1 x_0_0) (= x_0_1 1))) (= (+ y_0_0 y_0_1 y_8_8) 1)
Sugar 1 2 3 Sugar (3) Web x i j y i j {0, 1} 1 (2) (int x_0_0 0 81) (int y_0_0 0 1) (iff (> d_0_0 0) (> x_0_0 0)) (iff (= x_0_0 1) (= y_0_0 1)) (=> (> v_0_0 0) (or (> x_1_0 x_0_0) (= x_1_0 1))) (=> (> h_0_0 0) (or (> x_0_1 x_0_0) (= x_0_1 1))) (= (+ y_0_0 y_0_1 y_8_8) 1)
Sugar 1 2 3 Sugar (3) Web x i j y i j {0, 1} 1 (2) (int x_0_0 0 81) (int y_0_0 0 1) (iff (> d_0_0 0) (> x_0_0 0)) (iff (= x_0_0 1) (= y_0_0 1)) (=> (> v_0_0 0) (or (> x_1_0 x_0_0) (= x_1_0 1))) (=> (> h_0_0 0) (or (> x_0_1 x_0_0) (= x_0_1 1))) (= (+ y_0_0 y_0_1 y_8_8) 1)
Sugar 1 2 3 Sugar (3) Web x i j y i j {0, 1} 1 (2) (int x_0_0 0 81) (int y_0_0 0 1) (iff (> d_0_0 0) (> x_0_0 0)) (iff (= x_0_0 1) (= y_0_0 1)) (=> (> v_0_0 0) (or (> x_1_0 x_0_0) (= x_1_0 1))) (=> (> h_0_0 0) (or (> x_0_1 x_0_0) (= x_0_1 1))) (= (+ y_0_0 y_0_1 y_8_8) 1)
Sugar 1 2 3 Web 1 1 1 1 2 3 4
Sugar 1 2 3 Sugar Web i j s i j (bool s_2_3) (iff s_2_3 (or (and (!= v_1_3 0) (!= v_2_3 0)) (and (!= h_2_2 0) (!= h_2_3 0)))) s_6_4 ; (=> (!= v_6_4 0) (or (not s_5_4) (not s_7_4))) (=> (!= h_6_4 0) (or (not s_6_3) (not s_6_5))) (not s_2_3) ; (=> (!= v_1_3 0) s_1_3) (=> (!= v_2_3 0) s_3_3) (=> (!= h_2_2 0) s_2_2) (=> (!= h_2_3 0) s_2_4)
Sugar 1 2 3 Web 1 1 2 1 1 3 4
Sugar 1 2 3 Sugar Web x i j {0, 1} x i j 2 (int x_0_0 0 1) (int x_1_0 0 1) (or (= x_0_0 0) (= x_1_0 0)) (= (+ (neg v_0_0) v_1_0 h_1_0) 0) (= (+ (abs v_0_0) (abs v_1_0) (abs h_1_0)) (* 2 (- 1 x_1_0))) (= (+ x_4_3 x_5_3 x_6_3) 2)
Sugar 1 2 3
Sugar 1 2 3 Web 1 2
Sugar 1 2 3 Sugar (1) Web ( ) i j x i j {0, 1} (0 ) (1) (int x_0_0 0 1) (or (= x_0_2 0) (= x_0_4 0)) (or (> x_0_0 0) (> x_1_0 0))
Sugar 1 2 3 Sugar (1) Web ( ) i j x i j {0, 1} (0 ) (1) (int x_0_0 0 1) (or (= x_0_2 0) (= x_0_4 0)) (or (> x_0_0 0) (> x_1_0 0))
Sugar 1 2 3 Sugar (1) Web ( ) i j x i j {0, 1} (0 ) (1) (int x_0_0 0 1) (or (= x_0_2 0) (= x_0_4 0)) (or (> x_0_0 0) (> x_1_0 0))
Sugar 1 2 3 Sugar (1) Web ( ) i j x i j {0, 1} (0 ) (1) (int x_0_0 0 1) (or (= x_0_2 0) (= x_0_4 0)) (or (> x_0_0 0) (> x_1_0 0))
Sugar 1 2 3 Sugar (2) Web
Sugar 1 2 3 Sugar (2) Web (spanning tree) 1
Sugar 1 2 3 Sugar (3) Web z i j r i j {0, 1} 1 (2) (int z_0_0 0 64) (int r_0_0 0 1) (iff (= x_0_0 0) (= z_0_0 0)) (=> (and (> z_0_0 0) (<= r_0_0 0)) (or (< z_0_0 z_1_0) (< z_0_0 z_0_1))) (= (+ r_0_0 r_0_1 r_7_7) 1)
Sugar 1 2 3 Sugar (3) Web z i j r i j {0, 1} 1 (2) (int z_0_0 0 64) (int r_0_0 0 1) (iff (= x_0_0 0) (= z_0_0 0)) (=> (and (> z_0_0 0) (<= r_0_0 0)) (or (< z_0_0 z_1_0) (< z_0_0 z_0_1))) (= (+ r_0_0 r_0_1 r_7_7) 1)
Sugar 1 2 3 Sugar (3) Web z i j r i j {0, 1} 1 (2) (int z_0_0 0 64) (int r_0_0 0 1) (iff (= x_0_0 0) (= z_0_0 0)) (=> (and (> z_0_0 0) (<= r_0_0 0)) (or (< z_0_0 z_1_0) (< z_0_0 z_0_1))) (= (+ r_0_0 r_0_1 r_7_7) 1)
Sugar 1 2 3 Sugar (3) Web z i j r i j {0, 1} 1 (2) (int z_0_0 0 64) (int r_0_0 0 1) (iff (= x_0_0 0) (= z_0_0 0)) (=> (and (> z_0_0 0) (<= r_0_0 0)) (or (< z_0_0 z_1_0) (< z_0_0 z_0_1))) (= (+ r_0_0 r_0_1 r_7_7) 1)
Sugar 1 2 3 Web 1 2 3 4 1 2 5
Sugar 1 2 3 Sugar Web v i j, h i j { 2, 1, 0, 1, 2} (int v_0_0-2 2) (int h_0_0-2 2) (= (+ (abs v_4_3) (abs h_4_3) (abs v_2_3) (abs h_4_0)) 8) (or (= v_1_1 0) (= h_2_0 0))
Sugar 1 2 3 Web 1 2 3 ( ) 1 4 5 2x2
Sugar 1 2 3 Sugar (1) Web 11
Sugar 1 2 3 Sugar (1) Web 11 11
Sugar 1 2 3 Sugar (2) Web c i j c i j c i j (int c_0_0 1 6) (int c_0_1 3 3) (=> (> x_0_0 0) (= c_0_0 (+ (if (< v_0_0 0) c_1_0 0) (if (< h_0_0 0) c_0_1 0) 1)))
Sugar 1 2 3 Web 1 1 2 1 3 1 4
Sugar 1 2 3 Sugar Web q i j q i j (int q_0_0 1 49) (=> (> r_0_0 0) (= q_0_0 1)) (=> (> v_0_0 0) (= q_0_0 q_1_0)) (=> (= x_0_0 x_1_0) (= q_0_0 q_1_0))
Sugar 1 2 3 Web 1 2 3 3 4
Sugar 1 2 3 Sugar Web i j x i j {0, 1} (0 ) (int x_0_0 0 1) (= (+ x_0_0 x_0_1 x_1_0 x_1_1) 2) (or (> x_0_1 0) (> x_0_2 0) (> x_0_3 0)) (or (= x_0_0 0) (= x_1_0 0))
Sugar 1 2 3 Sugar
Sugar 1 2 3 Sugar!
Sugar 1 2 3 Sugar! 15 15
Sugar 1 2 3 Sugar! 15 15 ( )
Sugar 1 2 3 Sugar! 15 15 ( ) Web Sugar Web (by )