Abstract
A potential advantage of using a Boolean-ring formalism for propositional formulæ is the large measure of simplification it facilitates. We propose a combined linear and binomial representation for Boolean-ring polynomials with which one can easily apply Gaussian elimination and Horn-clause methods to advantage. We demonstrate that this framework, with its enhanced simplification, is especially amenable to intersection-based learning, as in recursive learning and the method of Stålmarck. Experiments support the idea that problem variables can be eliminated and search trees can be shrunk by incorporating learning in the form of Boolean-ring saturation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Ben-Sasson, E., Wigderson, A.: Short proofs are narrow — resolution made simple. Journal of the ACM 48, 149–169 (2001)
Björk, M.: A First Order Extension of Stålmarck’s Method, Ph.D. thesis, Department of Computer Science and Engineering, Göteborg University, Sweden (2006)
Bloniarz, P.A., Hunt III, H.B., Rosenkrantz, D.J.: Algebraic structures with hard equivalence and minimization problems. Journal of the ACM 31, 879–904 (1984)
Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Transactions on Computational Logic (to appear)
Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24, 293–318 (1992)
Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proc. 28th ACM Symposium on Theory of Computing, pp. 174–183 (1996)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)
Dershowitz, N., Hanna, Z., Nadel, A.: A clause-based heuristic for SAT solvers d heuristic for SAT solvers. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 46–60. Springer, Heidelberg (2005)
Dershowitz, N., Kirchner, C.: Abstract canonical presentations. Theoretical Computer Science 357, 53–69 (2006)
Dershowitz, N., Plaisted, D.A.: Rewriting. Handbook of Automated Reasoning. In: Robinson, A., Voronkov, A. (eds.) ch. 9, vol. 1, pp. 535–610. Elsevier, Amsterdam (2001)
Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming 3, 267–284 (1984)
Hsiang, J., Dershowitz, N.: Rewrite methods for clausal and non-clausal theorem proving. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 331–346. Springer, Heidelberg (1983)
Hsiang, J., Huang, G.S.: Some fundamental properties of Boolean ring normal forms. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 35, 587–602 (1997)
Hsiang, J., Huang, G.S.: Compact representation of Boolean formulas. Chinese Journal of Advanced Software Research 6(2), 178–187 (1999)
Jan, R.L.: Experimental results on propositional theorem proving with Boolean ring. Master’s thesis, Department of Computer Science and Information Engineering, National Taiwan University (1997)
Kunz, W., Pradhan, D.K.: Recursive learning: A new implication technique for efficient solutions to CAD problems — test, verification, and optimization. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 13, 1143–1158 (1994)
McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning 19, 263–276 (1997)
Marques-Silva, J.P.: Algebraic simplification techniques for propositional satisfiability. Technical Report RT/01/2000, INESC (2000)
Sasao, T.: And-exor expressions and their optimization. In: Sasao, T. (ed.) Logic Synthesis and Optimization, pp. 287–312. Kluwer, Dordrecht (1993)
Sasao, T., Besslich, P.: On the complexity of mod-2 sum PLA’s. IEEE Transactions on Computers C-39(2), 263–265 (1990)
Sheeran, M., Stålmarck, G.: A tutorial on stålmarck’s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 82–99. Springer, Heidelberg (1998)
Urquhart, A.: Hard examples for resolution. Journal of the ACM 34, 209–219 (1987)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dershowitz, N., Hsiang, J., Huang, GS., Kaiss, D. (2006). Boolean Rings for Intersection-Based Satisfiability. In: Hermann, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2006. Lecture Notes in Computer Science(), vol 4246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916277_33
Download citation
DOI: https://doi.org/10.1007/11916277_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48281-9
Online ISBN: 978-3-540-48282-6
eBook Packages: Computer ScienceComputer Science (R0)