NDLI: A New Exact Bit-Parallel Algorithm for SAT

Content Provider	IEEE Xplore Digital Library
Author	San Segundo, P. Tapia, C. Puente, J. Rodriguez-Losada, D.
Copyright Year	2008
Description	Author affiliation: Intell. Control Group, Univ. Politec. de Madrid, Madrid (San Segundo, P.; Tapia, C.; Puente, J.; Rodriguez-Losada, D.)
Abstract	This paper presents two new exact general purpose bit-parallel algorithms (BB-SAT and BBP-SAT) for the Boolean satisfiability problem (SAT). Based on the authors' recent successful bit-parallel algorithm for the maximum clique problem, the SAT formula is first reduced to a directed graph which is then bit encoded. As a result, search traverses a bit vector graph space. At present the encoding allows for an efficient bitwise computation of graph state transitions as well as unit clause and pure literal evaluation. Experiments carried out on a number of DIMACS instances are highly encouraging since BBP-SAT is already reasonably competitive employing just basic DPLL tactics with minor refinements. BBP-SAT is a fresh approach in an otherwise mature domain. Further additional bit encoded knowledge of the more recent successful SAT algorithms (e.g. bit parallel heuristic variable selection) should make BBP-SAT a competitive general purpose solver.
Starting Page	59
Ending Page	65
File Size	391831
Page Count	7
File Format	PDF
ISBN	9780769534404
ISSN	10823409
DOI	10.1109/ICTAI.2008.127
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2008-11-03
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Encoding Artificial intelligence Intelligent control Input variables Art Programming profession Data mining NP-complete problem Data structures Parallel processing Boolean satisfiability SAT bit vector bit-parallelism exact algorithms directed graphs
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Heuristic backtracking algorithms for SAT

FPGA-Based SAT Solver

A Hardware Accelerator for SAT Solving

An Improved Semidefinite Programming Relaxation for the Satisfiability Problem (2002)

Extended Finite-State Machine Induction Using SAT-Solver

Boolean satisfiability for sequence mining said jabbour.

A Tree Decomposition Based Approach to Solve Structured SAT Instances

Boolean function manipulation on massively parallel computers

Learning for Dynamic Assignments Reordering

A New Exact Bit-Parallel Algorithm for SAT

Similar Documents

Heuristic backtracking algorithms for SAT

FPGA-Based SAT Solver

A Hardware Accelerator for SAT Solving

An Improved Semidefinite Programming Relaxation for the Satisfiability Problem (2002)

Extended Finite-State Machine Induction Using SAT-Solver

Boolean satisfiability for sequence mining said jabbour.

A Tree Decomposition Based Approach to Solve Structured SAT Instances

Boolean function manipulation on massively parallel computers

Learning for Dynamic Assignments Reordering

A New Exact Bit-Parallel Algorithm for SAT