Automated testing and debugging of SAT and QBF solvers

DOI10.1007/978-3-642-14186-7_6MaRDI QIDQ4930578zbMATH OpenOpenAlexWikidataFDO

Authors Robert Brummayer, Florian Lonsing, Armin Biere

Publication date 29 September 2010

Published in Theory and Applications of Satisfiability Testing – SAT 2010 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14186-7_6

Mathematics Subject Classification ID

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

Recommendations

• Testing and debugging techniques for answer set solver development
• Automated benchmarking of incremental SAT and QBF solvers
• SpyBug: automated bug detection in the configuration space of SAT solvers
• Fault Localization and Correction with QBF
• Theory and Applications of Satisfiability Testing

Cited in

(25)

• Efficient benchmarking of algorithm configurators via model-based surrogates
• QBFFam: a tool for generating QBF families from proof complexity
• New models for generating hard random Boolean formulas and disjunctive logic programs
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• QMaxSATpb: a certified MaxSAT solver
• SpyBug: automated bug detection in the configuration space of SAT solvers
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• versat: A Verified Modern SAT Solver
• SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
• Expressing symmetry breaking in DRAT proofs
• Testing and debugging techniques for answer set solver development
• Fault Localization and Correction with QBF
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• scientific article; zbMATH DE number 7029312 (Why is no real title available?)
• Size, cost and capacity: a semantic technique for hard random QBFs
• The configurable SAT solver challenge (CSSC)
• Mining definitions in Kissat with Kittens
• Never trust your solver: certification for SAT and QBF
• Towards Uniform Certification in QBF
• Certified dominance and symmetry breaking for combinatorial optimisation
• Trusted scalable SAT solving with on-the-fly LRAT checking
• Clausal congruence closure
• Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers
• Certifying incremental SAT solving
• Certified MaxSAT preprocessing

Describes a project that uses

Uses Software

• ManySAT
• MiniSat
• QuBE++
• SMT-LIB
• PicoSAT
• QuickCheck
• Quaffle
• RSat

This page was built for publication: Automated testing and debugging of SAT and QBF solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4930578)