Toward leaner binary-clause reasoning in a satisfiability solver.

*(English)*Zbl 1099.68097Summary: Binary-clause reasoning has been shown to reduce the size of the search space on many satisfiability problems, but has often been so expensive that run-time was higher than that of a simpler procedure that explored a larger space. The method of Sharir for detecting strongly connected components in a directed graph can be adapted to performing “lean” resolution on a set of binary clauses. Beyond simply detecting unsatisfiability, the goal is to find implied equivalent literals, implied unit clauses, and implied binary clauses.

##### MSC:

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |

PDF
BibTeX
XML
Cite

\textit{A. Van Gelder}, Ann. Math. Artif. Intell. 43, No. 1--4, 239--253 (2005; Zbl 1099.68097)

Full Text:
DOI

##### References:

[1] | Aspvall, B.; Plass, M.; Tarjan, R., A linear-time algorithm for testing the truth of certain quantified Boolean formulas, Information Processing Letters, 8, 121-123, (1979) · Zbl 0398.68042 |

[2] | S. Baase and A. Van Gelder, Computer Algorithms: Introduction to Design and Analysis, 3rd edn (Addison-Wesley, 2000). |

[3] | F. Bacchus, Exploring the computational tradeoff of more reasoning and less searching, in: Proc. of Symposium on the Theory and Applications of Satisfiability Testing, Cincinnati, OH (2002) pp. 7-16. · Zbl 0212.34203 |

[4] | R.J. Bayardo, Jr. and R.C. Schrag, Using CSP look-back techniques to solve real-world SAT instances, in: Proc. of 14th National Conference on Artificial Intelligence (AAAI-97) (1997) pp. 203-208. · Zbl 0443.68046 |

[5] | Billionnet, A.; Sutter, A., An efficient algorithm for the 3-satisfiability problem, Operations Research Letters, 12, 29-36, (1992) · Zbl 0757.90059 |

[6] | T.H. Cormen, C.E. Leiserson, R.L. Rivest and C. Stein, Introduction to Algorithms, 2nd edn (McGraw-Hill, 2001). · Zbl 1047.68161 |

[7] | Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Communications of the ACM, 5, 394-397, (1962) · Zbl 0217.54002 |

[8] | Davis, M.; Putnam, H., A computing procedure for quantification theory, Journal of the Association for Computing Machinery, 7, 201-215, (1960) · Zbl 0212.34203 |

[9] | A. del Val, Simplifying binary propositional theories into connected components twice as fast, in: Proc. of 8th Int’l Conf. on Logic for Programming, Artificial Intelligence and Reasoning (Springer, 2001) pp. 389-403. · Zbl 0784.68077 |

[10] | Lee, S.-J.; Plaisted, D.A., Eliminating duplication with the hyper-linking strategy, Journal of Automated Reasoning, 9, 25-42, (1992) · Zbl 0784.68077 |

[11] | C.M. Li, Integrating equivalency reasoning into Davis-Putnam procedure, in: AAAI (2000). · Zbl 0757.90059 |

[12] | M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang and S. Malik, Chaff: Engineering an efficient SAT solver, in: Proc. of 39th Design Automation Conference (June 2001). |

[13] | D. Pretolani, Efficiency and stability of hypergraph SAT algorithms, in: Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, eds. D.S. Johnson and M. Trick, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 26 (American Mathematical Society, 1995). |

[14] | Sharir, M., A strong-connectivity algorithm and its application in data flow analysis, Computers and Mathematics with Applications, 7, 67-72, (1981) · Zbl 0443.68046 |

[15] | J.P. Silva and K.A. Sakallah, GRASP — a new search algorithm for satisfiability, in: Proc. of IEEE/ACM Int’l Conf. on Computer-Aided Design (IEEE Computer Society Press, 1996) pp. 220-227. |

[16] | A. Van Gelder, Toward leaner binary-clause reasoning in a satisfiability solver (extended abstract), in: Symposium on the Theory and Applications of Satisfiability Testing, Cincinnati, OH (2002) pp. 43-53. |

[17] | A. Van Gelder, Extracting (easily) checkable proofs from a satisfiability solver that employs both preorder and postorder resolution, in: Proc. of 17th Int’l Symposium on AI and Mathematics, Ft. Lauderdale, FL (2002). Also available at ftp://ftp.cse.ucsc.edu/pub/avg/CBJ/sat-pre-post.ps.gz. |

[18] | A. Van Gelder and Y.K. Tsuji, Satisfiability testing with more reasoning and less guessing, in: Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, eds. D.S. Johnson and M. Trick, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 26 (American Mathematical Society, 1996). Also at ftp://ftp.cse.ucsc.edu/pub/avg/kclose-tr.ps.gz. · Zbl 0868.03007 |

[19] | H. Zhang, SATO: An efficient propositional prover, in: Proc. of 14th International Conference on Automated Deduction (1997) pp. 272-275. |

[20] | L. Zhang, C. Madigan, M. Moskewicz and S. Malik, Efficient conflict driven learning in a boolean satisfiability solver, in: ICCAD (November 2001). |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.