NDLI: Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

Content Provider	ACM Digital Library
Author	Nieuwenhuis, Robert Oliveras, Albert Tinelli, Cesare
Copyright Year	2006
Abstract	We first introduce Abstract DPLL, a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason about them in a simple way. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as backjumping or clause learning.We then extend the framework to Satisfiability Modulo background Theories (SMT) and use it to model several variants of the so-called lazy approach for SMT. In particular, we use it to introduce a few variants of a new, efficient and modular approach for SMT based on a general $DPLL(\textit{X})$ engine, whose parameter $\textit{X}$ can be instantiated with a specialized solver $Solver_{T}$ for a given theory $\textit{T},$ thus producing a $DPLL(\textit{T})$ system. We describe the high-level design of $DPLL(\textit{X})$ and its cooperation with $Solver_{T},$ discuss the role of theory propagation, and describe different $DPLL(\textit{T})$ strategies for some theories arising in industrial applications.Our extensive experimental evidence, summarized in this article, shows that $DPLL(\textit{T})$ systems can significantly outperform the other state-of-the-art tools, frequently even in orders of magnitude, and have better scaling properties.
Starting Page	937
Ending Page	977
Page Count	41
File Format	PDF
ISSN	00045411
e-ISSN	1557735X
DOI	10.1145/1217856.1217859
Journal	Journal of the ACM (JACM)
Volume Number	53
Issue Number	6
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2006-11-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	SAT solvers Satisfiability Modulo Theories
Content Type	Text
Resource Type	Article
Subject	Hardware and Architecture Information Systems Control and Systems Engineering Artificial Intelligence Software

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

Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T (2006)

Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T (2006)

A first-order logic davis-putnam-logemann-loveland procedure.

OPTSAT: A Tool for Solving SAT related optimization problems (2006)

Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT

How good are branching rules in DPLL? (1996)

Overcoming Resolution-Based Lower Bounds for SAT Solvers (2002)

First-order logic Davis-Putnam-Logemann-Loveland procedure

Restart method and exponential acceleration of random 3-sat instances resolutions: a large deviation analysis of the davis–putnam–loveland–logemann algorithm (2002).

Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

Similar Documents

Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T (2006)

Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T (2006)

A first-order logic davis-putnam-logemann-loveland procedure.

OPTSAT: A Tool for Solving SAT related optimization problems (2006)

Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT

How good are branching rules in DPLL? (1996)

Overcoming Resolution-Based Lower Bounds for SAT Solvers (2002)

First-order logic Davis-Putnam-Logemann-Loveland procedure

Restart method and exponential acceleration of random 3-sat instances resolutions: a large deviation analysis of the davis–putnam–loveland–logemann algorithm (2002).

Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)