We express our gratitude to the reviewer for acknowledging our response.
1. *I understand that the proposed approach adds literals to clauses in
the UNSAT core rather than creating additional clauses. However,
there seems to be a conflict, as mentioned in Figure 2: "As
steps (1) and (2) are repeated, the core gradually becomes larger,
raising the hardness of the generated instance." This sentence
should be further clarified to avoid misunderstandings.*\
\
We agree that the sentence needs to be edited and we will revise it.
We will amend the text to clarify that the core we consider at each
step is specifically the easiest core (because traditional core
detection effectively solves the SAT problem). We also intend to
replace references to the "enlarging" of cores with their
"hardening" in order to emphasize our crucial assumption as
discussed previously. Thus, this phrase would read: "As steps (1)
and (2) are repeated, the easiest core of the problem is gradually
refined, raising the hardness of the generated instances."
2. *I noticed the global rebuttal results that demonstrate
generalization ability. However, the selected \"Tseitin\" family
likely shares a similar distribution with LEC problems, since LEC
data is also converted into CNF using the Tseitin Transformation.
Could the authors clarify this assumption? I suggest the authors
test the proposed approaches on non-circuit-based families and novel
cases in SAT benchmarks, such as cryptography and scheduling.*\
While it is true that the LEC and Tseitin data share an element of
origin, we note that the Tseitin data is made up of problems
generated in many different but random ways. For example, the
data-points contributed by Elfers in the 2016 Hand-Crafted track
\[1\] are generated by providing grid-graphs of varying dimensions
to the Tseitin transformation. These grid-graphs are very different
from the circuit-graphs seen during LEC. In consequence we see very
different runtime-distributions. Comparing Figure 2 in the rebuttal
pdf to Figure 6 in Appendix B of the paper and Figure 4 in the text,
we note significant differences. Most notably, Solvers 1 and 6
(which we generally have found to be strong for industrial data and
weak for random data, are much slower for the Tseitin data).
Therefore, we do not believe the Tseitin data shares a similar
distribution to the LEC data as the reviewer has suggested.
Additionally, while other data such as Cryptography and Scheduling
were considered, Tseitin was the family with the most UNSAT problems
available in the benchmarks. Since more data enable us to provide
more complete distributional experimentation as well as more results
on the data augmentation task, we chose the largest dataset: the
Tseitin.
With that said, we have begun experiments on a dataset of 100
scheduling problems taken from the SAT Competition data using the
filter "`family=scheduling and result=unsat`". Of the two families
suggested by the reviewer, scheduling had more problems, and so we
chose it over cryptography. If time permits for completion before
the end of the discussion period we will share results. Otherwise,
we will report the fully processed results in the appendix of the
revised paper.
\[1\] *Proceedings of SAT Competition 2016: Solver and Benchmark
Descriptions*, volume B-2016-1 of Department of Computer Science
Series of Publications B, University of Helsinki 2016. ISBN
978-951-51-2345-9.