Elimination Techniques in Modern Propositional Logic Reasoning NorbertManthey nmanthey@conp-solutions.com Elimination Techniques in Modern Propositional Logic Reasoning 17E7721AFF94E7EEFB318A5E3FE3E8DC GROBID - A machine learning software for extracting information from scholarly documents

The satisfiability testing (SAT) problem is one of the most relevant problems of computer science, as SAT is the representative problem for the complexity class N P [3]. Due to the numerous improvements to SAT solvers, many industrial problems are successfully reduced to SAT [3]. The highly optimized and specialized SAT solvers make these improvements accessible, and with such systems solving problems via SAT became effective.

Many recent improvements in SAT solvers are related to data structures, search heuristics or problem simplifications. However, the major reasoning techniques in propositional logic is resolution on clauses, used in unit propagation, variable elimination as well as clause learning [6,7,13]. State-of-the-art SAT solvers primarily use this technique to guide their search [1].

Both from a reasoning strength, as well as from an empirical analysis point of view, these systems still benefit from further problem simplifications, specifically variable elimination, where elimination is not only performed on pure clauses, but also on XOR constraints as well as cardinality constraints [2,4,8,14]. For the two more expressive constraint types, constraints can even be extracted from formulas in CNF.

The relations between formulas F before and after F a simplification have been described in [11]. For applied SAT solving, not only performance matters, but also the ability of constructing models for the original formula F based on a model for F . All above mentioned elimination techniques have this property.

Further simplification techniques rely on removing clauses, e.g. blocked clause elimination [9]. From a proof complexity point of view, the counter techniqueadding blocked clauses [10] -can lead to a much more powerful reasoning than resolution, namely introducing fresh variables via extended resolution [5]. Attempts on introducing fresh variables automatically exist [12], but are currently more used during encoding a problem into CNF than as a reasoning technique during search. Again, a model for the original formula can always be constructed based on a model of the simplified formula.
Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions SAT Competition 2017: Solver and Benchmark Descriptions
Helsinki, Finland
 2017. 2017 B. University of Helsinki Publication series Boosting the performance of SLS and CDCL solvers by preprocessor tuning ABalint NManthey POS-13 of EPiC Series EasyChair 2014 29 Copyright c SOQE 2017 -Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics PKoopmann SRudolph RSchmidt CWernhard
Dresden, Germany
 2017. December 6-8, 2017 by the paper's authors Handbook of Satisfiability Frontiers in Artificial Intelligence and Applications ABiere MJ HHeule HVan Maaren TWalsh IOS Press 2009 185 Detecting cardinality constraints in CNF ABiere DLe Berre ELonca NManthey SAT 2014 2014 8561 A short proof of the pigeon hole principle using extended resolution SACook SIGACT News 8 4 Oct. 1976 A machine program for theoremproving MDavis GLogemann DLoveland Communications of the ACM 5 7 1962 A computing procedure for quantification theory MDavis HPutnam Journal of the ACM 7 3 1960 Effective preprocessing in SAT through variable and clause elimination NEén ABiere SAT 2005 2005 3569 Blocked clause elimination MJärvisalo ABiere MJHeule TACAS 2010 6015 On a generalization of extended resolution OKullmann Discrete Applied Mathematics 96 97 1999 Towards Next Generation Sequential and Parallel SAT Solvers NManthey 2014 TU Dresden PhD thesis Automated reencoding of Boolean formulas NManthey MJHeule ABiere Hardware and Software: Verification and Testing 2013 7857 GRASP -a new search algorithm for satisfiability JPMarques-Silva KASakallah ICCAD '96 IEEE Computer Society 1996 Extending SAT solvers to cryptographic problems MSoos KNohl CCastelluccia SAT 2009 2009 5584