All about Programming Theories (18) 썸네일형 리스트형 SAT(Boolean Satisfiability Problem) ※ 이 글은 chatGPT를 기반으로 작성한 글입니다. ※ Coursera의 Automated Reasoning: satisfiability 강의를 기반으로 작성한 글입니다. ① SAT는 수리논리학에서 중요한 개념으로 명제 논리의 만족 가능성(Satisfiability in Propositional Logic) 문제를 나타낸다. ㉠ 즉 SAT 문제는 주어진 명제 논리 공식에 대해 그 공식을 참으로 만드는 변수 값이 존재하는 지를 확인하는 것이다. ② SAT 문제의 특징은 다음과 같다. ㉠ 공식이 만족 가능(satisfiable)하다는 것은 그 공식이 참이 되도록 하는 변수 값이 존재한다는 것이다. ㉡ 공식이 비만족 가능(unsatisfiable)하다는 것은 어떤 변수 값을 할당해도 공식을 참으로 만들 수.. 명제 공식(Propositional Formula) ※ 이 글은 chatGPT를 기반으로 작성한 글입니다. ※ Coursera의 Automated Reasoning: satisfiability 강의를 기반으로 작성한 글입니다. ① 명제 공식(propositional formula)은 수리논리학에서 상요되는 기호와 연산자들로 구성된 식이다. ㉠ 주로 명제 논리에서 상용되며, 간단한 명제들과 논리 연산자를 사용하여 복잡한 명제를 구성한다. ② 명제 공식의 기본 구성 요소는 다음과 같다. ㉠ 원자 명제(Atomic Propositions)는 가장 기본적인 명제로, 추가적인 분해가 불가능하다. 예를 들어 P, Q, R과 같은 단일 문자들이 사용될 수 있다. ㉡ 논리 연산자(Logical Operatos)는 기본 명제들을 결합하거나 변형하는 데 사용된다. ⓐ 부정.. 결정 문제(Decision Problem)와 결정적 알고리즘(Deterministic Algorithm) 그리고 최적화 문제 ※ 이 글은 chatGPT를 기반으로 작성한 글입니다. 결정 문제와 비결정 문제 ① 결정 문제(Decision Problem)는 주어진 문제에 대해 '예' 또는 '아니오'로 답할 수 있는 문제를 의미한다. ② 결정 문제에 대한 예시는 다음과 같다. ㉠ 소수 결정 문제(Prime Decision Problem) ⓐ 질문: n=7은 소수인가? ⓑ 답: yes ㉡ 그래프 연결성 결정 문제(Graph Connectivity Decision Problem) ⓐ 질문: 주어진 그래프가 연결되어 있는가? ⓑ 답: yes or no ㉢ 해밀턴 경로 문제(Hamiltonian Path Problem) ⓐ 질문: 주어진 그래프 내에서 모든 정점을 정확히 한 번씩 방문하는 경로가 존재하는가? ⓑ 답: yes or no ㉣ .. SAT(Boolean Satisfiability Problem)와 SMT(Satisfiability Modulo Theories) ※ 이 글은 chatGPT를 기반으로 작성한 글입니다. ※ Coursera의 Automated Reasoning: satisfiability 강의를 기반으로 작성한 글입니다. ① SAT(Boolean Satisfiability Problem)는 가장 기본적인 결정 문제(determinant problem) 중 하나로, 주어진 불리언(참/거짓) 논리식이 참인 값을 가질 수 있는지를 판별하는 문제다. ② SAT 문제에서는 논리식이 불리언 변수로 구성된다. 이 변수들은 AND, OR, NOT 등의 불리언 연산자로 연결된다. ③ SAT를 이용해 회로 설계 검증, 소프트웨어 검증, 암호학 등에서 사용할 수 있다. ④ SAT 문제를 해결하기 위해 개발된 알고리즘 중 가장 유명한 게 DPLL(Davis-Putnam-.. Seach-Based Fuzzing ※ 이 글은 chatGPT를 기반으로 작성한 글입니다. Search-Based Fuzzing - The Fuzzing Book Sometimes we are not only interested in fuzzing as many as possible diverse program inputs, but in deriving specific test inputs that achieve some objective, such as reaching specific statements in a program. When we have an idea of what we are looking for www.fuzzingbook.org Intro ① 다양한 프로그램 입력으로 퍼징(Fuzzing)을 수행하는 것뿐만 아니라 프로.. 버퍼(Buffer) ※ 이 글은 chatGPT를 기반으로 작성한 글입니다. ① 버퍼(buffer)는 데이터가 한 장소에서 다른 장소로 전송되는 동안 일시적으로 보관하는데 사용하는 임시 저장 공간이다. ㉠ 시스템의 다른 공간으로 데이터를 이동시킬 때 버퍼를 거쳐 감으로써 걸리는 시간을 줄이는 것으로 컴퓨터 성능을 높여준다. ㉡ 버퍼는 수신 장치 또는 응용 프로그램에서 데이터를 처리할 수 있을 때까지 데이터를 저장하는 데 사용된다. ② 버퍼는 다음의 상황에서 사용한다. ㉠ 입출력 버퍼링(Input/Output buffering) : 네트워크 통신이나 파일로부터 데이터가 들어올 때, 프로그램이 처리하기 전 버퍼를 거친다. ㉡ 그래픽 랜더링(graphics rendering) : 애니메이션 프레임을 화면에 출력하기 전에 버퍼를 거.. 버퍼 플러시(Buffer flush) 6. Linux - 스크립트 및 자동화 ※ 이 글은 chatGPT를 기반으로 작성한 글입니다. 이전 1 2 3 다음
