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 0 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 0. 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 technique adding 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.
Copyright c 2017 by the paper's authors