Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications

By Lintao Zhang, Sharad Malik. 2003 Design, Automation and Test in Europe Conference and Exhibition, 2003

339 citations recorded by the source corpus.

How researchers see this paper

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

Conflict-driven answer set solving: From theory to practice (2012, methodology): “[128,115]) also apply to CDNL-ASP, given that both search procedures make use of conflict-driven assertions to exclude repetitions of assignments.”
Interpolation and SAT-Based Model Checking (2003, background): “In the unsatisfiable case, it can produce a proof of unsatisfiability [16, 25 ].”
Iterative and core-guided MaxSAT solving: A survey and assessment (2013, background): “of the information provided by unsatisf iable cores [128] to guide the search.”
On Solving the Partial MAX-SAT Problem (2006, methodology): “the UNSAT core [21], and uses relaxation variables to eliminate these UNSAT cores one by one until the instance becomes satisfiable.”
PicoSAT Essentials (2008, background): “Another important feature of modern SAT solvers is their ability to produce proof traces [40, 18, 13, 36, 22, 16].”