NDLI: The Road to Improving the Performance of Satisfiability Solvers Using HPC

Content Provider	IEEE Xplore Digital Library
Author	Ezick, J. Lethin, R.
Copyright Year	2007
Description	Author affiliation: Reservoir Labs, New York (Ezick, J.; Lethin, R.)
Abstract	Boolean satisfiability (SAT) solvers have become an enabling technology for diverse application areas of military and commercial interest. A Phase II Small Business Innovation Research project under the architectures for cognitive information processing (ACIP) program has developed novel problem representations, algorithms, and heuristics to improve SAT solver performance over existing approaches. Reservoir Labs has parallelized a SAT solver for the Cray XD1, writing fine grained messaging layers over Message Passing Interface (MPI). The solver is written in a message-driven computing style. We partition the problem over the nodes of the XD1 to achieve concurrency in the propagation of implications. We have facilities to partition the clause database over the nodes to improve locality of reference. A tool, Salt, can translate a high level logic language into SAT problem instances and transmit partition and heuristic information into the solver. We report on the current capability and performance of the solver, and in particular the tradeoff between locality and concurrency in our system. Finally, we point to the forward roadmap to achieving greater performance on this problem.
Starting Page	410
Ending Page	413
File Size	135751
Page Count	4
File Format	PDF
ISBN	9780769530885
DOI	10.1109/HPCMP-UGC.2007.74
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2007-06-18
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Concurrent computing Technological innovation Databases Heuristic algorithms Message passing Information processing Writing Reservoirs Partitioning algorithms Business
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

Performance analysis of algorithms on a message passing multiprocess

Dynamic Load Balancing Algorithm for MPI Parallel Computing

Checking Non-divergence, Channel-Bound and Global Cooperation Using SAT-Solvers

Improving the performance of a parallel data mining algorithm using communication message scheduling

Performance of distributed memory methods in multiprocessing clusters

PMRSB: Parallel Multilevel Recursive Spectral Bisection

Optimizing Message Passing Programs Based on Task Section Duplication

Parallel compact WY QR factorization for asynchronous message passing

Programming models for petascale to exascale

The Road to Improving the Performance of Satisfiability Solvers Using HPC

Similar Documents

Performance analysis of algorithms on a message passing multiprocess

Dynamic Load Balancing Algorithm for MPI Parallel Computing

Checking Non-divergence, Channel-Bound and Global Cooperation Using SAT-Solvers

Improving the performance of a parallel data mining algorithm using communication message scheduling

Performance of distributed memory methods in multiprocessing clusters

PMRSB: Parallel Multilevel Recursive Spectral Bisection

Optimizing Message Passing Programs Based on Task Section Duplication

Parallel compact WY QR factorization for asynchronous message passing

Programming models for petascale to exascale

The Road to Improving the Performance of Satisfiability Solvers Using HPC