scientific article; zbMATH DE number 5493266
From MaRDI portal
Publication:5503674
zbMath1183.68568MaRDI QIDQ5503674
No author found.
Publication date: 16 January 2009
Full work available at URL: http://www.booksonline.iospress.nl/Content/View.aspx?piid=11704
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science (68-00)
Related Items
Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Quantified maximum satisfiability ⋮ On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ Portfolio approaches for constraint optimization problems ⋮ Restart strategies in a continuous setting ⋮ An improved generator for 3-CNF formulas ⋮ ASlib: a benchmark library for algorithm selection ⋮ The QBF Gallery: behind the scenes ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Adding decision procedures to SMT solvers using axioms with triggers ⋮ Optimization modulo non-linear arithmetic via incremental linearization ⋮ Enforcing almost-sure reachability in POMDPs ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Learning general constraints in CSP ⋮ Constraint satisfaction with bounded treewidth revisited ⋮ P\(_-\)UNSAT approach of attractor calculation for Boolean gene regulatory networks ⋮ Augmenting measure sensitivity to detect essential, dispensable and highly incompatible features in mass customization ⋮ On a class of decision diagrams ⋮ SAT race 2015 ⋮ Model counting for CNF formulas of bounded modular treewidth ⋮ maxSAT-based large neighborhood search for high school timetabling ⋮ A branch-and-price algorithm for the minimum latency problem ⋮ Simulating circuit-level simplifications on CNF ⋮ A satisfiability algorithm and average-case hardness for formulas over the full binary basis ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Planning as satisfiability: heuristics ⋮ Autonomous operator management for evolutionary algorithms ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ Causal effect identification in acyclic directed mixed graphs and gated models ⋮ A constraint optimization approach to causal discovery from subsampled time series data ⋮ Fuzzy relational equations with min-biimplication composition ⋮ Automatically improving constraint models in Savile Row ⋮ On Davis-Putnam reductions for minimally unsatisfiable clause-sets ⋮ On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\) ⋮ Computer-aided proof of Erdős discrepancy properties ⋮ Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems ⋮ Synchronous counting and computational algorithm design ⋮ Polynomial graph transformability ⋮ Modular instantiation schemes ⋮ Learning from conflicts in propositional satisfiability ⋮ Gate elimination: circuit size lower bounds and \#SAT upper bounds ⋮ A finite state intersection approach to propositional satisfiability ⋮ Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases ⋮ Algorithms for computing minimal equivalent subformulas ⋮ The air traffic controller work-shift scheduling problem in Spain from a multiobjective perspective: a metaheuristic and regular expression-based approach ⋮ Regular inference as vertex coloring ⋮ Program verification using symbolic game semantics ⋮ \textit{teaspoon}: solving the curriculum-based course timetabling problems with answer set programming ⋮ Modeling and solving staff scheduling with partial weighted maxSAT ⋮ Formal reliability analysis of redundancy architectures ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ Counterexample-guided inductive synthesis for probabilistic systems ⋮ Autark assignments of Horn CNFs ⋮ Generalized probabilistic satisfiability ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Two approximate algorithms for model counting ⋮ Lower bound techniques for QBF expansion ⋮ Introduction to the special issue on combining constraint solving with mining and learning ⋮ Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability ⋮ Structured learning modulo theories ⋮ Intra- and interdiagram consistency checking of behavioral multiview models ⋮ Dealing with 4-variables by resolution: an improved MaxSAT algorithm ⋮ On semidefinite least squares and minimal unsatisfiability ⋮ Computation of the transient in max-plus linear systems via SMT-solving ⋮ Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings ⋮ Exploiting subproblem optimization in SAT-based maxsat algorithms ⋮ Conflict-driven answer set solving: from theory to practice ⋮ \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT ⋮ Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems ⋮ Engineering constraint solvers for automatic analysis of probabilistic hybrid automata ⋮ A formal methods approach to predicting new features of the eukaryotic vesicle traffic system ⋮ \textit{Branch} \& \textit{Memorize} exact algorithms for sequencing problems: efficient embedding of memorization into search trees ⋮ Understanding cutting planes for QBFs ⋮ Building strategies into QBF proofs ⋮ Probabilistic characterization of random Max \(r\)-Sat ⋮ Selecting and covering colored points ⋮ Pruning external minimality checking for answer set programs using semantic dependencies ⋮ The opacity of backbones ⋮ Generalized completeness for SOS resolution and its application to a new notion of relevance ⋮ SAT encodings for pseudo-Boolean constraints together with at-most-one constraints ⋮ Propagation complete encodings of smooth DNNF theories ⋮ SAT-based models for overlapping community detection in networks ⋮ On quasi-inconsistency and its complexity ⋮ Using the method of conditional expectations to supply an improved starting point for CCLS ⋮ Solving bitvectors with MCSAT: explanations from bits and pieces ⋮ Scalable algorithms for abduction via enumerative syntax-guided synthesis ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Theorem proving as constraint solving with coherent logic ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ Semantic relevance ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Ranking with multiple reference points: efficient SAT-based learning procedures ⋮ Solving QBF with counterexample guided refinement ⋮ On the query complexity of selecting minimal sets for monotone predicates ⋮ Domain expansion for ASP-programs with external sources ⋮ On some variants of the merging variables based \((1+1)\)-evolutionary algorithm with application to MaxSAT problem ⋮ Backdoors to q-Horn ⋮ Efficient all-UIP learned clause minimization ⋮ Investigating the existence of Costas Latin squares via satisfiability testing ⋮ Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ On preprocessing techniques and their impact on propositional model counting ⋮ Automated generation of exam sheets for automated deduction ⋮ Towards an answer set programming methodology for constructing programs following a semi-automatic approach -- extended and revised version ⋮ Gearing Up for Effective ASP Planning ⋮ What we can learn from conflicts in propositional satisfiability ⋮ Propositional SAT Solving ⋮ SAT-Based Model Checking ⋮ CEGAR-tableaux: improved modal satisfiability via modal clause-learning and SAT ⋮ Eliminating models during model elimination ⋮ Reducing Boolean networks with backward Boolean equivalence ⋮ SATenstein: automatically building local search SAT solvers from components ⋮ The sample analysis machine scheduling problem: definition and comparison of exact solving approaches ⋮ A novel algorithm for Max Sat calling MOCE to order ⋮ A parameterized view on the complexity of dependence logic ⋮ Related-tweakey impossible differential attack on reduced-round \texttt{SKINNY-AEAD} M1/M3 ⋮ Parameterized complexity classes beyond para-NP ⋮ Generalising and Unifying SLUR and Unit-Refutation Completeness ⋮ Careful synchronization of partial deterministic finite automata ⋮ Improved exact algorithms for mildly sparse instances of MAX SAT ⋮ Improving the Normalization of Weight Rules in Answer Set Programs ⋮ System aspmt2smt: Computing ASPMT Theories by SMT Solvers ⋮ Exact stochastic constraint optimisation with applications in network analysis ⋮ Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all? ⋮ Space Complexity in Polynomial Calculus ⋮ Two Decades of Maude ⋮ A SAT Approach to Clique-Width ⋮ Optimization Modulo Theories with Linear Rational Costs ⋮ Constructing 5-chromatic unit distance graphs embedded in the Euclidean plane and two-dimensional spheres ⋮ Constraint-based electoral districting using a new compactness measure: an application to Portugal ⋮ Formal verification of synchronous data-flow program transformations toward certified compilers ⋮ Solving projected model counting by utilizing treewidth and its limits ⋮ Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models ⋮ Generalized probabilistic satisfiability and applications to modelling attackers with side-channel capabilities ⋮ CHAMP: a multipass algorithm for Max Sat based on saver variables ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ Go-MOCE: greedy order method of conditional expectations for Max Sat ⋮ Minimizing binary decision diagrams for systems of incompletely defined Boolean functions using algebraic cofactor expansions ⋮ A taxonomy of exact methods for partial Max-SAT ⋮ Henkin quantifiers and Boolean formulae: a certification perspective of DQBF ⋮ The joy of probabilistic answer set programming: semantics, complexity, expressivity, inference ⋮ General lower bounds and improved algorithms for infinite-domain CSPs ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Efficient strategies for CEGAR-based model checking ⋮ XSAT and NAE-SAT of linear CNF classes ⋮ Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results ⋮ Semidefinite resolution and exactness of semidefinite relaxations for satisfiability ⋮ Capturing equilibrium models in modal logic ⋮ The complexity of computing the behaviour of lattice automata on infinite trees ⋮ Precise quantitative information flow analysis -- a symbolic approach ⋮ New ways to multiply \(3 \times 3\)-matrices ⋮ Faradžev Read-type enumeration of non-isomorphic CC systems ⋮ Local search with a SAT oracle for combinatorial optimization ⋮ Abstraction-Based Algorithm for 2QBF ⋮ Failed Literal Detection for QBF ⋮ Generating Diverse Solutions in SAT ⋮ New width parameters for SAT and \#SAT ⋮ Acceptance in incomplete argumentation frameworks ⋮ Propositional proof systems based on maximum satisfiability ⋮ Minimal self-similar Peano curve of genus \(5 \times 5\) ⋮ I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra ⋮ On the complexity of reconstructing chemical reaction networks ⋮ Zeon and idem-Clifford formulations of Boolean satisfiability ⋮ Synthesis of a DNF formula from a sample of strings using Ehrenfeucht-Fraïssé games ⋮ Delegatable Functional Signatures ⋮ New models for generating hard random Boolean formulas and disjunctive logic programs ⋮ How we designed winning algorithms for abstract argumentation and which insight we attained ⋮ The SAT+CAS method for combinatorial search with applications to best matrices ⋮ Continuous relaxations for the traveling salesman problem ⋮ Discovering causal graphs with cycles and latent confounders: an exact branch-and-bound approach ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ Conflict-driven satisfiability for theory combination: transition system and completeness ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ Definability for model counting ⋮ Reactive synthesis with maximum realizability of linear temporal logic specifications ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ The Normalized Autocorrelation Length of Random Max $$r$$ -Sat Converges in Probability to $$(1-1/2^r)/r$$ ⋮ Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer ⋮ On Q-Resolution and CDCL QBF Solving ⋮ BEACON: An Efficient SAT-Based Tool for Debugging $${\mathcal {EL}}{^+}$$ Ontologies ⋮ Using decomposition-parameters for QBF: mind the prefix! ⋮ Editorial: Symbolic computation and satisfiability checking ⋮ Cylindrical algebraic decomposition with equational constraints ⋮ A complete and terminating approach to linear integer solving ⋮ Applying computer algebra systems with SAT solvers to the Williamson conjecture ⋮ MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ Efficient Reasoning for Inconsistent Horn Formulae ⋮ On the complexity of inconsistency measurement ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ Hyperresolution for Gödel logic with truth constants ⋮ Improved WPM encoding for coalition structure generation under MC-nets ⋮ Expansion-based QBF solving versus Q-resolution ⋮ Methods for solving reasoning problems in abstract argumentation -- a survey ⋮ meSAT: multiple encodings of CSP to SAT ⋮ Generalising unit-refutation completeness and SLUR via nested input resolution ⋮ Projection heuristics for binary branchings between sum and product ⋮ On dedicated CDCL strategies for PB solvers ⋮ A fast algorithm for SAT in terms of formula length ⋮ A refined branching algorithm for the maximum satisfiability problem ⋮ OMTPlan: A Tool for Optimal Planning Modulo Theories ⋮ Reducing the number of disjuncts in DTPs ⋮ Mixed Iterated Revisions: Rationale, Algorithms, and Complexity ⋮ On computing probabilistic abductive explanations ⋮ Equational Theorem Proving for Clauses over Strings ⋮ CoProver: a recommender system for proof construction ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Computations about formal multiple zeta spaces defined by binary extended double shuffle relations ⋮ Search of fractal space-filling curves with minimal dilation ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ The Discrepancy of Unsatisfiable Matrices and a Lower Bound for the Komlós Conjecture Constant ⋮ Automated key recovery attacks on round-reduced Orthros ⋮ Repairing real-time requirements ⋮ A comparison of ASP-based and SAT-based algorithms for the contension inconsistency measure ⋮ Exact and approximate determination of the Pareto front using minimal correction subsets ⋮ A logical encoding for \(k\)-\(m\)-realization of extensions in abstract argumentation ⋮ Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications ⋮ Backdoors to Normality for Disjunctive Logic Programs ⋮ On the maximal minimal cube lengths in distinct DNF tautologies ⋮ Efficient Lifting of Symmetry Breaking Constraints for Complex Combinatorial Problems ⋮ A SAT-Based Approach for Index Calculus on Binary Elliptic Curves ⋮ aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming ⋮ Progress in clasp Series 3 ⋮ Automated Reasoning Building Blocks ⋮ Approximate Model Counting via Extension Rule ⋮ Hints Revealed ⋮ Computing Maximal Autarkies with Few and Simple Oracle Queries ⋮ Preprocessing for DQBF ⋮ SAT-Based Formula Simplification ⋮ Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing ⋮ Evaluating CDCL Variable Scoring Schemes ⋮ SAT-Based Horn Least Upper Bounds ⋮ Satisfiability Modulo Theories ⋮ Interpolation and Model Checking ⋮ MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers ⋮ Extracting a DPLL Algorithm ⋮ Gradient descent dynamics and the jamming transition in infinite dimensions ⋮ A Fast Symbolic Transformation Based Algorithm for Reversible Logic Synthesis ⋮ Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable ⋮ Satisfiability Checking: Theory and Applications ⋮ On black-box optimization in divide-and-conquer SAT solving ⋮ Small Resolution Proofs for QBF using Dependency Treewidth ⋮ Generating Difficult CNF Instances in Unexplored Constrainedness Regions ⋮ Accelerating a continuous-time analog SAT solver using GPUs ⋮ SAT-based optimal classification trees for non-binary data ⋮ A resolution proof system for dependency stochastic Boolean satisfiability ⋮ Machine learning and logic: a new frontier in artificial intelligence ⋮ Verification Modulo theories ⋮ Unnamed Item ⋮ Solution Enumeration by Optimality in Answer Set Programming ⋮ Clingo goes linear constraints over reals and integers ⋮ aspeed: Solver scheduling via answer set programming ⋮ Fuzzy answer set computation via satisfiability modulo theories ⋮ On local domain symmetry for model expansion ⋮ Combining Answer Set Programming and domain heuristics for solving hard industrial problems (Application Paper) ⋮ Further improvements for SAT in terms of formula length ⋮ Clingcon: The next generation ⋮ An interdisciplinary experimental evaluation on the disjunctive temporal problem ⋮ On counting propositional logic and Wagner's hierarchy ⋮ Privacy-preserving co-synthesis against sensor-actuator eavesdropping intruder ⋮ Experiments with automated reasoning in the class ⋮ Reluplex: a calculus for reasoning about deep neural networks ⋮ State identification and verification with satisfaction ⋮ Neural Network Verification Using Residual Reasoning ⋮ Beyond NP: Quantifying over Answer Sets ⋮ Constraint CNF: SAT and CSP Language Under One Roof. ⋮ Dynamical Systems Theory and Algorithms for NP-hard Problems ⋮ MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks* ⋮ Approximate Automata for Omega-Regular Languages ⋮ Bounds on the size of PC and URC formulas ⋮ Witnessing matrix identities and proof complexity ⋮ Chain, Generalization of Covering Code, and Deterministic Algorithm for k-SAT ⋮ Proving Termination Through Conditional Termination ⋮ Congruence Closure with Free Variables ⋮ DPLL: The Core of Modern Satisfiability Solvers ⋮ Finding Effective SAT Partitionings Via Black-Box Optimization ⋮ Finding the Hardest Formulas for Resolution ⋮ Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting ⋮ A Novel Approach to Strategic Planning of Rail Freight Transport ⋮ Automatic Scheduling of Periodic Event Networks by SAT Solving ⋮ Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms ⋮ Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases ⋮ Automated Verification of Signalling Principles in Railway Interlocking Systems ⋮ Unnamed Item ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ A lower bound on CNF encodings of the at-most-one constraint ⋮ An adaptive prefix-assignment technique for symmetry reduction ⋮ Compression of Propositional Resolution Proofs via Partial Regularization ⋮ Inlining External Sources in Answer Set Programs ⋮ plasp 3: Towards Effective ASP Planning ⋮ A computational status update for exact rational mixed integer programming ⋮ Unnamed Item ⋮ Parameterised complexity of model checking and satisfiability in propositional dependence logic ⋮ Using Merging Variables-Based Local Search to Solve Special Variants of MaxSAT Problem ⋮ ICE-based refinement type discovery for higher-order functional programs ⋮ Merging Variables: One Technique of Search in Pseudo-Boolean Optimization ⋮ A Propositional CONEstrip Algorithm ⋮ Exact or approximate inference in graphical models: why the choice is dictated by the treewidth, and how variable elimination can be exploited ⋮ Unnamed Item ⋮ Boolean satisfiability in quantum compilation ⋮ Unnamed Item ⋮ Streamlining variational inference for constraint satisfaction problems ⋮ Good speciation and endogenous business cycles in a constraint satisfaction macroeconomic model ⋮ Varieties of mathematical understanding ⋮ Hard satisfiable 3-SAT instances via autocorrelation ⋮ On Linear Resolution ⋮ RC2: an Efficient MaxSAT Solver ⋮ Planning with Incomplete Information in Quantified Answer Set Programming ⋮ Study of discrete automaton models of gene networks of nonregular structure using symbolic calculations ⋮ Implementing Efficient All Solutions SAT Solvers ⋮ Comments on: ``An overview of curriculum-based course timetabling ⋮ Almost all Classical Theorems are Intuitionistic ⋮ On Quantifying Literals in Boolean Logic and its Applications to Explainable AI ⋮ Learning Optimal Decision Sets and Lists with SAT ⋮ A Volunteer-Computing-Based Grid Architecture Incorporating Idle Resources of Computational Clusters
Uses Software
