Theory and Applications of Satisfiability Testing
From MaRDI portal
Publication:5713748
DOI10.1007/b137280zbMath1128.68463OpenAlexW2497844642MaRDI QIDQ5713748
Publication date: 15 December 2005
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b137280
Related Items
On preprocessing techniques and their impact on propositional model counting, Progress in certifying hardware model checking results, Advances in WASP, Algorithms for Solving Satisfiability Problems with Qualitative Preferences, What we can learn from conflicts in propositional satisfiability, PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF, Preprocessing for DQBF, Recognition of Nested Gates in CNF Formulas, Evaluating CDCL Variable Scoring Schemes, Propositional SAT Solving, Termination of \(\{aa\rightarrow bc,bb\rightarrow ac,cc\rightarrow ab\}\), SATenstein: automatically building local search SAT solvers from components, Simulating circuit-level simplifications on CNF, Solving satisfiability problems with preferences, Craig interpolation with clausal first-order tableaux, Extended formulation and valid inequalities for the multi-item inventory lot-sizing problem with supplier selection, Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms, Automatically improving constraint models in Savile Row, On Davis-Putnam reductions for minimally unsatisfiable clause-sets, Symmetry in Gardens of Eden, Tighter bounds on directed Ramsey number \(R(7)\), Mining definitions in Kissat with Kittens, A Generalized Framework for Conflict Analysis, Adaptive Restart Strategies for Conflict Driven SAT Solvers, Finding Guaranteed MUSes Fast, Constraint answer set solver EZCSP and why integration schemas matter, Extended clause learning, Inconsistency Proofs for ASP: The ASP - DRUPE Format, SAT-Inspired Higher-Order Eliminations, What is answer set programming to propositional satisfiability, An Expressive Model for Instance Decomposition Based Parallel SAT Solvers, Learning from conflicts in propositional satisfiability, Auto-tabling for subproblem presolving in MiniZinc, A pearl on SAT and SMT solving in Prolog, The complexity of inverting explicit Goldreich's function by DPLL algorithms, SAT-solving in CSP trace refinement, Symbolic algorithmic verification of intransitive generalized noninterference, Hierarchical Hardness Models for SAT, Constraint CNF: SAT and CSP Language Under One Roof., Incremental preprocessing methods for use in BMC, Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases, Guarantees and limits of preprocessing in constraint satisfaction and reasoning, Matrix interpretations for proving termination of term rewriting, On the completeness of pruning techniques for planning with conditional effects, LCF-Style Propositional Simplification with BDDs and SAT Solvers, Incremental column-wise verification of arithmetic circuits using computer algebra, Truth Assignments as Conditional Autarkies, Resizing cardinality constraints for MaxSAT, An overview of parallel SAT solving, Local search for Boolean satisfiability with configuration checking and subscore, Algorithm runtime prediction: methods \& evaluation, Decomposing SAT Instances with Pseudo Backbones, Visualizing SAT instances and runs of the DPLL algorithm, On Freezing and Reactivating Learnt Clauses, Efficient CNF Simplification Based on Binary Implication Graphs, Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability, Automatic construction of parallel portfolios via algorithm configuration, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Conflict-driven answer set solving: from theory to practice, Cardinality networks: a theoretical and empirical study, Exploiting partial variable assignment in interpolation-based model checking, Preprocessing of propagation redundant clauses, Unnamed Item, Blocked Clause Elimination for QBF, Experimental Study of the Shortest Reset Word of Random Automata, Clause vivification by unit propagation in CDCL SAT solvers, How we designed winning algorithms for abstract argumentation and which insight we attained, Efficiently checking propositional refutations in HOL theorem provers, SAT-Based Model Checking without Unrolling, Efficient generation of small interpolants in CNF, Variable and clause elimination for LTL satisfiability checking, Definability for model counting, On the Hardness of SAT with Community Structure, Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer, Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers, Finding Finite Models in Multi-sorted First-Order Logic, Predicate Elimination for Preprocessing in First-Order Theorem Proving, LMHS: A SAT-IP Hybrid MaxSAT Solver, Automatic Termination, Finding Lean Induced Cycles in Binary Hypercubes, On the One-Way Function Candidate Proposed by Goldreich, Computing properties of stable configurations of thermodynamic binding networks, DRAT Proofs for XOR Reasoning, Compiling CP subproblems to MDDs and d-DNNFs, On the hardness of solving edge matching puzzles as SAT or CSP problems, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, Flexible proof production in an industrial-strength SMT solver, Preprocessing of propagation redundant clauses, Practical Algorithms for Finding Extremal Sets, On Quantifying Literals in Boolean Logic and its Applications to Explainable AI, Broken triangles: from value merging to a tractable class of general-arity constraint satisfaction problems, SAT-Inspired Eliminations for Superposition, Set constraint model and automated encoding into SAT: application to the social golfer problem, Hash-based preprocessing and inprocessing techniques in SAT solvers, On the hierarchical community structure of practical Boolean formulas, XOR local search for Boolean Brent equations, Leveraging GPUs for effective clause sharing in parallel SAT solving
Uses Software
