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

DOI10.1007/s10472-005-2369-1zbMath1099.68104MaRDI QIDQ1776200

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

density; satisfiability; 3-SAT; Horn

Mathematics Subject Classification ID

68T27: Logic in artificial intelligence

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

Uses Software

• UnitWalk

Cites Work

• Unnamed Item
• Unnamed Item
• Some simplified NP-complete graph problems
• 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
• Variable and term removal from Boolean formulae
• Phase transitions and complexity in computer science: An overview of the statistical physics approach to the random satisfiability problem
• UnitWalk: A new SAT solver that uses local search guided by unit clause elimination
• Solving satisfiability problems using elliptic approximations. A note on volumes and weights
• Maximum renamable Horn sub-CNFs
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Sharp thresholds of graph properties, and the $k$-sat problem
• Theory and Applications of Satisfiability Testing
• The complexity of theorem-proving procedures
• Theory and Applications of Satisfiability Testing