Thumbnail
Access Restriction
Subscribed

Author Toda, Takahisa ♦ Soh, Takehide
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2016
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Computer programming, programs & data
Subject Keyword AllSAT solvers ♦ BDD ♦ CNF to DNF conversion ♦ Blocking clause ♦ Conflict-directed backjumping ♦ Formula caching ♦ Knowledge compilation ♦ Model enumeration
Abstract All solutions SAT (AllSAT for short) is a variant of the propositional satisfiability problem. AllSAT has been relatively unexplored compared to other variants despite its significance. We thus survey and discuss major techniques of AllSAT solvers. We accurately implemented them and conducted comprehensive experiments using a large number of instances and various types of solvers including a few publicly available software. The experiments revealed the solvers’ characteristics. We made our implemented solvers publicly available so that other researchers can easily develop their solvers by modifying our code and comparing it with existing methods.
Description Author Affiliation: University of Electro-Communications, Tokyo, Japan (Toda, Takahisa); Kobe University, Nada Kobe, Japan (Soh, Takehide)
ISSN 10846654
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2016-11-04
Publisher Place New York
e-ISSN 10846654
Journal Journal of Experimental Algorithmics (JEA)
Volume Number 21
Page Count 44
Starting Page 1
Ending Page 44


Open content in new tab

   Open content in new tab
Source: ACM Digital Library