全部 标题 作者
关键词 摘要

OALib Journal期刊
ISSN: 2333-9721
费用:99美元

查看量下载量

相关文章

更多...

A framework for good SAT translations, with applications to CNF representations of XOR constraints

Full-Text   Cite this paper   Add to My Lib

Abstract:

We present a general framework for good CNF-representations of boolean constraints, to be used for translating decision problems into SAT problems (i.e., deciding satisfiability for conjunctive normal forms). We apply it to the representation of systems of XOR-constraints, also known as systems of linear equations over the two-element field, or systems of parity constraints. The general framework defines the notion of "representation", and provides several methods to measure the quality of the representation by the complexity ("hardness") needed for making implicit "knowledge" of the representation explicit (to a SAT-solving mechanism). We obtain general upper and lower bounds. Applied to systems of XOR-constraints, we show a super-polynomial lower bound on "good" representations under very general circumstances. A corresponding upper bound shows fixed-parameter tractability in the number of constraints. The measurement underlying this upper bound ignores the auxiliary variables needed for shorter representations of XOR-constraints. Improved upper bounds (for special cases) take them into account, and a rich picture begins to emerge, under the various hardness measurements.

Full-Text

Contact Us

service@oalib.com

QQ:3279437679

WhatsApp +8615387084133