Theory and Applications of Satisfiability Testing
From MaRDI portal
Publication:5325885
DOI10.1007/b95238zbMath1204.68191OpenAlexW2494235144WikidataQ56039662 ScholiaQ56039662MaRDI QIDQ5325885
Publication date: 24 July 2009
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b95238
Related Items
\(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers, Fast, flexible MUS enumeration, Quantified maximum satisfiability, On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Semantically-guided goal-sensitive reasoning: model representation, Interpolation and model checking for nonlinear arithmetic, Compiling finite linear CSP into SAT, Generating SAT instances with community structure, KBO orientability, Nonrealizable minimal vertex triangulations of surfaces: showing nonrealizability using oriented matroids and satisfiability solvers, Looking-ahead in backtracking algorithms for abstract argumentation, On a class of decision diagrams, Merged processes: a new condensed representation of Petri net behaviour, SAT race 2015, Online belief tracking using regression for contingent planning, Tableau reasoning for description logics and its extension to probabilities, A competitive and cooperative approach to propositional satisfiability, Merging almost sorted sequences yields a 24-sorter, Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005), Answer set programming based on propositional satisfiability, M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures, A verified SAT solver framework with learn, forget, restart, and incrementality, Some computational aspects of DISTANCE SAT, Solving satisfiability problems with preferences, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Minimal sets on propositional formulae. Problems and reductions, The first international competition on computational models of argumentation: results and analysis, Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms, Incremental bounded model checking for embedded software, Optimization techniques for Craig interpolant compaction in unbounded model checking, Symmetry in Gardens of Eden, On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\), On the impact of configuration on abstract argumentation automated reasoning, Computer-aided proof of Erdős discrepancy properties, Efficient, verified checking of propositional proofs, raSAT: an SMT solver for polynomial constraints, Synchronous counting and computational algorithm design, Automatic construction of optimal static sequential portfolios for AI planning and beyond, Design and results of the Fifth Answer Set Programming Competition, Learning from conflicts in propositional satisfiability, A pearl on SAT and SMT solving in Prolog, Probabilistic satisfiability: algorithms with the presence and absence of a phase transition, The complexity of inverting explicit Goldreich's function by DPLL algorithms, SAT-solving in CSP trace refinement, Analytic tableaux for higher-order logic with choice, Dealing with satisfiability and \(n\)-ary CSPs in a logical framework, An explicit transition system construction approach to LTL satisfiability checking, Efficient benchmarking of algorithm configurators via model-based surrogates, Explaining the \texttt{cumulative} propagator, Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning, Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search, Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases, Algorithms for computing minimal equivalent subformulas, Verification conditions for source-level imperative programs, Curriculum-based course timetabling with SAT and MaxSAT, SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata, An overview of parallel SAT solving, Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories, Complexity-sensitive decision procedures for abstract argumentation, Algorithm runtime prediction: methods \& evaluation, Boosting haplotype inference with local search, Accelerating predicate abstraction by minimum unsatisfiable cores extraction, Loop detection in term rewriting using the eliminating unfoldings, The configurable SAT solver challenge (CSSC), The incremental satisfiability problem for a two conjunctive normal form, Automatic construction of parallel portfolios via algorithm configuration, Improving configuration checking for satisfiable random \(k\)-SAT instances, About some UP-based polynomial fragments of SAT, State space search nogood learning: online refinement of critical-path dead-end detectors in planning, Parallelizing SMT solving: lazy decomposition and conciliation, An empirical comparison of formalisms for modelling and analysis of dynamic reconfiguration of dependable systems, SAT solver management strategies in IC3: an experimental approach, Efficient branch-and-bound algorithms for weighted MAX-2-SAT, Verification and falsification of programs with loops using predicate abstraction, On the power of clause-learning SAT solvers as resolution engines, Haplotype inference with pseudo-Boolean optimization, Deciding effectively propositional logic using DPLL and substitution sets, Sharpening constraint programming approaches for bit-vector theory, Haplotyping populations by pure parsimony based on compatible genotypes and greedy heuris\-tics, Accelerating backtrack search with a best-first-search strategy, SAT and IP based algorithms for magic labeling including a complete search for total magic labelings, CompoSAT: specification-guided coverage for model finding, A satisfiability and workload-based exact method for the resource constrained project scheduling problem with generalized precedence constraints, SCIP: solving constraint integer programs, Efficiently checking propositional refutations in HOL theorem provers, Efficient bounded model checking of heap-manipulating programs using tight field bounds, SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking, A generative power-law search tree model, Variable and clause elimination for LTL satisfiability checking, New developments in the theory of Gröbner bases and applications to formal verification, Efficient SAT-based proof search in intuitionistic propositional logic, MiniSat, Polybori: A framework for Gröbner-basis computations with Boolean polynomials, Labelled splitting, A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas, Data compression for proof replay, Topological configurations \((n_4)\) exist for all \(n\geq 17\), Increasing interpretations, Set constraint model and automated encoding into SAT: application to the social golfer problem, A Study of Symmetry Breaking Predicates and Model Counting, Implementing Superposition in iProver (System Description), Diagnostic Reasoning for Robotics Using Action Languages, PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF, Speeding up MUS Extraction with Preprocessing and Chunking, Hints Revealed, Mining Backbone Literals in Incremental SAT, Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API, Using Community Structure to Detect Relevant Learnt Clauses, SAT-Based Formula Simplification, Between SAT and UNSAT: The Fundamental Difference in CDCL SAT, Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing, QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving, SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving, Search-Space Partitioning for Parallelizing SMT Solvers, A New Approach to Partial MUS Enumeration, Evaluating CDCL Variable Scoring Schemes, Propositional SAT Solving, SAT-Based Model Checking, Expressing Symmetry Breaking in DRAT Proofs, Checking Reversibility of Boolean Functions, The CADE-28 Automated Theorem Proving System Competition – CASC-28, Integrating Inductive Definitions in SAT, Modelling Max-CSP as Partial Max-SAT, A Generalized Framework for Conflict Analysis, A Decision-Making Procedure for Resolution-Based SAT-Solvers, Improvements to Hybrid Incremental SAT Algorithms, SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions, Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms, Finding Guaranteed MUSes Fast, Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems withIDP3, Combining Answer Set Programming and domain heuristics for solving hard industrial problems (Application Paper), Constraint answer set solver EZCSP and why integration schemas matter, Complete SAT-Based Model Checking for Context-Free Processes, A Note on Universal Point Sets for Planar Graphs, Arctic Termination ...Below Zero, Root-Labeling, GAC Via Unit Propagation, Limitations of Restricted Branching in Clause Learning, Exploiting Past and Future: Pruning by Inconsistent Partial State Dominance, Towards Robust CNF Encodings of Cardinality Constraints, On Universal Restart Strategies for Backtracking Search, Hierarchical Hardness Models for SAT, D2-SYNCHRONIZATION IN NONDETERMINISTIC AUTOMATA, Constraint Integer Programming: A New Approach to Integrate CP and MIP, Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting, LCF-Style Propositional Simplification with BDDs and SAT Solvers, Imperative Functional Programming with Isabelle/HOL, Qualitative Numeric Planning: Reductions and Complexity, Advancing Lazy-Grounding ASP Solving Techniques – Restarts, Phase Saving, Heuristics, and More, MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks*, Practical Implementation of a Quantum Backtracking Algorithm, Decomposing SAT Instances with Pseudo Backbones, Quantitative Logic Reasoning, Finding Effective SAT Partitionings Via Black-Box Optimization, An Algorithm for Direct Construction of Complete Merged Processes, Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models, On the Implementation of Weight Constraint Rules in Conflict-Driven ASP Solvers, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Finding Reductions Automatically, Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases, Compressing Propositional Refutations, Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis, Multi-shot ASP solving with clingo, Algebraic Cryptanalysis of the Data Encryption Standard, Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems, Sort It Out with Monotonicity, Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms, Experimental Study of the Shortest Reset Word of Random Automata, Mutation-Based Test Case Generation for Simulink Models, The External Interface for Extending WASP, Solving Advanced Argumentation Problems with Answer Set Programming, Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints, SAT-Based Model Checking without Unrolling, Temporal Logic Modeling of Biological Systems, Abductive Reasoning on Molecular Interaction Maps, Coloring the Voronoi tessellation of lattices, Validating QBF Validity in HOL4, Dependency Pairs and Polynomial Path Orders, Efficiently Calculating Evolutionary Tree Measures Using SAT, Finding Lean Induced Cycles in Binary Hypercubes, Boundary Points and Resolution, Dynamic Symmetry Breaking by Simulating Zykov Contraction, Generalizing Core-Guided Max-SAT, Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search, Unnamed Item, Putting ABox Updates into Action, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Abstract Answer Set Solvers, Present and Future of Practical SAT Solving, Increasing Interpretations, Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time, Applications of SAT Solvers in Cryptanalysis: Finding Weak Keys and Preimages, Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores, On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving, MiFuMax—a Literate MaxSAT Solver, ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver, Implementing Efficient All Solutions SAT Solvers, Experimental Evaluation of a Branch-and-Bound Algorithm for Computing Pathwidth and Directed Pathwidth, A Volunteer-Computing-Based Grid Architecture Incorporating Idle Resources of Computational Clusters, Combining SAT solvers with computer algebra systems to verify combinatorial conjectures, Lego-like spheres and tori, Analyzing program termination and complexity automatically with \textsf{AProVE}, The complete parsimony haplotype inference problem and algorithms based on integer programming, branch-and-bound and Boolean satisfiability, Applications of Action Languages in Cognitive Robotics, Algorithms for Solving Satisfiability Problems with Qualitative Preferences, What we can learn from conflicts in propositional satisfiability, Using SAT solvers for synchronization issues in non-deterministic automata, Using Satisfiability for Non-optimal Temporal Planning, Satisfiability and synthesis modulo oracles, A logical approach to efficient Max-SAT solving, Modelling and solving temporal reasoning as propositional satisfiability, Cutting plane versus compact formulations for uncertain (integer) linear programs, Linear templates of ACTL formulas with an application to SAT-based verification, Learning a propagation complete formula, Careful synchronization of partial deterministic finite automata, Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form, Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem, A SAT Approach to Clique-Width, Optimization Modulo Theories with Linear Rational Costs, Modular strategic SMT solving with \textbf{SMT-RAT}, Algebraic Attacks Using Binary Decision Diagrams, Constructing 5-chromatic unit distance graphs embedded in the Euclidean plane and two-dimensional spheres, Meet-in-the-middle attacks and structural analysis of round-reduced PRINCE, Solving Nonlinear Integer Arithmetic with MCSAT, An Expressive Model for Instance Decomposition Based Parallel SAT Solvers, A Boolean satisfiability approach to the resource-constrained project scheduling problem, Efficient theory combination via Boolean search, Deep learning for the generation of heuristics in answer set programming: a case study of graph coloring, QMaxSATpb: a certified MaxSAT solver, A note on universal point sets for planar graphs, Unified QBF certification and its applications, Processes and continuous change in a SAT-based planner, Local search with a SAT oracle for combinatorial optimization, Formal semantics and verification of network-based biocomputation circuits, Visualizing SAT instances and runs of the DPLL algorithm, DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions, On Freezing and Reactivating Learnt Clauses, Between Restarts and Backjumps, Abstraction-Based Algorithm for 2QBF, Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One, Generalized Conflict-Clause Strengthening for Satisfiability Solvers, Empirical Study of the Anatomy of Modern Sat Solvers, Popularity-similarity random SAT formulas, Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions, Propositional proof systems based on maximum satisfiability, Algorithms for computing minimal unsatisfiable subsets of constraints, On the complexity of reconstructing chemical reaction networks, Polynomial time algorithm for min-ranks of graphs with simple tree structures, On the order of test goals in specification-based testing, Limitations of restricted branching in clause learning, Design and results of the second international competition on computational models of argumentation, Clause vivification by unit propagation in CDCL SAT solvers, How we designed winning algorithms for abstract argumentation and which insight we attained, \textsc{OptiMathSAT}: a tool for optimization modulo theories, raSAT: An SMT Solver for Polynomial Constraints, Subsumption Algorithms for Three-Valued Geometric Resolution, Satisfiability via Smooth Pictures, Extreme Cases in SAT Problems, Improved Static Symmetry Breaking for SAT, Learning Rate Based Branching Heuristic for SAT Solvers, Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer, Finding Finite Models in Multi-sorted First-Order Logic, MCS Extraction with Sublinear Oracle Queries, Predicate Elimination for Preprocessing in First-Order Theorem Proving, 2QBF: Challenges and Solutions, HordeQBF: A Modular and Massively Parallel QBF Solver, LMHS: A SAT-IP Hybrid MaxSAT Solver, An automated approach to the Collatz conjecture, A tableaux calculus for default intuitionistic logic, Certifying proofs for SAT-based model checking, Anti-alignments in Conformance Checking – The Dark Side of Process Models, SAT competition 2020, Pakota: A System for Enforcement in Abstract Argumentation, DRAT Proofs for XOR Reasoning, Wombit: a portfolio bit-vector solver using word-level propagation, An iterative method for linear decomposition of index generating functions, On orthogonal symmetric chain decompositions, New records of pre-image search of reduced SHA-1 using SAT solvers, SAT-based explicit LTL reasoning and its application to satisfiability checking, On affine sub-families of the NFSR in grain, Methods for solving reasoning problems in abstract argumentation -- a survey, On the hardness of solving edge matching puzzles as SAT or CSP problems, View-based propagator derivation, meSAT: multiple encodings of CSP to SAT, Interpolant Learning and Reuse in SAT-Based Model Checking, A posthumous contribution by Larry Wos: excerpts from an unpublished column, Flexible proof production in an industrial-strength SMT solver, Iterative and core-guided maxsat solving: a survey and assessment, Supercharging plant configurations using Z3, Towards a compact SAT-based encoding of itemset mining tasks, OptiLog: a framework for SAT-based systems, Deep cooperation of CDCL and local search for SAT, Efficient all-UIP learned clause minimization, Assessing progress in SAT solvers through the Lens of incremental SAT, On dedicated CDCL strategies for PB solvers, The \textsc{MergeSat} solver, Leveraging GPUs for effective clause sharing in parallel SAT solving, Certified DQBF solving by definition extraction, Logical cryptanalysis with WDSat, Using a SAT Solver to Find Interesting Sets of Nonstandard Dice, Bit-precise verification of discontinuity errors under fixed-point arithmetic, Machine learning and logic: a new frontier in artificial intelligence, Towards better heuristics for solving bounded model checking problems, Generating random instances of weighted model counting. An empirical analysis with varying primal treewidth, The 11th IJCAR automated theorem proving system competition – CASC-J11, Functional synthesis via input-output separation, FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets, State identification and verification with satisfaction, Solving modal logic problems by translation to higher-order logic, Synthesising programs with non-trivial constants, Enumerating, cataloguing and classifying all quantales on up to nine elements, Exact Synthesis of ESOP Forms, Drawing Order Diagrams Through Two-Dimension Extension, Balanced covering arrays: A classification of covering arrays and packing arrays via exact methods, Three-dimensional stable matching with cyclic preferences, iProver-Eq: An Instantiation-Based Theorem Prover with Equality, Decreasing Diagrams and Relative Termination, Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution, Proofs and Certificates for Max-SAT
Uses Software
