GRASP: a search algorithm for propositional satisfiability

DOI10.1109/12.769433zbMath1392.68388OpenAlexW2044560939WikidataQ56039660 ScholiaQ56039660MaRDI QIDQ4571400

Karem A. Sakallah, João P. 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

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

Related Items

Narrow Proofs May Be Maximally Long, On CDCL-Based Proof Systems with the Ordered Decision Strategy, ASP and subset minimality: enumeration, cautious reasoning and MUSes, Reluplex: a calculus for reasoning about deep neural networks, A novel two-echelon hierarchical location-allocation-routing optimization for green energy-efficient logistics systems, Inconsistency Proofs for ASP: The ASP - DRUPE Format, Computations about formal multiple zeta spaces defined by binary extended double shuffle relations, On vanishing sums of roots of unity in polynomial calculus and sum-of-squares, Unnamed Item, Constraint and Satisfiability Reasoning for Graph Coloring, Constraint Integer Programming: A New Approach to Integrate CP and MIP, The Mechanical Verification of a DPLL-Based Satisfiability Solver, An automated approach to the Collatz conjecture, Debugging Non-ground ASP Programs: Technique and Graphical Tools, Cutting to the Chase Solving Linear Integer Arithmetic, Unnamed Item, Supercritical Space-Width Trade-offs for Resolution, Short Proofs Are Hard to Find, Unnamed Item, Unnamed Item, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, Implementing Efficient All Solutions SAT Solvers, On preprocessing techniques and their impact on propositional model counting, On the efficient modeling and solution of the multi-mode resource-constrained project scheduling problem with generalized precedence relations, Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, Bounded model checking of infinite state systems, Advances in WASP, Clause-Learning for Modular Systems, What we can learn from conflicts in propositional satisfiability, Cumulative Space in Black-White Pebbling and Resolution, Between SAT and UNSAT: The Fundamental Difference in CDCL SAT, Propositional SAT Solving, Eliminating models during model elimination, Extracting a DPLL Algorithm, A note about \(k\)-DNF resolution, An approach using SAT solvers for the RCPSP with logical constraints, On a class of decision diagrams, SAT race 2015, BerkMin: A fast and robust SAT-solver, Random backtracking in backtrack search algorithms for satisfiability, A logic-based Benders decomposition for microscopic railway timetable planning, A competitive and cooperative approach to propositional satisfiability, Cautious reasoning in ASP via minimal models and unsatisfiable cores, Answer set programming based on propositional satisfiability, Unnamed Item, Unnamed Item, Unnamed Item, Planning as satisfiability: heuristics, Satisfiability Checking: Theory and Applications, Strong ETH and resolution via games and the multiplicity of strategies, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Space Complexity in Polynomial Calculus, Modular strategic SMT solving with \textbf{SMT-RAT}, A Decision-Making Procedure for Resolution-Based SAT-Solvers, SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions, Clingcon: The next generation, Towards NP-P via proof complexity and search, Design and results of the Fifth Answer Set Programming Competition, Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers, A View from the Engine Room: Computational Support for Symbolic Model Checking, What is answer set programming to propositional satisfiability, Domain reduction techniques for global NLP and MINLP optimization, Approximating minimal unsatisfiable subformulae by means of adaptive core search, Resolution and binary decision diagrams cannot simulate each other polynomially, Semantically-guided goal-sensitive reasoning: inference system and completeness, Limitations of Restricted Branching in Clause Learning, Cliques enumeration and tree-like resolution proofs, Formal verification based on Boolean expression diagrams, Simulating strong practical proof systems with extended resolution, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., Deciding floating-point logic with abstract conflict driven clause learning, Search techniques for SAT-based Boolean optimization, Truth Assignments as Conditional Autarkies, Complexity-sensitive decision procedures for abstract argumentation, Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions, Propositional proof systems based on maximum satisfiability, CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability, Another look at graph coloring via propositional satisfiability, Efficient SAT-based bounded model checking for software verification, Conflict analysis in mixed integer programming, Improving configuration checking for satisfiable random \(k\)-SAT instances, State space search nogood learning: online refinement of critical-path dead-end detectors in planning, Branch-and-bound algorithms: a survey of recent advances in searching, branching, and pruning, Extended resolution simulates binary decision diagrams, Resource-constrained project scheduling with activity splitting and setup times, Conflict-driven answer set solving: from theory to practice, A heuristic block coordinate descent approach for controlled tabular adjustment, Resolution cannot polynomially simulate compressed-BFS, UnitWalk: A new SAT solver that uses local search guided by unit clause elimination, GridSAT: Design and implementation of a computational grid application, A satisfiability and workload-based exact method for the resource constrained project scheduling problem with generalized precedence constraints, Selection of search strategies for solving 3-SAT problems, Clause vivification by unit propagation in CDCL SAT solvers, The External Interface for Extending WASP, Understanding the power of Max-SAT resolution through up-resilience, A generative power-law search tree model, A conflict-driven solving procedure for poly-power constraints, A complete adaptive algorithm for propositional satisfiability, Definability for model counting, Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space, Preface, Editorial: Symbolic computation and satisfiability checking, Computational aspects of infeasibility analysis in mixed integer programming, AND/OR search spaces for graphical models, Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search, Conflict Analysis for MINLP, Hyperresolution for Gödel logic with truth constants, A novel SAT solver for the van der Waerden numbers, An interpolating theorem prover, Methods for solving reasoning problems in abstract argumentation -- a survey, Bounded Model Checking with Parametric Data Structures, MiFuMax—a Literate MaxSAT Solver, ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver, On Exponential Lower Bounds for Partially Ordered Resolution, On Linear Resolution, Accelerating logic-based benders decomposition for railway rescheduling by exploiting similarities in delays, Cutting to the chase., Backjump-based backtracking for constraint satisfaction problems, Supercharging plant configurations using Z3, Proving unsatisfiability of CNFs locally, Assessing progress in SAT solvers through the Lens of incremental SAT, On dedicated CDCL strategies for PB solvers