NDLI: A parsimony tree for the SAT2002 competition

Content Provider	Springer Nature Link
Author	Purdom, Paul W. Berre, Daniel Simon, Laurent
Copyright Year	2004
Abstract	Twenty of the programs (solvers) submitted to the SAT 2002 Contest had no disqualifying errors. These solvers were run on 2023 satisfiability problems of varying hardnesses. Each solver was judged by which problems it could solve within the allowed time limit. Twelve solvers were best on some problem — they could solve it and the others could not. Only two solvers could not beat each remaining solver on some problems (where the problems could vary depending on which solver it was trying to beat). Thus, there is evidence that 18 solvers were extremely good. It is interesting to analyze the contest results in a way that groups together solvers with similar strengths and weaknesses. This paper uses the parsimony algorithm to produce a classification of the twenty solvers. The paper also has a second classification, almost the same as the first, for the twenty solvers, updated versions of two solvers, and a fictitious state of the art solver. The contest problems came in three groups, Industrial, Hand Made, and Random. The Random group of problems was about three times as large as the other two together. The classification identifies four groups of solvers (plus a miscellaneous group): weak solvers, incomplete solvers which are very good at some satisfiable Random problems, complete solvers which are very good at most Random problems, and complete solvers which are very good at Industrial and Hand Made problems.
Starting Page	343
Ending Page	365
Page Count	23
File Format	PDF
ISSN	10122443
Journal	Annals of Mathematics and Artificial Intelligence
Volume Number	43
Issue Number	1-4
e-ISSN	15737470
Language	English
Publisher	Springer Netherlands
Publisher Date	2004-12-31
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Boolean satisfiability (SAT) empirical evaluation parsimony Artificial Intelligence (incl. Robotics) Mathematics Computer Science Statistical Physics, Dynamical Systems and Complexity
Content Type	Text
Resource Type	Article
Subject	Applied Mathematics Artificial Intelligence

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

Similar Documents

The SAT2002 competition

UnitWalk: A new SAT solver that uses local search guided by unit clause elimination

Dynamic symmetry-breaking for Boolean satisfiability

Efficient data structures for backtrack search SAT solvers

The complexity of Boolean constraint satisfaction local search problems

Toward leaner binary-clause reasoning in a satisfiability solver

On deciding subsumption problems

Probability logic and optimization SAT: The PSAT and CPA models

Solving the resolution-free SAT problem by submodel propagation in linear time

A parsimony tree for the SAT2002 competition