Abstract
Recent research on Boolean satisfiability (SAT) reveals modern solvers’ inability to handle formulae in the abundance of parity (xor) constraints. Although xor-handling in SAT solving has attracted much attention, challenges remain to completely deduce xor-inferred implications and conflicts, to effectively reduce expensive overhead, and to directly generate compact interpolants. This paper integrates SAT solving tightly with Gaussian elimination in the style of Dantzig’s simplex method. It yields a powerful tool overcoming these challenges. Experiments show promising performance improvements and efficient derivation of compact interpolants, which are otherwise unobtainable.
Chapter PDF
Similar content being viewed by others
Keywords
- Gaussian Elimination
- Conjunctive Normal Form
- Conjunctive Normal Form Formula
- Nonbasic Variable
- Resolution Refutation
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Altera Advanced Synthesis Cookbook, http://www.altera.com/literature/manual/stx_cookbook.pdf
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press (2009)
Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification, http://www.eecs.berkeley.edu/~alanmi/abc/
Baumgartner, P., Massacci, F.: The taming of the (X)OR. In: Proc. Int’l Conf. on Computational Logic, pp. 508–522 (2000)
Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. on Computational Logic 12(1), 7 (2010)
Chen, J.-C.: XORSAT: An efficient algorithm for the DIMACS 32-bit parity problem, CoRR abs/cs/0703006 (2007)
Chen, J.-C.: Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 298–311. Springer, Heidelberg (2009)
Craig, W.: Linear reasoning: A new form of the Herbrand-Gentzen theorem. J. Symbolic Logic 22(3), 250–268 (1957)
Dantzig, G.: Maximization of linear function of variables subject to linear inequalities. Activity Analysis of Production and Allocation, 339–347 (1951)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Gomes, C., Sabharwal, A., Selman, B.: Model counting: A new strategy for obtaining good bounds. In: Proc. National Conf. on Artificial Intelligence (AAAI), pp. 54–61 (2006)
Haanpaa, H., Jarvisalo, M., Kaski, P., Niemela, I.: Hard satisfiable clause sets for benchmarking equivalence reasoning techniques. Journal on Satisfiability, Boolean Modeling and Computation 2(1-4), 27–46 (2006)
Jiang, J.-H.R., Lee, C.-C., Mishchenko, A., Huang, C.-Y.: To SAT or not to SAT: Scalable exploration of functional dependency. IEEE Trans. on Computers 59(4), 457–467 (2010)
Liu, H.-Y., Chou, Y.-C., Lin, C.-H., Jiang, J.-H.R.: Towards Completely Automatic Decoder Synthesis. In: Proc. Int’l Conf. on Computer Aided Design (ICCAD), pp. 389–395 (2011)
Li, C.M.: Integrating equivalency reasoning into Davis-Putnam procedure. In: Proc. National Conf. on Artificial Intelligence (AAAI), pp. 291–296 (2000)
Laitinen, T., Junttila, T., Niemela, I.: Extending clause learning DPLL with parity reasoning. In: Proc. European Conference on Artificial Intelligence (ECAI), pp. 21–26 (2010)
Laitinen, T., Junttila, T., Niemela, I.: Equivalence class based parity reasoning with DPLL(XOR). In: Proc. Int’l Conf. on Tools with Artificial Intelligence (ICTAI), pp. 649–658 (2011)
Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: Proc. Int’l Conf. on Computer-Aided Design (ICCAD), pp. 836–843 (2006)
McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
McMillan, K.L.: An interpolating theorem prover. Theoretical Computer Science 345(1), 101–121 (2005)
Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT-problem: Encoding and analysis. Journal of Automated Reasoning 24(1-2), 165–203 (2000)
Moskewicz, M., Madigan, C., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. Design Automation Conf. (DAC), pp. 530–535 (2001)
Marques-Silva, J., Sakallah, K.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. on Computeres 48(5), 506–521 (1999)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937–977 (2006)
Soos, M., Nohl, K., Castelluccia, C.: Extending SAT Solvers to Cryptographic Problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009)
Soos, M.: Enhanced Gaussian elimination in DPLL-based SAT solvers. In: Proc. Pragmatics of SAT (2010)
Warners, J., van Maaren, H.: A two-phase algorithm for solving a class of hard satisfiability problems. Operations Research Letters 23(3-5), 81–88 (1998)
Yorsh, G., Musuvathi, M.: A Combination Method for Generating Interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 353–368. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Han, CS., Jiang, JH.R. (2012). When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way. In: Madhusudan, P., Seshia, S.A. (eds) Computer Aided Verification. CAV 2012. Lecture Notes in Computer Science, vol 7358. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31424-7_31
Download citation
DOI: https://doi.org/10.1007/978-3-642-31424-7_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31423-0
Online ISBN: 978-3-642-31424-7
eBook Packages: Computer ScienceComputer Science (R0)