NDLI: A Variational Method for Analysing Unit Clause Search

Content Provider	Society for Industrial and Applied Mathematics (SIAM)
Author	Mjean, Henri-M. Morel, Henri Reynaud, Grard
Copyright Year	1995
Abstract	We expose a variational method for analysing algorithms, as applied to analyse the algorithm $\textbf{UC}$, which is the Davis-Putnam procedure for a set of clauses of three literals. The variable from a unit clause or, if there is none, the first remaining variable from a fixed list is chosen. The algorithm $\textbf{UC}$ finds all the solutions as a set of cylinders. Following the nomenclature of Purdom [J. Inform. Process., 13 (1990), pp. 449455], we call this algorithm unit clause backtracking with cylinders of solutions.First we give an expression for the number of nodes of the calculation trees of all the inputs. Then we use a variational method to calculate the base $\beta $ of the principal exponential part of the average time of calculation T. This exponential base is the maximum of three elementary functions $f_{i}$ of four real variables, These functions are defined on the product of the half positive real line by the 3-dimensional unit real cube. We finally obtain the following short statement. Let v be the number of the variables. Let c be the number of the clauses. Let $\gamma = \frac{c}{v} > 1$. Let $\gamma $ be constant when v grows to infinity. The principal exponential part of the average time of $\textbf{UC}$ is $\beta^{v}$ where \[ \beta = \max\limits_{0 \leq \lambda \leq 1} 2^{\lambda} \left( 1 - \frac{3\lambda ^{2}}{8} + \frac{\lambda ^{3}}{4} \right)^{\gamma}. \]We mean that $\lim_{v \rightarrow \infty} T^{1/v} =\beta $.As a first consequence of our method we match $\textbf{UC}$, with the algorithm $\textbf{B}$ without rearrangement (i.e., with a fixed order for introducing the variables). This gives a proof to a conjecture of P W. Purdom [Artif. Intell., 21(1983), pp. 117133].
Starting Page	621
Ending Page	649
Page Count	29
File Format	PDF
ISSN	00975397
DOI	10.1137/S0097539792230484
e-ISSN	10957111
Journal	SIAM Journal on Computing (SMJCAT)
Issue Number	3
Volume Number	24
Language	English
Publisher	Society for Industrial and Applied Mathematics
Publisher Date	2006-07-13
Access Restriction	Subscribed
Subject Keyword	variational methods analysis of algorithms satisfiability computational complexity
Content Type	Text
Resource Type	Article
Subject	Mathematics Computer Science

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