Improved single pass algorithms for resolution proof reduction

Gupta A. 2012. Improved single pass algorithms for resolution proof reduction. 10th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 7561, 107–121.

Download
OA 2012_ATVA_Gupta.pdf 465.50 KB [Submitted Version]

Conference Paper | Published | English

Scopus indexed

Corresponding author has ISTA affiliation

Series Title
LNCS
Abstract
Unsatisfiability proofs find many applications in verification. Today, many SAT solvers are capable of producing resolution proofs of unsatisfiability. For efficiency smaller proofs are preferred over bigger ones. The solvers apply proof reduction methods to remove redundant parts of the proofs while and after generating the proofs. One method of reducing resolution proofs is redundant resolution reduction, i.e., removing repeated pivots in the paths of resolution proofs (aka Pivot recycle). The known single pass algorithm only tries to remove redundancies in the parts of the proof that are trees. In this paper, we present three modifications to improve the algorithm such that the redundancies can be found in the parts of the proofs that are DAGs. The first modified algorithm covers greater number of redundancies as compared to the known algorithm without incurring any additional cost. The second modified algorithm covers even greater number of the redundancies but it may have longer run times. Our third modified algorithm is parametrized and can trade off between run times and the coverage of the redundancies. We have implemented our algorithms in OpenSMT and applied them on unsatisfiability proofs of 198 examples from plain MUS track of SAT11 competition. The first and second algorithm additionally remove 0.89% and 10.57% of clauses respectively as compared to the original algorithm. For certain value of the parameter, the third algorithm removes almost as many clauses as the second algorithm but is significantly faster.
Publishing Year
Date Published
2012-09-28
Proceedings Title
10th International Symposium on Automated Technology for Verification and Analysis
Publisher
Springer Nature
Acknowledgement
This work was supported by the ERC Advanced Investigator grant on Quantitative Reactive Modeling (QUAREM).
Volume
7561
Page
107-121
Conference
ATVA: Automated Technology for Verification and Analysis
Conference Location
Thiruvananthapuram, Kerala, India
Conference Date
2012-10-03 – 2012-10-06
ISSN
eISSN
IST-REx-ID

Cite this

Gupta A. Improved single pass algorithms for resolution proof reduction. In: 10th International Symposium on Automated Technology for Verification and Analysis. Vol 7561. Springer Nature; 2012:107-121. doi:10.1007/978-3-642-33386-6_10
Gupta, A. (2012). Improved single pass algorithms for resolution proof reduction. In 10th International Symposium on Automated Technology for Verification and Analysis (Vol. 7561, pp. 107–121). Thiruvananthapuram, Kerala, India: Springer Nature. https://doi.org/10.1007/978-3-642-33386-6_10
Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” In 10th International Symposium on Automated Technology for Verification and Analysis, 7561:107–21. Springer Nature, 2012. https://doi.org/10.1007/978-3-642-33386-6_10.
A. Gupta, “Improved single pass algorithms for resolution proof reduction,” in 10th International Symposium on Automated Technology for Verification and Analysis, Thiruvananthapuram, Kerala, India, 2012, vol. 7561, pp. 107–121.
Gupta A. 2012. Improved single pass algorithms for resolution proof reduction. 10th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 7561, 107–121.
Gupta, Ashutosh. “Improved Single Pass Algorithms for Resolution Proof Reduction.” 10th International Symposium on Automated Technology for Verification and Analysis, vol. 7561, Springer Nature, 2012, pp. 107–21, doi:10.1007/978-3-642-33386-6_10.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2018-12-18
MD5 Checksum
68415837a315de3cc4d120f6019d752c


Export

Marked Publications

Open Data ISTA Research Explorer

Search this title in

Google Scholar
ISBN Search