Логическа задача

[ins-]

Конете Арко, Брик, Вест, Грош и Доро участват в конно надбягване. Преди състезанието били дадени следните пет прогнози:
(1) Доро ще бъде пръв, а втори ще финишира Вест.
(2) Арко ще заеме второ място, а Грош ще бъде четвърти.
(3) Вест ще бъде трети, а Доро ще финишира последен.
(4) Състезанието ще спечели Вест, а Грош ще бъде четвърти.
(5) Арко ще финишира втори, а веднага след него ще бъде Вест.
Във всяка от прогнозите точно едната част е вярна, а другата – не е вярна.
Кой кон кое място е заел?

[peyo]

Конете Арко, Брик, Вест, Грош и Доро участват в конно надбягване. Преди състезанието били дадени следните пет прогнози:
(1) Доро ще бъде пръв, а втори ще финишира Вест.
(2) Арко ще заеме второ място, а Грош ще бъде четвърти.
(3) Вест ще бъде трети, а Доро ще финишира последен.
(4) Състезанието ще спечели Вест, а Грош ще бъде четвърти.
(5) Арко ще финишира втори, а веднага след него ще бъде Вест.
Във всяка от прогнозите точно едната част е вярна, а другата – не е вярна.
Кой кон кое място е заел?

Интересно! Задачата изглежда особено подходяща за решение със Z3.

Код: Избери целия код

   from z3 import *
   Arko, Brik, Vest, Grosh, Doro = Ints("Arko, Brik, Vest, Grosh, Doro")
   Eq = [
      ((not (Doro == 1)) and Vest == 2) or (Doro == 1 and not (Vest == 2)),
      ((not (Arko == 2)) and Grosh== 4) or (Arko == 2 and not (Grosh == 4)),
      ((not (Vest == 3)) and Doro == 5) or (Vest == 3 and not (Doro == 5)),
      ((not (Vest == 1)) and Grosh == 4) or (Vest == 1 and not (Grosh == 4)),
      ((not (Arko == 2)) and Vest == 3) or (Arko == 2 and not (Vest == 3))
   ]
   solve( Eq )

no solution

Изглежда няма решение. Но може и да съм объркал нещо, затова ако някой намери решение, моля да го каже.

[ins-]

Какво е Z3? Ако правилно разбирам кода - би могло да се напише нещо подобно на много езици. С едни ще е по-добре, а с други по-зле.
Аз имам 2 решения. Лошото е, че се получават различни отговори (с поне едно възможно класиране) и затова ми е интересно да видя и други разсъждения.

[pal702004]

1 арко
2 вест
3 брик
4 грош
5 доро

Peyo, твърдението "Арко ще финишира втори, а веднага след него ще бъде Вест." не е равносилно на "Арко ще финишира втори, а Вест - трети"

[ins-]

И аз получих същото като pal702004.

Задачата е от олимпиада - 1-ви кръг - 2005 г.

"От второто и четвъртото твърдение следва, че или Грош е четвърти или че Арко е втори и Вест е първи. ( 1 т.) І случай. Нека Грош е четвърти. Тогава Арко не е втори и от петото твърдение следва , че Вест е трети."

Това е откъс от официалното решение. Мисля, че има грешка в това, че от 5-тото твърдение не следва, че Вест е трети.

Следва пълното решение, дадено от авторите на темата:

От второто и четвъртото твърдение следва, че или Грош е четвърти или че Арко е втори и Вест е първи. ( 1 т.) І случай. Нека Грош е четвърти. Тогава Арко не е втори и от петото твърдение следва , че Вест е трети. Тогава в първата прогноза е вярно, че Доро е първи и остава Арко да е последен. Следователно конете са финиширали в реда: Доро, Брик, Вест, Грош, Арко. (3 т.) ІІ случай. Нека Арко е втори и Вест е първи, а Грош не е четвърти. Тогава от третата прогноза следва, че Доро е пети. За твърденията в първата прогноза получаваме,че и първата и втората част не са верни, което е невъзможно. (3 т.)

[peyo]

1 арко
2 вест
3 брик
4 грош
5 доро

Peyo, твърдението "Арко ще финишира втори, а веднага след него ще бъде Вест." не е равносилно на "Арко ще финишира втори, а Вест - трети"

Ааa! Мерси pal702004! Моя грешка тук. Правилното кодиране на проблема в Z3 е следното:

Код: Избери целия код

   from z3 import *
   Arko, Brik, Vest, Grosh, Doro = Ints("Arko, Brik, Vest, Grosh, Doro")
   Eq = [
      Or(And(Doro != 1 , Vest == 2), And(Doro == 1 , Vest != 2)),
      Or(And(Arko != 2 , Grosh== 4), And(Arko == 2 , Grosh != 4)),
      Or(And(Vest != 3 , Doro == 5), And(Vest == 3 , Doro != 5)),
      Or(And(Vest != 1 , Grosh== 4), And(Vest == 1 , Grosh != 4)),
      Or(And(Arko != 2 , Vest == Arko +1), And(Arko == 2 , Vest != Arko +1)),
   ]
   solve( Eq )

[Doro = 5, Arko, = 1, Vest, = 2, Grosh, = 4]

Както виждаме освен, чe съм променил последния ред на условията, трябваше и да сменя Or и And операторите с функции. И така получихме същия отговор като pal702004.

[peyo]

Какво е Z3? Ако правилно разбирам кода - би могло да се напише нещо подобно на много езици. С едни ще е по-добре, а с други по-зле.
Аз имам 2 решения. Лошото е, че се получават различни отговори (с поне едно възможно класиране) и затова ми е интересно да видя и други разсъждения.

Z3 e generic problem solver, но точно: https://en.wikipedia.org/wiki/Z3_Theorem_Prover. Доста удобен за ползване от Python.

[ins-]

[Doro = 5, Arko, = 1, Vest, = 2, Grosh, = 4] - липсва, че Брик е на 3-то място, но то се подразбира.

[peyo]

[Doro = 5, Arko, = 1, Vest, = 2, Grosh, = 4] - липсва, че Брик е на 3-то място, но то се подразбира.

А, вярно! Z3 е малко капризен явно.