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. © 2012 Springer-Verlag.
CITATION STYLE
Han, C. S., & Jiang, J. H. R. (2012). When Boolean satisfiability meets Gaussian elimination in a simplex way. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7358 LNCS, pp. 410–426). https://doi.org/10.1007/978-3-642-31424-7_31
Mendeley helps you to discover research relevant for your work.