Loading...
Please wait, while we are loading the content...
Similar Documents
Resolution and Clause Learning for Multi-Valued CNF
| Content Provider | CiteSeerX |
|---|---|
| Author | Mitchell, David |
| Abstract | Abstract. Conflict-directed clause learning (CDCL) is the basis of SAT solvers with impressive performance on many problems. CDCL with restarts (CDCL-R) has been shown to have essentially the same rea-soning power as unrestricted resolution (formally, they p-Simulate each other). We show that this property generalizes to multi-valued CNF for-mulas. In particular, for Signed (or Multi-Valued) CNF formulas, and Regular Formulas, we show that a natural generalization of CDCL-R to these logics has essentially the same reasoning power as natural gener-alizations of resolution from the literature. These formulas are possible reduction targets for a number of multi-valued logics, and thus a possible basis for efficient reasoning systems for these logics. 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Clause Learning Multi-valued Cnf Natural Generalization Regular Formula Conflict-directed Clause Learning Unrestricted Resolution Cnf Formula Rea-soning Power Sat Solver Multi-valued Cnf For-mulas Multi-valued Logic Many Problem Possible Basis Possible Reduction Target Natural Gener-alizations Impressive Performance |
| Content Type | Text |
| Resource Type | Article |
