4 ms·

Using the clpb library [0]: solution([A1,A2,A3,A4,A5,A6]) :- sat(A1 =:= A2*A3*A4*A5*A6), sat(A2 =:= ~(A3+A4+A5+A6)), sat(A3 =:= A1*A2

• archi42 7y ago
  Imho this would be a nice answer for stack exchange as well.
• pfortuny 7y ago
  The fact that it is consistent does not mean that it is correct...
• grubb 7y ago
  Alternatively using z3 [0]: (declare-const a1 Bool) (declare-const a2 Bool) (declare-const a3 Bool) (declare-const a4 Bool) (declare-const a5 Bool) (declare-const a6 Bool) (assert (= a1 (and a2 (and a3 (and a4 (and a5 a6)))))) (assert (= a2 (not (or a3 (or a4 (or a5 a6)))))) (assert (= a3 (and a1 a2))) (assert (= a4 (or a1 (or a2 a3)))) (assert (= a5 (not (or a1 (or a2 (or a3 a4)))))) (assert (= a6 (not (or a1 (or a2 (or a3 (or a4 a5))))))) (assert (or a1 (or a2 (or a3 (or a4 (or a5 a6)))))) (check-sat) (get-model) (exit) The model is satisfiable where only a5 is true, anyone can run it themselves and play with it [1]. Additionally forcing a5 to be false by adding the following to the list of assertions: (assert (not a5)) And the model becomes unsatisfiable. Edit: Finally, to make sure there's not some possible solution where a5 is true as well as another assertion you could alternatively add this assertion: (assert (and a5 (or a1 (or a2 (or a3 (or a4 (or a6))))))) And the model also becomes unsatisfiable. So 5 only seems to be the correct answer. [0] https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [1] https://rise4fun.com/Z3/1DMW https://rise4fun.com/Z3/1DMW
  • Recursing 7y ago
    I posted a solution using the python z3 library, which might be easier to use for people used to python, here: https://news.ycombinator.com/item?id=21545143 https://news.ycombinator.com/item?id=21545143
    • Recursing 7y ago
      That solution was not correct, see https://news.ycombinator.com/item?id=21568151 https://news.ycombinator.com/item?id=21568151
• justtopostthis3 7y ago
  Using no libraries! a1([f,f,_,_,_,_]). a1([f,t,f,_,_,_]). a1([f,t,t,f,_,_]). a1([f,t,t,t,f,_]). a1([f,t,t,t,t,f]). a1([t,t,t,t,t,t]). a2([_,f,t,_,_,_]). a2([_,f,f,t,_,_]). a2([_,f,f,f,t,_]). a2([_,f,f,f,f,t]). a2([_,t,f,f,f,f]). a3([f,_,f,_,_,_]). a3([t,f,f,_,_,_]). a3([t,t,t,_,_,_]). a4([t,_,_,t,_,_]). a4([f,t,_,t,_,_]). a4([f,f,t,t,_,_]). a4([f,f,f,f,_,_]). a5([t,_,_,_,f,_]). a5([f,t,_,_,f,_]). a5([f,f,t,_,f,_]). a5([f,f,f,t,f,_]). a5([f,f,f,f,t,_]). a6([t,_,_,_,_,f]). a6([f,t,_,_,_,f]). a6([f,f,t,_,_,f]). a6([f,f,f,t,_,f]). a6([f,f,f,f,t,f]). a6([f,f,f,f,f,t]). solution(X) :- a1(X), a2(X), a3(X), a4(X), a5(X), a6(X).
• deleted 7y ago
  [deleted]