SAT-Based Formula Simplification

DOI10.1007/978-3-319-24318-4_21MaRDI QIDQ3453233zbMATHOpenAlexFDO

Authors A. A. Ignatiev, Alessandro Previti, Joao Marques-Silva

Publication date 20 November 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-24318-4_21

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05)

Recommendations

• scientific article; zbMATH DE number 2090300
• An Improved SAT Algorithm in Terms of Formula Length
• Formalization and implementation of modern SAT solvers
• scientific article; zbMATH DE number 2080337
• Theory and Applications of Satisfiability Testing
• A fast algorithm for SAT in terms of formula length
• Theory and Applications of Satisfiability Testing
• scientific article; zbMATH DE number 1099516
• scientific article; zbMATH DE number 1903355
• Efficient SAT solving under assumptions

Cites work

• scientific article; zbMATH DE number 3902554 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• scientific article; zbMATH DE number 918600 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A GRASP algorithm to solve the unicost set covering problem
• A Way to Simplify Truth Functions
• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• A note on the complexity of Boolean concepts
• A theory of diagnosis from first principles
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Complexity minimization in rule-based category learning: revising the catalog of Boolean concepts and evidence for non-minimal rules
• Efficient 2 and 3-flip neighborhood search algorithms for the MAX SAT: experimental Evaluation
• Efficient Privacy-Preserving Ciphertext-Policy Attribute Based-Encryption and Broadcast Encryption
• Enumerating prime implicants of propositional formulae in conjunctive normal form
• Fast, flexible MUS enumeration
• Improving Glucose for incremental SAT solving with assumptions: application to MUS extraction
• Input Variable Assignment and Output Phase Optimization of PLA's
• Iterative and core-guided maxsat solving: a survey and assessment
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Logic minimization techniques with applications to cryptology
• Minimal Logic Programs
• Progression in maximum satisfiability
• Quantified maximum satisfiability
• Quantified maximum satisfiability: a core-guided approach
• Redundancy in logic. I: CNF propositional formulae
• The Problem of Simplifying Truth Functions
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Towards efficient MUS extraction
• Two-level logic minimization: an overview

Cited in

(8)

• On simplification of formulas with unconstrained variables and quantifiers
• Minimizing models for Tseitin-encoded SAT instances
• Two-level logic minimization: an overview
• McColl and minimization
• scientific article; zbMATH DE number 2080337 (Why is no real title available?)
• Theory and Applications of Satisfiability Testing
• Optimal symmetry breaking for graph problems
• Minimal sets on propositional formulae. Problems and reductions

Describes a project that uses

Uses Software

• MiniSat
• Glucose
• ABC

This page was built for publication: SAT-Based Formula Simplification

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