Learning from conflicts in propositional satisfiability

DOI10.1007/S10288-011-0191-7MaRDI QIDQ427560zbMATH OpenOpenAlexFDO

Authors Youssef Hamadi, Said Jabbour, Lakhdar Sais

Publication date 13 June 2012

Published in 4OR (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10288-011-0191-7

zbMATH Keywords

constraint satisfactionsatisfiabilityconflict learning

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in artificial intelligence (68T27)

Recommendations

• What we can learn from conflicts in propositional satisfiability
• Publication:5715680
• On the power of clause-learning SAT solvers as resolution engines
• Generalized conflict-clause strengthening for satisfiability solvers
• Propositional SAT solving

Cites work

• scientific article; zbMATH DE number 1324220 (Why is no real title available?)
• scientific article; zbMATH DE number 1149402 (Why is no real title available?)
• scientific article; zbMATH DE number 1550909 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A Generalized Framework for Conflict Analysis
• A Machine-Oriented Logic Based on the Resolution Principle
• A Way to Simplify Truth Functions
• A linear-time transformation of linear inequalities into conjunctive normal form
• A machine program for theorem-proving
• Adaptive Restart Strategies for Conflict Driven SAT Solvers
• Branch-and-cut solution of inference problems in propositional logic
• Clause elimination procedures for CNF formulas
• Efficient CNF simplification based on binary implication graphs
• Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
• Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
• Input Proofs and Rank One Cutting Planes
• ManySAT: a parallel SAT solver
• On freezing and reactivating learnt clauses
• Optimal speedup of Las Vegas algorithms
• Solving propositional satisfiability problems
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(18)

• Learning to select branching rules in the DPLL procedure for satisfiability
• Generalized conflict-clause strengthening for satisfiability solvers
• Surveys in operations research
• IntSat: integer linear programming by conflict-driven constraint learning
• What we can learn from conflicts in propositional satisfiability
• Deciding floating-point logic with abstract conflict driven clause learning
• Twelve surveys in operations research
• Learning Disjunctions: Near-Optimal Trade-off between Mistakes and “I Don't Knows”
• Stronger Inference through Implied Literals from Conflicts and Knapsack Covers
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• CrystalBall: gazing in the black box of SAT solving
• Extended clause learning
• Clause-learning for modular systems
• Logic Programming and Nonmonotonic Reasoning
• Abstract conflict driven learning
• Conflict-driven XOR-clause learning
• A Generalized Framework for Conflict Analysis
• BDD-guided clause generation

Describes a project that uses

Uses Software

• DIMACS
• Chaff
• SATO
• MiniSat
• ManySAT

This page was built for publication: Learning from conflicts in propositional satisfiability

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