4 ms·
With Z3 : https://rise4fun.com/z3 https://rise4fun.com/z3 (declare-const a Bool) (declare-const b Bool) (declare-const c Bool) (declare-const d
by hokkos 7y ago
With Z3 :
https://rise4fun.com/z3 https://rise4fun.com/z3
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)
(declare-const e Bool)
(declare-const f Bool)
(define-fun conjecture () Bool
(and
(= a (and b c d e f))
(= b (and (not b) (not c) (not d) (not e) (not f)))
(= c (and a b))
(= d (or a b c))
(= e (and (not a) (not b) (not c) (not d)))
(= f (and (not a) (not b) (not c) (not d) (not e)))
(xor a b c d e f)
)
)
(assert conjecture)
(check-sat)
(get-model)
result :
sat
(model
(define-fun f () Bool
false)
(define-fun b () Bool
false)
(define-fun a () Bool
false)
(define-fun c () Bool
false)
(define-fun d () Bool
false)
(define-fun e () Bool
true)
)
Old code was with another tool :
http://logictools.org/ http://logictools.org/
(a-> (b & c & d & e & -f)) &
(b -> (-b & -c & -d & -e & -f)) &
(c -> (a & b)) &
(d -> (a | b | c)) &
(e -> (-a & -b & -c & -d)) &
(f -> (-a & -b & -c & -d & -e)) &
( a + b + c + d + e + f)
then
(a <-> (b & c & d & e & f)) &
(b <-> (-b & -c & -d & -e & -f)) &
(c <-> (a & b)) &
(d <-> (a | b | c)) &
(e <-> (-a & -b & -c & -d)) &
(f <-> (-a & -b & -c & -d & -e)) &
( a + b + c + d + e + f)
where it would crash
- colanderman 7y agoImplication is not strong enough. That permits e.g. f to be true and e to be false. Also I don't know the specifics of the language that tool uses, but typically variadic XOR simply constrains that an odd number of its operands are true. (It so happens that there are no solutions to this problem with 3 or 5 true answers.)
- hokkos 7y agoI changed the solver as it would crash when I corrected my code, and redone it with z3 online.