Exponential Recency Weighted Average Branching Heuristic for SAT Solvers
Authors: Jia Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki
AAAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We evaluated CHB on 1200 instances from the SAT Competition 2013 and 2014 instances, and showed that CHB solves significantly more instances than VSIDS, currently the most effective branching heuristic in widespread use. |
| Researcher Affiliation | Academia | Jia Hui Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki jliang@gsd.uwaterloo.ca, vijay.ganesh@uwaterloo.ca ppoupart@uwaterloo.ca, kczarnec@gsd.uwaterloo.ca University of Waterloo, Canada |
| Pseudocode | Yes | Algorithm 1 a simple CDCL solver with CHB as the branching heuristic. |
| Open Source Code | No | The paper mentions implementing CHB within Mini Sat and Glucose solvers but does not provide an explicit statement or a link to the open-source code for their modified versions. |
| Open Datasets | Yes | First, CHB was evaluated on all 1200 instances from the application and hand-crafted categories of the SAT Competition 2013 and 2014 benchmarks. |
| Dataset Splits | No | The paper evaluates on the SAT Competition 2013 and 2014 benchmarks as a whole and does not specify traditional training, validation, or test dataset splits. |
| Hardware Specification | Yes | Each run was executed on Star Exec (Stump, Sutcliffe, and Tinelli 2014), a platform designed for evaluating logic solvers. The Star Exec platform uses the Intel Xeon CPU E5-2609 at 2.40GHz with 10240 KB cache and 24 GB of main memory, running on Red Hat Enterprise Linux Workstation release 6.3, and Linux kernel 2.6.32-431.1.2.el6.x86 64. |
| Software Dependencies | Yes | CHB was evaluated on 2 notable CDCL SAT solvers: Mini Sat version 2.2.0 (Sorensson and Een 2005) and Glucose version 4.0 (Audemard and Simon 2009a). |
| Experiment Setup | Yes | Each run of a solver was given 5000 seconds and 7.5 GB of memory to solve an instance, as per the rules of SAT Competition 2013. |