Distributed clause-sharing SAT solvers are powerful automated reasoning tools capable of rapidly solving many difficult instances. Users of SAT solving often rely on incremental SAT solving, i.e., interactive solve calls over an evolving formula. We present the first approach to distributed incremental SAT solving that grants full confidence in the obtained result. Specifically, we extend a recent distributed real-time proof checking approach with an incremental proof interface. Our approach offers great flexibility in that it supports dynamic re-scheduling of computational resources and enables safely sharing clauses across tasks that operate on deviating assumptions and formula increments. We further add on-the-fly clause compression to checkers in order to reduce memory consumption. Experiments with the distributed solver MallobSat on up to 1216 cores show that our trusted solving approach checks incremental SAT tasks with small mean overhead ( \(< 33\) %) over unchecked solving.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Real-time Proof Checking for Distributed Incremental SAT Solving

  • Dominik Schreiber,
  • Mathias Fleury,
  • Katalin Fazekas,
  • Armin Biere

摘要

Distributed clause-sharing SAT solvers are powerful automated reasoning tools capable of rapidly solving many difficult instances. Users of SAT solving often rely on incremental SAT solving, i.e., interactive solve calls over an evolving formula. We present the first approach to distributed incremental SAT solving that grants full confidence in the obtained result. Specifically, we extend a recent distributed real-time proof checking approach with an incremental proof interface. Our approach offers great flexibility in that it supports dynamic re-scheduling of computational resources and enables safely sharing clauses across tasks that operate on deviating assumptions and formula increments. We further add on-the-fly clause compression to checkers in order to reduce memory consumption. Experiments with the distributed solver MallobSat on up to 1216 cores show that our trusted solving approach checks incremental SAT tasks with small mean overhead ( \(< 33\) %) over unchecked solving.