Lookahead saturation with restriction for SAT
| dc.contributor.author | Anbulagan, Anbu | |
| dc.contributor.author | Slaney, John K | |
| dc.contributor.editor | Peter van Beek | |
| dc.coverage.spatial | Sitges Spain | |
| dc.date.accessioned | 2015-12-10T21:55:55Z | |
| dc.date.available | 2015-12-10T21:55:55Z | |
| dc.date.created | October 1-5 2005 | |
| dc.date.issued | 2005 | |
| dc.date.updated | 2024-04-21T08:16:01Z | |
| dc.description.abstract | We present; a new and more efficient heuristic by restricting lookahead saturation (LAS) with NVO (neighbourhood variable ordering) and DEW (dynamic equality weighting). We report on the integration of this heuristic in Satz, a high-performance SAT solver, showing empirically that it significantly improves the performance on an extensive range of benchmark problems that exhibit, hard structure. | |
| dc.identifier.isbn | 9783540292388 | |
| dc.identifier.uri | http://hdl.handle.net/1885/39185 | |
| dc.publisher | Springer | |
| dc.relation.ispartofseries | International Conference on Principles and Practice of Constraint Programming (CP 2005) | |
| dc.source | Proceedings of International Conference on Principles and Practice of Constraint Programming (CP 2005) | |
| dc.subject | Keywords: Benchmarking; Dynamic programming; Function evaluation; Heuristic methods; Problem solving; Benchmark problems; Dynamic equality weighting (DEW); Lookahead saturation (LAS); Neighbourhood variable ordering (NVO); Computer programming | |
| dc.title | Lookahead saturation with restriction for SAT | |
| dc.type | Conference paper | |
| local.bibliographicCitation.lastpage | 731 | |
| local.bibliographicCitation.startpage | 727 | |
| local.contributor.affiliation | Anbulagan, Anbu, College of Engineering and Computer Science, ANU | |
| local.contributor.affiliation | Slaney, John K, College of Engineering and Computer Science, ANU | |
| local.contributor.authoremail | u4593416@anu.edu.au | |
| local.contributor.authoruid | Anbulagan, Anbu, u4593416 | |
| local.contributor.authoruid | Slaney, John K, u8800435 | |
| local.description.notes | Imported from ARIES | |
| local.description.refereed | Yes | |
| local.identifier.absfor | 080199 - Artificial Intelligence and Image Processing not elsewhere classified | |
| local.identifier.ariespublication | MigratedxPub173 | |
| local.identifier.doi | 10.1007/11564751_53 | |
| local.identifier.scopusID | 2-s2.0-33646189654 | |
| local.identifier.thomsonID | 000233596400053 | |
| local.identifier.uidSubmittedBy | Migrated | |
| local.type.status | Published Version |