Modelling more realistic SAT problems

Abstract

The satisfiability problem is widely used in research on combinatorial search and for industrial applications such as verification and planning. Real world search problem benchmarks are not plentiful, yet understanding search algorithm behaviour in the real world domain is highly important. This work justifies and investigates a randomised satisfiability problem model with modular properties akin to those observed in real world search problem domains. The proposed problem model provides a reliable benchmark which highlights pitfalls and advantages with various satisfiability search algorithms.