资源论文Read-Once Resolution for Unsatis?ability-Based Max-SAT Algorithms ?

Read-Once Resolution for Unsatis?ability-Based Max-SAT Algorithms ?

2019-11-12 | |  60 |   32 |   0
Abstract This paper proposes the integration of the resolution rule for Max-SAT with unsatis?ability-based Max-SAT solvers. First, we show that the resolution rule for Max-SAT can be safely applied as dictated by the resolution proof associated with an unsatis?able core when such proof is read-once, that is, each clause is used at most once in the resolution process. Second, we study how this property can be integrated in an unsatis?ability-based solver. In particular, the resolution rule for MaxSAT is applied to read-once proofs or to read-once subparts of a general proof. Finally, we perform an empirical investigation on structured instances from recent Max-SAT evaluations. Preliminary results show that the use of read-once resolution substantially improves the performance of the solver.

上一篇:Minimization for Generalized Boolean Formulas ? Edith Hemaspaandra Henning Schnoor

下一篇:Real-Time Heuristic Search with Depression Avoidance Carlos Herna?ndez Jorge A. Baier

用户评价
全部评价

热门资源

  • Learning to Predi...

    Much of model-based reinforcement learning invo...

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • The Variational S...

    Unlike traditional images which do not offer in...

  • Learning to learn...

    The move from hand-designed features to learned...

  • A Mathematical Mo...

    Direct democracy, where each voter casts one vo...