Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances

DOI10.1007/S10472-005-2369-1MaRDI QIDQ1776200zbMATH OpenOpenAlexFDO

Authors Hans van Maaren, Linda van Norden

Publication date 20 May 2005

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-005-2369-1

zbMATH Keywords

3-SATdensityHornsatisfiability

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2080304
• Theory and Applications of Satisfiability Testing
• scientific article; zbMATH DE number 1305521
• scientific article; zbMATH DE number 2083805
• scientific article; zbMATH DE number 2151254

Cites work

• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
• scientific article; zbMATH DE number 2084700 (Why is no real title available?)
• scientific article; zbMATH DE number 1369843 (Why is no real title available?)
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Maximum renamable Horn sub-CNFs
• Phase transitions and complexity in computer science: An overview of the statistical physics approach to the random satisfiability problem
• Sharp thresholds of graph properties, and the k-sat problem
• Solving satisfiability problems using elliptic approximations. A note on volumes and weights
• Some simplified NP-complete graph problems
• The complexity of theorem-proving procedures
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• UnitWalk: A new SAT solver that uses local search guided by unit clause elimination
• Variable and term removal from Boolean formulae

Describes a project that uses

Uses Software

• UnitWalk

This page was built for publication: Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances

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