[Z3 입문 시리즈] 0. 논리를 푸는 도구, Z3를 소개합니다
Z3는 수식이나 논리를 자동으로 증명하거나, 조건을 만족하는 값을 찾아주는 SMT Solver입니다.정수나 실수 같은 간단한 종류부터 배열, 비트벡터 등 복잡한 구조까지 폭넓게 지원해,형식 검증부터 퍼즐 풀이까지 다양하게 활용할 수 있습니다.1) Z3란?SMT(Satisfiability Modulo Theories)라는 개념에 기반한 솔버입니다.논리식의 참/거짓만 따지는 SAT(참/거짓 문제)에서 더 나아가,정수, 실수, 배열, 비트벡터 같은 수학적 이론까지 고려해 “만족 가능한 해가 있나?”를 찾습니다.마이크로소프트 리서치에서 만들었고 오픈소스로 공개되어 있어,형식 검증이나 프로그램 분석 등 다양한 분야에서 두루 활용됩니다.2) 왜 Z3를 써야 하는가?한 번 제약을 써넣기만 하면, Z3가 알아서 해를 ..
2025. 4. 4.
[ISSUE][용어] 로앤비 판결
"로엔비 판결"이란, 법령이나 판결문처럼 누구나 쓸 수 있는 공공정보를 그저 모아놓은 게 아니라, 쓰기 편하게 잘 정리하고 분류해서 새로운 형태로 만든 데이터베이스는 저작권으로 보호받을 수 있다고 한 판결입니다. 쉽게 말해, 공짜 자료라도 ‘어떻게 새롭게 정리하고 구성하느냐’에 따라 그 결과물에 대한 법적 보호가 달라진다는 뜻입니다. 로앤비(Law&Business)는 법령, 판례, 행정해석, 학술논문 등 광범위한 법률정보를 수집하고, 이를 온라인 데이터베이스 형태로 구축하여 유료로 제공하는 법률정보 서비스 기업입니다. 이 과정에서 단순히 국가기관이 발행한 공공자료를 무작위로 나열하는 것이 아니라, 전문 법학자나 변호사의 검수를 거쳐 자료의 중요도, 주제 분야, 관련 법령·판례 간의 상관관계 등을 종합적으..
2024. 12. 16.
