zebra
1.0.0
2024년 현재, 프로젝트는 대부분 유지 관리되지 않습니다. 나는 그것을 시도하고 싶은 몇 가지 작업을 위한 놀이터로 사용하고 있지만 누구에게도 이것을 구축하는 것을 권장하지 않습니다.
이렇게 생긴 논리 퍼즐을 기억하시나요? 그들은 다음과 같은 단서를 갖고 있었습니다.
투샤르(Tushar)와 마우이(Maui) 사이에는 집이 하나 있습니다.
루비가 가장 좋아하는 비디오 게임은 포켓몬입니다.
차이를 마시는 사람은 파란색을 좋아하지 않습니다.
저는 어렸을 때 이것을 좋아했고, Raymond Hettinger의 PyCon 2019 강연을 보면서 이러한 문제를 다시 생각해 보게 되었습니다. 그는 우리에게 문제를 해결하는 방법을 보여주었습니다. 나는 그것들을 생성하는 방법을 배우고 싶었습니다.
최신 Python 및 SAT(제약 만족) 솔버를 사용하여 이 프로젝트를 사용하여 임의의 얼룩말 퍼즐을 만들 수 있습니다.
이 프로젝트는 Python 3.12와 Poetry를 사용합니다.
이 프로젝트의 진입점은 src/main.py 입니다. 따라서 [poetry run] python -m src.main 으로 실행하세요. 간단한 상호 작용이 가능한 CLI를 생성하기 위해 질문을 사용합니다.
기타 중요한 파일은 다음과 같습니다.
puzzle.py 에는 주로 단서와 퍼즐 요소를 연결하는 주요 Puzzle 클래스가 포함되어 있습니다.
clues.py 단서(CNF로 변환할 수 있는 상위 수준 명령문)와 found_at 또는 same_house 와 같은 여러 팩토리를 정의합니다. generate.py 에는 단서를 생성하는 유틸리티가 있습니다.
elements.py 및 traptor_elements.py 에는 다양한 퍼즐 요소가 있습니다.
마지막으로 sat_utils.py 에는 SAT 솔버 pycosat와 상호 작용하기 위한 기본 유틸리티가 포함되어 있습니다. 이 코드는 Raymond Hettinger가 2019년 강연을 위해 거의 전부 작성했습니다(감사합니다!).
❯ 시 실행 python -m src.main? 퍼즐의 크기는 얼마나 됩니까? (화살표 키를 사용하세요)
» 5
4
3? 트랩터 유형 선택(화살표 키 사용)
? 열렬한
» ? 신화적인가? ? 퍼즐에 스무디가 포함되어야 하나요? (화살표 키를 사용하세요)
" 예
아니요? ? 퍼즐에 병뚜껑이 포함되어야 하나요? (화살표 키를 사용하세요)
" 예
아니요
단서
-----# ... 일부 플레이버 텍스트가 생략되었습니다 ...1. 하급 트랩터와 늪 트랩터는 같은 집에 있습니다.
2. 고대 사냥꾼은 초콜릿 스무디 바로 왼쪽에 있습니다.
3. 고대 트랩터와 레몬 스무디가 같은 집에 있습니다.
4. 화산 함정은 불안한 함정의 바로 왼쪽에 있습니다.
5. 동굴 사냥꾼과 녹색 병뚜껑은 같은 집에 있습니다.
6. Lake Traptor와 Snapper Traptor 사이에는 두 개의 집이 있습니다.
7. 녹색 병뚜껑과 맹렬한 덫이 같은 집에 있습니다.
8. 블랙병뚜껑과 코코넛 스무디 사이에 집이 하나 있어요.
9. 레서 트랩터와 키위 스무디 사이에는 집이 하나 있습니다.
10. 드웰러 트랩터와 초콜릿 스무디가 같은 집에 있어요.
11. 빨간 병뚜껑과 드웰러 트랩터가 같은 집에 있습니다.
12. 빨간색 병뚜껑은 Hoarder Traptor 바로 왼쪽에 있습니다.
13. 스타프루트 스무디와 노란병뚜껑 사이에 집이 두 개 있어요.
14. 레이크 트랩터와 블랙 병뚜껑은 같은 집에 있습니다.
15. 스토커 트랩터와 맹렬한 트랩터가 같은 집에 있습니다.
해결책
┏━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━ ━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━┓
┃ 네스트 ┃ MythicalTraptorPrimary ┃ MythicalTraptorSecondary ┃ MythicalTraptorTertiary ┃ 스무디 ┃ 병뚜껑 ┃
┡━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━ ━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━┩
│ 1 │ 맹렬한 함정 │ 동굴 함정 │ 추적자 함정 │ 스타프루트 스무디 │ 녹색 병뚜껑 │
│ 2 │ 고대 트랩터 │ 호수 트랩터 │ 크롤러 트랩터 │ 레몬 스무디 │ 검은색 병뚜껑 │
│ 3 │ 하급 트랩터 │ 늪 트랩터 │ 드웰러 트랩터 │ 초콜릿 스무디 │ 빨간색 병뚜껑 │
│ 4 │ 그레이터 트랩터 │ 화산 트랩터 │ 호더 트랩터 │ 코코넛 스무디 │ 노란색 병뚜껑 │
│ 5 │ 불안한 함정 │ 산의 함정 │ 도미 사냥꾼 │ 키위 스무디 │ 파란색 병뚜껑 │
└──────┴───────────────────────┴───────────────── ─────────┴───── ────────────────────┴───────────────────────┴──── ───────────────┘2024년 2월에 이 작업이 '완료'되었다고 간주하려면 무엇이 필요합니까?
HTML 템플릿을 추가합니다. 왜냐하면 제가 이를 구축하는 사이트에서는 BR 태그와 같은 항목을 포함해야 하기 때문입니다.
플레이버 텍스트의 대문자 사용과 같이 출력의 문법 니트를 개선합니다.
제출물에 복사/붙여넣기한 머리글/바닥글 리소스를 추가합니다.
아마도 언젠가는 웹 인터페이스를 고려하게 될 것입니다. pyodide를 사용하여 프로젝트를 들어 올릴 수 있습니까? 아니면 C 기반 pycosat이 문제를 일으킬 수 있습니까? PySAT, 응답 세트 프로그래밍 또는 이 HN 스레드의 다른 논리 프로그래밍 인터페이스는 어떻습니까?
이런 일이 발생할 수 있습니다. 하지만 프로젝트가 마침내 제가 만족할 만한 수준에 도달했기 때문에 이에 대해 공유하고 글을 쓰게 되어 기쁩니다.
2/18: 출력을 더 단순하고, 덜 장황하고, 더 예쁘게 만듭니다. 새로운 형식과 변경 사항으로 이 README를 업데이트하세요. 마침내 퍼즐 생성기를 사용하여 새로운 퍼즐을 만들어보세요!
2/17: 솔루션만 허용하고 솔루션에서 요소와 요소 클래스를 추론하도록 퍼즐 서명을 업데이트합니다. 솔루션에 대해 더 멋진 디스플레이를 추가하십시오.
11/26: 퍼즐/솔루션 생성 로직을 정리합니다. 사용자가 퍼즐 크기를 선택하게 하세요.
11/25: 몇 가지 일반적인 유형의 이름을 유형 별칭으로 지정합니다(Python 3.12 덕분에). 인쇄 대신 로깅을 사용하십시오.
generate.py 내에 단서 유형에 대한 테스트를 추가하세요.
clues.py 에 소개한 버그를 수정하세요. 해당 파일은 이해하기가 너무 어렵지만 단위 테스트를 작성하기도 어렵습니다. 부울 표현식을 CNF로 직접 변환하는 것은 재미가 없습니다.
솔루션에서 단서의 가중치를 조정합니다. 퍼즐과 풀이 수업을 통합할 준비를 하세요.
체크박스 같은 스무디 선택을 제거하세요. 퍼즐을 빨리 만들려고 할 때 방해가 되기 때문입니다.
계속해서 테스트를 추가하세요. sat_utils.py 에 대한 단위 테스트를 완료하고 clues.py 에 대한 몇 가지 테스트를 시작합니다. 하지만 해당 파일은 DNF에서 CNF로의 변환을 직접 계산하는 것이 어렵기 때문에 테스트하기가 매우 어렵습니다.
다음 단계는 퍼즐과 솔루션을 통합하고, 더 나은 __repr__ 만들고, 퍼즐 크기를 표현하는 방법을 단순화하는 것입니다( Puzzle 의 속성, 1에서 N까지의 정수 튜플, 숫자 n_houses 등).
검은색을 제거하고 러프를 사용하여 포맷합니다. 종속성을 업데이트합니다. 더 간단하고 명확한 사용법으로 새로운 CLI를 추가하세요. python -m src.main .
SATLiteral -> PuzzleElement (스무디, 고양이 등)의 이름을 바꿉니다. 이는 부울 의미의 리터럴이 아니며 대신 퍼즐의 문자와 같은 이름임을 명확히 합니다.
새로운 유형의 SATLiteral (트렌치코트의 str )을 생성합니다. 이는 " el 값이 house loc 에 있음" 또는 " el 값이 house loc 에 없음"과 같은 부울 변수 의미의 리터럴을 나타냅니다. 내부적으로 이는 정수 i 와 음수 대응물인 -i 로 표시됩니다.
(새로운) SATLiteral comb(el: str, loc: int) -> SATLiteral 의 반환 유형으로 사용하고, 퍼즐 요소를 리터럴에 매핑하고, neg(el: SATLiteral) -> SATLiteral 사용하여 리터럴을 부정합니다.
Clause: tuple[SATLiteral, ...] ; 예를 들어, (1, -5, 6) x_1 이 참, x_5 참이 아니거나 x_6 이 참임을 나타내는 분리입니다.
ClueCNF: list[Clause] 추가합니다. 이는 Clause s의 "∧"(부울 AND; 접속사)를 나타냅니다. CNF의 퍼즐은 "AND of OR"("∧ of ∨s" 또는 "∧ of Clauses")입니다.
퍼즐을 더 명확하게 인쇄하세요. 단서 감소의 장황함을 줄입니다.
각 실행마다 무작위로 퍼즐(시드 포함)을 생성합니다.
예제를 자체 파일로 이동합니다. Python 3.12(베타)로 업데이트합니다. 린트 규칙을 더 추가하세요. 수입품을 정리하세요.
개발 도구 추가(검정색, 러프, 파이라이트) 사전 커밋에서 Black & Ruff를 실행합니다. 일부 유형을 업데이트합니다.
"∧"는 부울 AND입니다.
"∨"는 부울 OR입니다.
절은 "리터럴의 ∨"입니다.
CNF는 "∧ of Clauses" 또는 "∧ of ∨s"("AND of ORs")와 동일합니다.
대조적으로 DNF는 "∨ of ∧s"입니다. DNF는 SAT 문제에 대한 답 입니다. "A 또는 B 또는 C"의 DNF는 A, B 및 C가 모두 유효한(만족스러운) 할당임을 읽습니다. 따라서 CNF를 DNF로 변환하는 것은 NP 하드입니다. 왜냐하면 DNF에서 CNF에 대한 솔루션을 읽을 수 있기 때문입니다.
CNF는 ∨s의 ∧입니다. 여기서 ∨는 변수 또는 해당 부정(리터럴)에 대한 것입니다. 리터럴의 ∨는 절이라고도 합니다. DNF는 ∧의 ∨입니다. 리터럴의 ∧를 용어라고 합니다.
이 프로젝트의 핵심은 얼룩말 퍼즐을 SAT( Boolean Satisfiability ) 문제로 표현하는 것입니다(Wikipedia.
3-SAT 문제는 NP-완전 문제로 알려져 있습니다. 즉, 이를 해결하는 다항식 시간 알고리즘이 없을 가능성이 높습니다. 하지만 이는 일반적인 경우에만 설명됩니다.
우리의 문제는 작고 잘 명시되어 있습니다(결국 우리는 인간을 위해 특별히 이러한 문제를 만들고 있습니다!). 이는 현대 SAT 해결사에게 매우 적합하며 Hettinger의 강연(및 메모)은 이를 아름답게 보여줍니다.
