Effective Preprocessing in SAT Through Variable and Clause Elimination

By Niklas Eén, Armin Biere. International Conference on Theory and Applications of Satisfiability Testing, 2005

746 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications

View Paper: https://www.semanticscholar.org/paper/6825642b6377689796c4d2d896f726f6152d285f

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Computer Networks and Communications

Citations in the corpus

Handbook of Satisfiability (2021, background): “, the two-watched literal scheme [52]), and advanced preprocessing techniques [10, 8, 21].”
PicoSAT Essentials (2008, background): “As it has been shown in [10], most state-of-the-art solvers can beneﬁt from such preprocessing and therefore we focus in this paper on low-level optimizations of the back end.”
Computing (2021, neutral): “Some have argued that these techniques can be used to make cities emotion-aware by developing tech niques to sense emotion in real time through the mining of social media data and spatially explicit experiences [Guthier et al. 2014, de Oliveira and Painho 2015].”
Efficient implementation of property directed reachability (2011, methodology): “The netlist is transformed to CNF using the standard Tseitin transformation [9] plus variable elimination [6].”
Conflict-driven answer set solving: From theory to practice (2012, methodology): “The latter, denoted by clasp+ , invokes clasp with options -sat-prepro and -transext=dynamic, using SatELite-like preprocessing [33] on nogoods as well as a context-dependent handling of extended”
SAT-Based Model Checking without Unrolling (2011, background): “(1) pre (2) ∀ ( i, q ) ∈ states prev , ∃ j ≥ i, ( j, q ) ∈ states } ( n, s ) := choose from states , minimizing n p := the predecessor extracted from the witness { @assert ( E ): [12, 13].”
Predicting Learnt Clauses Quality in Modern SAT Solvers (2009, methodology): “For instance, since the introduction of ZCHAFF [Moskewicz et al. , 2001] and M INISAT [E´en and Biere, 2005], the global architecture of solvers is stalling, despite important efforts of the whole community [Le Berre et al. , 2007].”
Automated configuration of algorithms for solving hard computational problems (2009, background): “More specifically, over 50% of the instances in set SWV could be solved by applying the polynomial-time preprocessor SATelite (Eén and Biere, 2005) (note that we already pointed out this large fraction of trivial SWV instances in our empirical analysis in Section 4.”
Potassco: The Potsdam Answer Set Solving Collection (2011, neutral): “Once a program has been transformed into Boolean constraints, they can be subject to further preprocessing, primarily based on resolution [25].”
Handbook of satisfiability (2009, background): “, the two-watched literal scheme [52]), and advanced preprocessing techniques [10, 8, 21].”
Algorithm runtime prediction: Methods & evaluation (2012, methodology): “Since various preprocessing techniques are routinely used before applying a general-purpose SAT solver and typically lead to substantial reductions in instance size and difficulty (especially for industrial-like instances), we apply the preprocessing procedure SATElite [23] on all instances first, a”
Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT (2015, methodology): “Bounded variable elimination (VE) [Eén and Biere, 2005], currently the most important SAT preprocessing technique, follows the Davis-Putnam procedure (DP).”