Local redundancy in SAT: generalizations of blocked clauses.

*(English)*Zbl 1403.68239Summary: Clause-elimination procedures that simplify formulas in conjunctive normal form play an important role in modern SAT solving. Before or during the actual solving process, such procedures identify and remove clauses that are irrelevant to the solving result. These simplifications usually rely on so-called redundancy properties that characterize cases in which the removal of a clause does not affect the satisfiability status of a formula. One particularly successful redundancy property is that of blocked clauses, because it generalizes several other redundancy properties. To find out whether a clause is blocked – and therefore redundant – one only needs to consider its resolution environment, i.e., the clauses with which it can be resolved. For this reason, we say that the redundancy property of blocked clauses is local. In this paper, we show that there exist local redundancy properties that are even more general than blocked clauses. We present a semantic notion of blocking and prove that it constitutes the most general local redundancy property. We furthermore introduce the syntax-based notions of set-blocking and super-blocking, and show that the latter coincides with our semantic blocking notion. In addition, we show how semantic blocking can be alternatively characterized via Davis and Putnam’s rule for eliminating atomic formulas. Finally, we perform a detailed complexity analysis and relate our novel redundancy properties to prominent redundancy properties from the literature.

##### MSC:

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

03B05 | Classical propositional logic |

##### References:

[1] | Tomas Balyo, Andreas Fr¨ohlich, Marijn Heule, and Armin Biere. Everything you always wanted to know about blocked sets (but were afraid to ask). In Carsten Sinz and Uwe Egly, editors, Proc. of the 17th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2014 ), volume 8561 of LNCS, pages 317–332, Cham, 2014. Springer. · Zbl 1423.68435 |

[2] | Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, pages 825–885. IOS Press, 2009. |

[3] | Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research, 22:319–351, 2004. · Zbl 1080.68651 |

[4] | Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability. IOS Press, 2009. · Zbl 1183.68568 |

[5] | Jingchao Chen. Fast blocked clause decomposition with high quality. CoRR, abs/1507.00459, 2015. |

[6] | Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201–215, 1960. · Zbl 0212.34203 |

[7] | Niklas E´en and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Proc. of the 8th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2005 ), volume 3569 of LNCS, pages 61–75. Springer, 2005. · Zbl 1128.68463 |

[8] | Hyojung Han and Fabio Somenzi. Alembic: An efficient algorithm for CNF preprocessing. In Proc. of the 44th Design Automation Conference (DAC 2007 ), pages 582–587. IEEE, 2007. |

[9] | Marijn Heule and Armin Biere. Blocked clause decomposition. In Ken McMillan, Aart Middeldorp, and Andrei Voronkov, editors, Proc. of the 19th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19 ), volume 8312 of LNCS, pages 423–438, Heidelberg, 2013. Springer. · Zbl 1407.68451 |

[10] | Marijn Heule, Warren A. Hunt, Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In Maria Paola Bonacina, editor, Proc. of the 24th Int. Conference on Automated Deduction (CADE 2013 ), volume 7898 of LNCS, pages 345–359, Heidelberg, 2013. Springer. · Zbl 1381.68270 |

[11] | Marijn Heule, Matti J¨arvisalo, Florian Lonsing, Martina Seidl, and Armin Biere. Clause elimination for SAT and QSAT. Journal of Artifical Intelligence Research, 53:127–168, 2015. · Zbl 1336.68231 |

[12] | Marijn J. H. Heule, Martina Seidl, and Armin Biere. A unified proof system for QBF preprocessing. In Proc. of the 7th Int. Joint Conference on Automated Reasoning (IJCAR 2014 ), volume 8562 of LNCS, pages 91–106. Springer, 2014. · Zbl 1409.68257 |

[13] | Marijn J.H. Heule, Matti J¨arvisalo, and Armin Biere. Efficient CNF simplification based on binary implication graphs. In Karem A. Sakallah and Laurent Simon, editors, Proc. of the 14th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2011 ), volume 6695 of LNCS, pages 201–215, Heidelberg, 2011. Springer. · Zbl 1330.68269 |

[14] | Markus Iser, Norbert Manthey, and Carsten Sinz. Recognition of nested gates in CNF formulas. In Marijn Heule and Sean Weaver, editors, Proc. of the 18th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2015 ), volume 9340 of LNCS, pages 255–271, Cham, 2015. Springer. · Zbl 06512578 |

[15] | Mikol´as Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. Artificial Intelligence, 234:1–25, 2016. · Zbl 1351.68254 |

[16] | Matti J¨arvisalo, Armin Biere, and Marijn Heule. Blocked clause elimination. In Javier Esparza and Rupak Majumdar, editors, Proc. of the 16th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010 ), volume 6015 of LNCS, pages 129–144, Heidelberg, 2010. Springer. · Zbl 1284.03208 |

[17] | Matti J¨arvisalo, Armin Biere, and Marijn Heule. Simulating circuit-level simplifications on CNF. Journal on Automated Reasoning, 49(4):583–619, 2012. · Zbl 1267.94144 |

[18] | Matti J¨arvisalo, Marijn Heule, and Armin Biere. Inprocessing rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Proc. of the 6th Int. Joint Conference on Automated Reasoning (IJCAR 2012 ), volume 7364 of LNCS, pages 355–370, Heidelberg, 2012. Springer. · Zbl 1358.68256 |

[19] | Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere. Super-blocked clauses. In Nicola Olivetti and Ashish Tiwari, editors, Proc. of the 8th Int. Joint Conference on Automated Reasoning (IJCAR 2016), volume 9706 of LNCS, pages 45–61, Cham, 2016. Springer. · Zbl 06623253 |

[20] | Hans Kleine B¨uning and Uwe Bubeck. Theory of quantified boolean formulas. In Handbook of Satisfiability, pages 735–760. IOS Press, 2009. · Zbl 1247.68237 |

[21] | Florian Lonsing, Fahiem Bacchus, Armin Biere, Uwe Egly, and Martina Seidl. Enhancing search-based QBF solving by dynamic blocked clause elimination. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Proc. of the 20th Int. Conference on Logic for Programming, Artificial Intelligence (LPAR-20 ), volume 9450 of LNCS, pages 418–433, Heidelberg, 2015. Springer. · Zbl 06528797 |

[22] | Mao Luo, Chu-Min Li, Fan Xiao, Felip Many‘a, and Zhipeng L¨u. An effective learnt clause minimization approach for CDCL SAT solvers. In Carles Sierra, editor, Proc. of the 26th Int. Joint Conference on Artificial Intelligence (IJCAI 2017 ), pages 703–711. ijcai.org, 2017. |

[23] | Norbert Manthey, Tobias Philipp, and Christoph Wernhard. Soundness of inprocessing in clause sharing SAT solvers. In Matti J¨arvisalo and Allen Van Gelder, editors, Proc. of the 16th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2013 ), volume 7962 of LNCS, pages 22–39, Heidelberg, 2013. Springer. · Zbl 1390.68582 |

[24] | C´edric Piette, Youssef Hamadi, and Lakhdar Sais. Vivifying propositional clausal formulae. In Malik Ghallab, Constantine D. Spyropoulos, Nikos Fakotakis, and Nikolaos M. Avouris, editors, Proc. of the 18th European Conference on Artificial Intelligence (ECAI 2008 ), volume 178 of Frontiers in Artificial Intelligence and Applications, pages 525–529. IOS Press, 2008. |

[25] | Giles Reger, Martin Suda, and Andrei Voronkov. Playing with AVATAR. In P. Amy Felty and Aart Middeldorp, editors, Proc. of the 25th Int. Conference on Automated Deduction (CADE 2015 ), volume 9195 of LNCS, pages 399–415, Cham, 2015. Springer. · Zbl 06515522 |

[26] | Horst Samulowitz and Fahiem Bacchus. Using SAT in QBF. In Peter van Beek, editor, Proc. of the 11th Int. Conference on Principles and Practice of Constraint Programming (CP 2005 ), volume 3709 of LNCS, pages 578–592, Heidelberg, 2005. Springer. · Zbl 1153.68485 |

[27] | Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In Proc. of the 10th Int. Symposium on Artificial Intelligence and Mathematics (ISAIM 2008 ), 2008. |

[28] | Y. Vizel, G. Weissenbacher, and S. Malik. Boolean satisfiability solvers and their applications in model checking. Proc. of the IEEE, 103(11):2021–2035, 2015. |

[29] | Nathan D. Wetzler, Marijn J. H. Heule, and Warren A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, Proc. of the 17th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2014 ), volume 8561 of LNCS, pages 422–429, Cham, 2014. Springer. · Zbl 1423.68475 |

[30] | Siert Wieringa and Keijo Heljanko. Concurrent clause strengthening. In Matti J¨arvisalo and Allen Van Gelder, editors, Proc. of the 16th Int. Conference on Theory and Applications of Satisfiability Testing (SAT 2013 ), volume 7962 of LNCS, pages 116–132, Heidelberg, 2013. Springer. · Zbl 1390.68586 |

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.