Presentation 2006-05-18
Preprocessing SAT Problems with Abstract Models
Miyuki KOSHIMURA, Ryuzo HASEGAWA,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) We presented an simplification (pre-processing) method for the first-order CNF formula. The method makes use of an abstraction of the formula. We aimed to enhance the performance of automated theorem provers with the method. This paper applies the method to the prepositional CNF formula (SAT problem) and evaluates its effect for the problems from SATLIB.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) CNF formula / abstraction / simplification / SAT
Paper # AI2006-5
Date of Issue

Conference Information
Committee AI
Conference Date 2006/5/11(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Artificial Intelligence and Knowledge-Based Processing (AI)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) Preprocessing SAT Problems with Abstract Models
Sub Title (in English)
Keyword(1) CNF formula
Keyword(2) abstraction
Keyword(3) simplification
Keyword(4) SAT
1st Author's Name Miyuki KOSHIMURA
1st Author's Affiliation Graduate School of Information Science and Electrical Engineering, Kyushu University()
2nd Author's Name Ryuzo HASEGAWA
2nd Author's Affiliation Graduate School of Information Science and Electrical Engineering, Kyushu University
Date 2006-05-18
Paper # AI2006-5
Volume (vol) vol.106
Number (no) 38
Page pp.pp.-
#Pages 4
Date of Issue