Efficient SAT solving under assumptions

DOI10.1007/978-3-642-31612-8_19MaRDI QIDQ2843331zbMATH OpenOpenAlexFDO

Authors Alexander Nadel, Vadim Ryvchin

Publication date 12 August 2013

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

Full work available at URL https://doi.org/10.1007/978-3-642-31612-8_19

Mathematics Subject Classification ID

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

Recommendations

• Ultimately incremental SAT
• Speeding up assumption-based SAT
• Factoring Out Assumptions to Speed Up MUS Extraction
• Improvements to Hybrid Incremental SAT Algorithms
• Incremental inprocessing in SAT solving

Cited in

(24)

• Incremental inprocessing in SAT solving
• Speeding up assumption-based SAT
• Guiding high-performance SAT solvers with unsat-core predictions
• Local search with a SAT oracle for combinatorial optimization
• MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
• Solving Difficult SAT Problems by Using OBDDs and Greedy Clique Decomposition
• Ultimately incremental SAT
• SAT-Based Formula Simplification
• scientific article; zbMATH DE number 5542984 (Why is no real title available?)
• Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences
• SAT-Problems and Reductions with Respect to the Number of Variables
• Optimizing S-Box Implementations for Several Criteria Using SAT Solvers
• scientific article; zbMATH DE number 1903342 (Why is no real title available?)
• scientific article; zbMATH DE number 2090309 (Why is no real title available?)
• On using incremental encodings in unsatisfiability-based MaxSAT solving
• Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
• Managing caching strategies for stream reasoning with reinforcement learning
• Formal Methods in Computer-Aided Design
• Theory and Applications of Satisfiability Testing
• Combining incomplete search and clause generation: an application to the orienteering problems with time windows
• Unsatisfiability-based algorithms for multi-objective combinatorial optimization
• Entailing generalization boosts enumeration
• Satisfiability modulo user propagators
• A nonexistence certificate for projective planes of order ten with weight 15 codewords

This page was built for publication: Efficient SAT solving under assumptions

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