4 ms·

An expert system answer (Prolog, CLIPS) would be cool to see here.

felixyz 7y ago
You should check this out, solving a somewhat similar type of problem using Alloy: https://www.hillelwayne.com/post/knights-knaves/ https://www.hillelwayne.com/post/knights-knaves/
dmurray 7y ago
The second answer is a C program. It specifies the constraints and loops over all the possible solutions. That's the most naive constraint solver possible, but adequate for this task. Once you put in the effort of translating the problem into constraints, the Prolog solution is trivial, because the Prolog compiler is a constraint solver.
tephra 7y ago
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), sat(A4 =:= A1+A2+A3), sat(A5 =:= ~(A1+A2+A3+A4)), sat(A6 =:= ~(A1+A2+A3+A4+A5)). [0] https://www.metalevel.at/prolog/puzzles https://www.metalevel.at/prolog/puzzles
- 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]

You should check this out, solving a somewhat similar type of problem using Alloy: https://www.hillelwayne.com/post/knights-knaves/ https://www.hillelwayne.com/post/knights-knaves/

dmurray 7y ago

The second answer is a C program. It specifies the constraints and loops over all the possible solutions. That's the most naive constraint solver possible, but adequate for this task. Once you put in the effort of translating the problem into constraints, the Prolog solution is trivial, because the Prolog compiler is a constraint solver.

tephra 7y ago

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), sat(A4 =:= A1+A2+A3), sat(A5 =:= ~(A1+A2+A3+A4)), sat(A6 =:= ~(A1+A2+A3+A4+A5)). [0] https://www.metalevel.at/prolog/puzzles https://www.metalevel.at/prolog/puzzles

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]