GRASP: a search algorithm for propositional satisfiability

DOI10.1109/12.769433MaRDI QIDQ4571400zbMATH OpenOpenAlexWikidataFDO

Authors Karem A. Sakallah, Joao Marques-Silva

Publication date 9 July 2018

Published in IEEE Transactions on Computers (Search for Journal in Brave)

Full work available at URL https://eprints.soton.ac.uk/262032/1/jpms-tcomp99.pdf

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Special problems of linear programming (transportation, multi-index, data envelopment analysis, etc.) (90C08)

Cited in

(only showing first 100 items - show all)

• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability
• Selection of search strategies for solving 3-SAT problems
• A satisfiability and workload-based exact method for the resource constrained project scheduling problem with generalized precedence constraints
• Another look at graph coloring via propositional satisfiability
• Certified Core-Guided MaxSAT Solving
• The mechanical verification of a DPLL-based satisfiability solver
• Clause vivification by unit propagation in CDCL SAT solvers
• Planning as satisfiability: heuristics
• Clause-learning for modular systems
• Supercritical space-width trade-offs for resolution
• scientific article; zbMATH DE number 7199588 (Why is no real title available?)
• Resolution cannot polynomially simulate compressed-BFS
• On enumerating short projected models
• An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL
• The CDSAT method for satisfiability modulo theories and assignment: an exposition
• Algebraic cryptanalysis of 9 rounds of lightweight block cipher Simon32/64
• Inverting 29-step MD5 compression function via SAT
• Preimage attack on 44-step MD4 compression function with weakened last step
• Advanced metaheuristics for bi-criteria optimization in a distributed blocking flow shop problem with setup times
• A View from the Engine Room: Computational Support for Symbolic Model Checking
• The External Interface for Extending WASP
• Preimage attack on 5-round cryptographic hash function JH-256 via parallel SAT solver
• An interpolating theorem prover
• Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
• Lower bounds for set-blocked clauses proofs
• Search techniques for SAT-based Boolean optimization
• Narrow proofs may be maximally long
• Backjump-based backtracking for constraint satisfaction problems
• A simple supercritical tradeoff between size and height in resolution
• Cutting to the chase.
• A conflict-driven solving procedure for poly-power constraints
• Hyperresolution for Gödel logic with truth constants
• Improving configuration checking for satisfiable random \(k\)-SAT instances
• Domain reduction techniques for global NLP and MINLP optimization
• What is answer set programming to propositional satisfiability
• A \textit{DPLL} procedure with dichotomous branching for propositional product logic
• \textsc{ahmaxsat}: description and evaluation of a branch and bound Max-SAT solver
• UnitWalk: A new SAT solver that uses local search guided by unit clause elimination
• AND/OR search spaces for graphical models
• Limitations of Restricted Branching in Clause Learning
• SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions
• Bounded model checking with parametric data structures
• Between SAT and UNSAT: the fundamental difference in CDCL SAT
• MiFuMax -- a literate MaxSAT solver. System description
• State space search nogood learning: online refinement of critical-path dead-end detectors in planning
• Cliques enumeration and tree-like resolution proofs
• Modular strategic SMT solving with \textbf{SMT-RAT}
• \textit{clingcon}: the next generation
• Branch-and-bound algorithms: a survey of recent advances in searching, branching, and pruning
• Methods for solving reasoning problems in abstract argumentation -- a survey
• Bounded model checking of infinite state systems
• Constraint and satisfiability reasoning for graph coloring
• Extended resolution simulates binary decision diagrams
• Efficient SAT-based bounded model checking for software verification
• Editorial: Symbolic computation and satisfiability checking
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
• Propositional proof skeletons
• GridSAT: Design and implementation of a computational grid application
• On CDCL-Based Proof Systems with the Ordered Decision Strategy
• Computational aspects of infeasibility analysis in mixed integer programming
• Towards NP-P via proof complexity and search
• Implementing efficient All solutions SAT solvers
• Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
• BerkMin: A fast and robust SAT-solver
• Accelerating logic-based benders decomposition for railway rescheduling by exploiting similarities in delays
• Certified SAT solving with GPU accelerated inprocessing
• Computations about formal multiple zeta spaces defined by binary extended double shuffle relations
• SatEx: A web-based framework for SAT experimentation
• Towards an efficient library for SAT: A manifesto
• On preprocessing techniques and their impact on propositional model counting
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Proving unsatisfiability of CNFs locally
• Resource-constrained project scheduling with activity splitting and setup times
• Supercharging plant configurations using Z3
• On dedicated CDCL strategies for PB solvers
• A review on declarative approaches for constrained clustering
• A competitive and cooperative approach to propositional satisfiability
• An annotated bibliography of GRASP-Part II: Applications
• A novel SAT solver for the van der Waerden numbers
• On the efficient modeling and solution of the multi-mode resource-constrained project scheduling problem with generalized precedence relations
• scientific article; zbMATH DE number 7300350 (Why is no real title available?)
• A greedy randomized adaptive search procedure (GRASP) for inferring logical clauses from examples in polynomial time and some extensions
• Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Conflict Analysis for MINLP
• Reluplex: a calculus for reasoning about deep neural networks
• Strong ETH and resolution via games and the multiplicity of strategies
• Resolution and binary decision diagrams cannot simulate each other polynomially
• ASP and subset minimality: enumeration, cautious reasoning and MUSes
• Experimental and Efficient Algorithms
• Advances in WASP
• Propositional proof systems based on maximum satisfiability
• What we can learn from conflicts in propositional satisfiability
• Deciding floating-point logic with abstract conflict driven clause learning
• Propositional SAT solving
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Random backtracking in backtrack search algorithms for satisfiability
• Branch and bound for piecewise linear neural network verification
• A Decision-Making Procedure for Resolution-Based SAT-Solvers

This page was built for publication: GRASP: a search algorithm for propositional satisfiability

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