Efficient Conflict Driven Learning in a Boolean Satisfiability Solver

Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. Lintao Zhang, Madigan, C., Moskewicz, M., & Malik, S. In IEEE/ACM International Conference on Computer Aided Design. ICCAD 2001. IEEE/ACM Digest of Technical Papers (Cat. No.01CH37281), pages 279–285.

Paper doi abstract bibtex

One of the most important features of current state-of-the-art SAT solvers is the use of conflict based backtracking and learning techniques. In this paper, we generalize various conflict driven learning strategies in terms of different partitioning schemes of the implication graph. We re-examine the learning techniques used in various SAT solvers and propose an array of new learning schemes. Extensive experiments with real world examples show that the best performing new learning scheme has at least a 2X speedup compared with learning schemes employed in state-of-the-art SAT solvers.

@inproceedings{lintaozhangEfficientConflictDriven2001,
  title = {Efficient Conflict Driven Learning in a {{Boolean}} Satisfiability Solver},
  isbn = {0-7803-7247-6},
  url = {http://ieeexplore.ieee.org/document/968634/},
  doi = {10.1109/ICCAD.2001.968634},
  abstract = {One of the most important features of current state-of-the-art SAT solvers is the use of conflict based backtracking and learning techniques. In this paper, we generalize various conflict driven learning strategies in terms of different partitioning schemes of the implication graph. We re-examine the learning techniques used in various SAT solvers and propose an array of new learning schemes. Extensive experiments with real world examples show that the best performing new learning scheme has at least a 2X speedup compared with learning schemes employed in state-of-the-art SAT solvers.},
  booktitle = {{{IEEE}}/{{ACM International Conference}} on {{Computer Aided Design}}. {{ICCAD}} 2001. {{IEEE}}/{{ACM Digest}} of {{Technical Papers}} ({{Cat}}. {{No}}.{{01CH37281}})},
  date = {2001},
  pages = {279--285},
  keywords = {CDCL,Clause Learning,Learning,SAT,UIP First UIP},
  author = {{Lintao Zhang} and Madigan, C.F. and Moskewicz, M.H. and Malik, S.},
  file = {/home/dimitri/Nextcloud/Zotero/storage/L78I4MD2/cdcl.pdf}
}

Downloads: 0

{"_id":"dHAz357iPZtEXiDyp","bibbaseid":"lintaozhang-madigan-moskewicz-malik-efficientconflictdrivenlearninginabooleansatisfiabilitysolver","authorIDs":[],"author_short":["Lintao Zhang","Madigan, C.","Moskewicz, M.","Malik, S."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Efficient Conflict Driven Learning in a Boolean Satisfiability Solver","isbn":"0-7803-7247-6","url":"http://ieeexplore.ieee.org/document/968634/","doi":"10.1109/ICCAD.2001.968634","abstract":"One of the most important features of current state-of-the-art SAT solvers is the use of conflict based backtracking and learning techniques. In this paper, we generalize various conflict driven learning strategies in terms of different partitioning schemes of the implication graph. We re-examine the learning techniques used in various SAT solvers and propose an array of new learning schemes. Extensive experiments with real world examples show that the best performing new learning scheme has at least a 2X speedup compared with learning schemes employed in state-of-the-art SAT solvers.","booktitle":"IEEE/ACM International Conference on Computer Aided Design. ICCAD 2001. IEEE/ACM Digest of Technical Papers (Cat. No.01CH37281)","date":"2001","pages":"279–285","keywords":"CDCL,Clause Learning,Learning,SAT,UIP First UIP","author":[{"firstnames":[],"propositions":[],"lastnames":["Lintao Zhang"],"suffixes":[]},{"propositions":[],"lastnames":["Madigan"],"firstnames":["C.F."],"suffixes":[]},{"propositions":[],"lastnames":["Moskewicz"],"firstnames":["M.H."],"suffixes":[]},{"propositions":[],"lastnames":["Malik"],"firstnames":["S."],"suffixes":[]}],"file":"/home/dimitri/Nextcloud/Zotero/storage/L78I4MD2/cdcl.pdf","bibtex":"@inproceedings{lintaozhangEfficientConflictDriven2001,\n title = {Efficient Conflict Driven Learning in a {{Boolean}} Satisfiability Solver},\n isbn = {0-7803-7247-6},\n url = {http://ieeexplore.ieee.org/document/968634/},\n doi = {10.1109/ICCAD.2001.968634},\n abstract = {One of the most important features of current state-of-the-art SAT solvers is the use of conflict based backtracking and learning techniques. In this paper, we generalize various conflict driven learning strategies in terms of different partitioning schemes of the implication graph. We re-examine the learning techniques used in various SAT solvers and propose an array of new learning schemes. Extensive experiments with real world examples show that the best performing new learning scheme has at least a 2X speedup compared with learning schemes employed in state-of-the-art SAT solvers.},\n booktitle = {{{IEEE}}/{{ACM International Conference}} on {{Computer Aided Design}}. {{ICCAD}} 2001. {{IEEE}}/{{ACM Digest}} of {{Technical Papers}} ({{Cat}}. {{No}}.{{01CH37281}})},\n date = {2001},\n pages = {279--285},\n keywords = {CDCL,Clause Learning,Learning,SAT,UIP First UIP},\n author = {{Lintao Zhang} and Madigan, C.F. and Moskewicz, M.H. and Malik, S.},\n file = {/home/dimitri/Nextcloud/Zotero/storage/L78I4MD2/cdcl.pdf}\n}\n\n","author_short":["Lintao Zhang","Madigan, C.","Moskewicz, M.","Malik, S."],"key":"lintaozhangEfficientConflictDriven2001","id":"lintaozhangEfficientConflictDriven2001","bibbaseid":"lintaozhang-madigan-moskewicz-malik-efficientconflictdrivenlearninginabooleansatisfiabilitysolver","role":"author","urls":{"Paper":"http://ieeexplore.ieee.org/document/968634/"},"keyword":["CDCL","Clause Learning","Learning","SAT","UIP First UIP"],"downloads":0},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/dlozeve/newblog/master/bib/all.bib","creationDate":"2020-01-08T20:39:39.020Z","downloads":0,"keywords":["cdcl","clause learning","learning","sat","uip first uip"],"search_terms":["efficient","conflict","driven","learning","boolean","satisfiability","solver","lintao zhang","madigan","moskewicz","malik"],"title":"Efficient Conflict Driven Learning in a Boolean Satisfiability Solver","year":null,"dataSources":["3XqdvqRE7zuX4cm8m"]}