key: cord-0046699-8crdtoq5
authors: Yolcu, Emre; Wu, Xinyu; Heule, Marijn J. H.
title: Mycielski Graphs and [Formula: see text] Proofs
date: 2020-06-26
journal: Theory and Applications of Satisfiability Testing - SAT 2020
DOI: 10.1007/978-3-030-51825-7_15
sha: 2182092a5a28a523766941ff33e355e4dd1e9bbd
doc_id: 46699
cord_uid: 8crdtoq5

Mycielski graphs are a family of triangle-free graphs [Formula: see text] with arbitrarily high chromatic number. [Formula: see text] has chromatic number k and there is a short informal proof of this fact, yet finding proofs of it via automated reasoning techniques has proved to be a challenging task. In this paper, we study the complexity of clausal proofs of the uncolorability of [Formula: see text] with [Formula: see text] colors. In particular, we consider variants of the [Formula: see text] (propagation redundancy) proof system that are without new variables, and with or without deletion. These proof systems are of interest due to their potential uses for proof search. As our main result, we present a sublinear-length and constant-width [Formula: see text] proof without new variables or deletion. We also implement a proof generator and verify the correctness of our proof. Furthermore, we consider formulas extended with clauses from the proof until a short resolution proof exists, and investigate the performance of CDCL in finding the short proof. This turns out to be difficult for CDCL with the standard heuristics. Finally, we describe an approach inspired by SAT sweeping to find proofs of these extended formulas.

Proof complexity investigates the relative strengths of Cook-Reckhow proof systems [7] , defined in terms of the length of the shortest proof of a tautology as a function of the length of the tautology. Proof systems are separated with respect to their strengths by establishing lower and upper bounds on the lengths of the proofs of certain "difficult" tautologies in each system. Finding short proofs of such tautologies in a proof system is a method for proving small upper bounds, which provide evidence for the strength of a proof system. Similarly, the existence of a large lower bound implies that a proof system is relatively weak. The related field of SAT solving involves the study of search algorithms that have corresponding proof systems, and concerns itself with not only the existence of short proofs, but also the prospect of finding them automatically when they exist. As a result, the two areas interact. The long-term agenda of proof complexity is to prove lower bounds on proof systems of increasing strength towards concluding NP = co-NP, whereas SAT solving benefits from strong proof systems with properties that make them suitable for automation. A recently proposed such system is PR (propagation redundancy) [14] and some of its variants SPR (subset PR), PR − (without new variables), DPR − (allowing deletion).

For several difficult tautologies, PR has been shown to admit proofs that are short (at most polynomial length), narrow (small clause width), and without extension (disallowing new variables) [5, 12, 13, 14] . From the perspective of proof search, these are favorable qualities for a proof system: -Polynomial length is essentially a necessity.

-Small width implies that we may limit the search to narrow proofs. -Eliminating extension drastically shrinks the search space.

Compared to strong proof systems with extension, a proof system with the above properties may admit a proof search algorithm that is effective in practice.

Mycielski graphs are a family of triangle-free graphs M k with arbitrarily high chromatic number. In particular, M k has chromatic number k. Despite having a simple informal proof, this has been a difficult fact to prove via automated reasoning techniques, and the state-of-the-art tools can only handle instances up to M 6 or M 7 [6, 9, 18, 19, 20, 21, 23] . Symmetry breaking [8] , a crucial automated reasoning technique for hard graph coloring instances, is hardly effective on these graphs as the largest clique has size 2. Most short PR proofs for hard problems are based on symmetry arguments. Donald Knuth challenged us in personal communication 1 to explore whether short PR proofs exist for Mycielski graph formulas.

In this paper, we provide short proofs in PR − and DPR − for the colorability of Mycielski graphs [17] . Our proofs are of length quasilinear (with deletion and low discrepancy) and sublinear (without deletion but high discrepancy) in the length of the original formula, and include clauses that are at most ternary. With deletion allowed, the PR inferences have short witnesses, which allows us to additionally establish the existence of quasilinear-length DSPR − proofs. We also implement a proof generator and verify the generated proofs with dpr-trim 2 . Furthermore, we experiment with adding various combinations of the clauses in the proofs to the formulas and observe their effect on conflict-driven clause learning (CDCL) solver [3, 16] performance. It turns out that the resulting formulas are still difficult for state-of-the-art CDCL solvers despite the existence of short resolution proofs, reinforcing a recent result by Vinyals [22] . We then demonstrate an approach inspired by SAT sweeping [24] to solve these difficult formulas automatically.

In this work we focus on propositional formulas in conjunctive normal form (CNF), which consist of the following: n Boolean variables, at most 2n literals p i and p i referring to different polarities of variables, and m clauses C 1 , . . . , C m where each clause is a disjunction of literals. The CNF formula is the conjunction of all clauses. Formulas in CNF can be treated as sets of clauses, and clauses as 1 Email correspondence on May 25, 2019 2 https://github.com/marijnheule/dpr-trim sets of literals. For two clauses C, D such that p ∈ C, p ∈ D, their resolvent on p is the clause (C \ {p}) ∪ (D \ {p}). A clause is called a tautology if it includes both p and p. We denote the empty clause by ⊥.

An assignment α is a partial mapping of variables in a formula to truth values in {0, 1}. We denote assignments by a conjunction of the literals they satisfy. As an example, the assignment x → 1, y → 0, z → 1 is denoted by x ∧ y ∧ z. The set of variables assigned by α is denoted by dom(α). We denote by F | α the restriction of a formula F under an assignment α, the formula obtained by removing satisfied clauses and falsified literals from F . A clause C is said to block the assignment α = p∈C p, which we denote by C.

A clause is called unit if it contains a single literal. Unit propagation refers to the iterative procedure where we assign the variables in a formula F to satisfy the unit clauses, restrict the formula under the assignment, and repeat until no unit clauses remain. If this procedure yields the empty clause ⊥, we say that unit propagation derives a conflict on F .

Assume for the rest of the paper that F, H are formulas in CNF, C is a clause, and α is the assignment blocked by C. Formulas F, H are equisatisfiable if either they are both satisfiable or both unsatisfiable. C is redundant with respect to F if F and F ∧ C are equisatisfiable. C is blocked with respect to F if there exists a literal p ∈ C such that for each clause D ∈ F that includes p, the resolvent of C and D on p is a tautology [15] . C is a reverse unit propagation (RUP) inference from F if unit propagation derives a conflict on F ∧ α [11] . F implies H by unit propagation, denoted F 1 H, if each clause C ∈ H is a RUP inference from F . Let us state a lemma about implication by unit propagation for later use.

). Let C, D be clauses such that C ∨ D is not a tautology and let α be the assignment blocked by C. Then

Letting x i be either a unit clause or a conjunction of unit clauses, we will use the notation

This serves as a compact way of writing a sequence of unit clauses that become true on the way to deriving x N from F via unit propagation.

Redundancy is the basis for clausal proof systems. In a clausal proof of a contradiction, we start with the formula and introduce redundant clauses until we can finally introduce the empty clause. Since satisfiability is preserved at each step due to redundancy, introduction of the empty clause implies that the formula is unsatisfiable. The sequence of redundant clauses constitutes a proof of the formula. Also note that since only unsatisfiable formulas are of interest, we use "proof" and "refutation" interchangeably. Definition 1. For a formula F , a valid clausal proof of it is a sequence of clause-witness pairs (C 1 , ω 1 ), . . . , (C N , ω N ) where, defining F i := F ∧ i j=1 C j , we have -each clause C i is redundant with respect to the conjunction of the formula with the preceding clauses in the proof, that is,

For a clausal proof P of length N , we call max i∈{1,...,N } |C i | its width.

Note that propagation redundancy can be decided in polynomial time given a witness ω due to the existence of efficient unit propagation algorithms. Unit propagation is a core primitive in SAT solvers, and despite the prevalence of large collections of heuristics implemented in solvers, in practice the majority of the runtime of a SAT solver is spent performing unit propagation inferences.

). If C is propagation redundant with respect to F , then it is redundant with respect to F . Theorem 1 allows us to define a specific clausal proof system:

Resolvents, blocked clauses, and RUP inferences are propagation redundant. Hence they are valid steps in a PR proof.

Let us also mention a few notable variants of the PR proof system:

-SPR: For each clause-witness pair (C i , ω i ) in the proof and α i the assignment blocked by C i , require that dom(ω i ) = dom(α i ). -PR − : No clause C in the proof can include a variable that does not occur in the formula F being proven. -DPR: In addition to introducing redundant clauses, allow deletion of a previous clause in the proof (or the original formula), that is, allow

Following the notation of Buss and Thapen [5] , the prefix "D" denotes a variant of a proof system with deletion allowed, and the superscript "−" denotes a variant disallowing new variables.

Intuition PR allows us to introduce clauses that intuitively support the following reasoning:

If there exists a satisfying assignment, then there exists a satisfying assignment with a certain property X, described by the witness ω. This is because we can take any assignment that does not have X, apply a transformation to it that does not violate any original constraints of the formula, and obtain a new satisfying assignment with property X. The validation of such a transformation in general is NP-hard. Transformations are limited such that they can be validated using unit propagation.

Hence, if our goal is to find some (not all) of the satisfying assignments to a formula or to refute it, then we can extend the formula by introducing useful assumptions without harming our goal since satisfiability is preserved with each assumption. The redundancy of each assumption is efficiently checkable using the blocked assignment α and the witness ω which together describe the transformation that we apply to a solution without property X to obtain another with X. Having this kind of understanding and mentally executing unit propagation allows us to look for PR proofs while continuing to reason at a relatively intuitive level. This proves useful when working towards upper bounds.

Upper bounds For several difficult tautologies (pigeonhole principle, bit pigeonhole principle, parity principle, clique-coloring principle, Tseitin tautologies) short SPR − proofs exist [5, 14] . Still, there are several problems mentioned by Buss and Thapen [5] for which there are no known PR − proofs of polynomial length. Furthermore, we do not know whether there are short SPR − proofs of the Mycielski graph formulas. Buss and Thapen [5] have a partial simulation result between SPR − and PR − depending on a notion called "discrepancy", defined as follows.

For a PR inference, its discrepancy is |dom(ω) \ dom(α)|.

Then, F has an SPR refutation of length O(2 δ N ) without using variables not in the PR refutation.

As a result, a PR proof of length N with maximum discrepancy at most log N directly gives an SPR proof of length O(N 2 ). In our case, the maximum discrepancy of the PR − proof is Ω(N/(log N ) 2 ), hence we cannot utilize Theorem 2 to obtain a polynomial-length SPR − proof. For our DPR − proof, the maximum discrepancy is 2, and by Theorem 2 there do exist quasilinear-length DSPR − proofs of the Mycielski graph formulas.

Let G = (V, E) be a graph. Its Mycielski graph μ(G) is constructed as follows:

1. Include G in μ(G) as a subgraph.

Unless G has a triangle μ(G) does not have a triangle, and μ(G) has chromatic number one higher than G. We denote the chromatic number of G by χ(G).

Starting with M 2 = K 2 (the complete graph on 2 vertices) and applying M k = μ(M k−1 ) repeatedly, we obtain triangle-free graphs with arbitrarily large chromatic number. We call M k the kth Mycielski graph. Since χ(M 2 ) = 2 and μ increases the chromatic number by one, we have Let us denote by MYC k the contradiction that M k is colorable with k − 1 colors. We will present short PR − and DPR − proofs of MYC k in Section 4.2. Before doing so, let us present the short informal argument to prove that applying μ increases the chromatic number, which implies that χ(M k ) > k − 1.

Proof. Assume we partition the vertices of μ(G) as V ∪ U ∪ {w} where V is the set of vertices of G which is included as a subgraph, U is the set of newly added vertices corresponding to each vertex in V , and w is the vertex that is connected to all of U .

Assume that in this coloring U uses only the first k − 1 colors. Then we can

and copying φ for the remaining vertices. The coloring φ is proper, because for

As a result, we can obtain a proper (k − 1)-coloring of G, contradiction. Hence, U must use at least k colors in a proper coloring of μ(G), and since w then has to have a color greater than k we have χ(μ(G)) > k = χ(G).

Proof. Follows from the fact that χ(M 2 ) = 2 and Proposition 1 via induction.

To obtain PR − and DPR − proofs, we follow a different kind of reasoning than that of the informal proof in the previous section. Let k ≥ 3. Denote by v i , E k−1 the vertices and the edge set of the (k−1)th Mycielski graph, respectively. Assume we partition the vertices of M k as in the proof of Proposition

For both the PR − and the DPR − proofs, the high-level strategy is to introduce clauses that effectively insert edges between any u i , u j for which v i v j ∈ E k−1 . In other words, if there is an edge v i v j , we introduce clauses that imply the existence of the edge u i u j , resulting in the modified graph M k that has an induced subgraph M k [U ] isomorphic to M k−1 , and has all of its vertices connected to w. As an example, Figure 3a shows the result of this step on M 4 . Then we partition the vertices of M k [U ] into new V ∪ U ∪ {w} similar to the way we did for M k . Such a partition exists as M k [U ] is isomorphic to M k−1 which by construction has this partition. Then we inductively repeat the whole process. Figure 3c displays the result of repeating it once. Finally, the added edges result in a k-clique in M k , as illustrated in Figure 3d . The vertices that participate in the clique are the two u i 's of the subgraph we obtain at the last step that is isomorphic to M 3 and the w's of all the intermediate graphs isomorphic to M k for k ∈ [k] \ {1, 2}. Since we have k − 1 colors available, the problem then reduces to the pigeonhole principle with k pigeons and k − 1 holes (denoted PHP k−1 ), for which we know there exists a polynomial-length PR − proof due to Heule et al. [14] . At the end we simply concatenate the pigeonhole proof for the clique, which derives the empty clause as desired.

The primary difference between the versions of the proof with and without deletion is the discrepancy of the PR inferences. Deletion allows us to detach

, as illustrated in Figure 3b , by removing each preceding clause that contains both a variable corresponding to some vertex in U and another corresponding to some vertex in V . This makes it possible to introduce the PR clauses with discrepancy bounded by a constant. Without deletion, we instead introduce the PR inferences at each inductive step which imply that every u i ∈ U has the same color as its corresponding v i , and this requires us to keep track of sets of equivalent vertices and assign them together in the witnesses. Figure 4 displays the effect of introducing these clauses on M 4 .

For ease of presentation, we first describe the DPR − proof, followed by the PR − proof. Proof. At each step below, let F denote the conjunction of MYC k with the clauses introduced in the previous steps.

for each c, c ∈ [k − 1] such that c < c . These clauses assert that each vertex in the graph can be assumed to have at most one color.

Intuitively, these clauses introduce the assumption that if there exists a solution, then there exists a solution that does not simultaneously have v i colored c, u i colored c , and w not colored c. If u i has color c , then we can switch its color to c and still have a valid coloring. The validity of this new coloring is verifiable relying only on unit propagation inferences. It does not create any monochromatic edges between u i and v j ∈ N (v i ) ∩ V , as v j would already not have the color c. It also does not create a monochromatic edge between u i and w since w is already assumed not to have color c. Figure 2 shows this argument with a diagram. The corresponding witness for this transformation is ω = v i,c ∧ u i,c ∧ u i,c ∧ w c , leading to a discrepancy of 1. 

Due to the previously introduced blocked and PR clauses (from (1) and (2)) we have

Let D = u i,c ∨ u j,c and β = D. From the previous set of RUP inferences in (3) we have

Due to the edge u j v i we also have F | vi,c 1 u j,c and consequently F | β 1 u j,c . Since u j,c ∈ D, we have F | β 1 ⊥ by Lemma 1.

With the addition of this last set of assumptions, we have effectively copied the edges between v i to between u i . Figure 3a visualizes the result of this step on M 4 with the red edges corresponding to the newly introduced assumptions. 5. After the addition of the new edges, we delete the clauses introduced in steps 2, 3, and the clauses corresponding to the edges between U and V of the current Mycielski graph. Figure 3b displays the graph after the deletions. 6. Then we inductively repeat steps 2-5, that is, we introduce clauses and delete the intermediate ones for each subgraph isomorphic to Mycielski graphs of descending order. Figure 3c shows the result of repeating the process on a subgraph isomorphic to M 3 , with the blue edges corresponding to the latest assumptions.

(a) Introduction of edge assumptions to obtain a subgraph isomorphic to the Mycielski graph of the previous order.

(b) Deletions of the clauses introduced previously and the edges between U, V to detach the subgraph.

(c) Repetition of the inductive step on the previously obtained subgraph isomorphic to M3.

(d) Detached clique obtained after deleting the clauses corresponding to the edges leaving the clique. 7. After an edge is inserted between the two u i of the subgraph isomorphic to M 3 , we obtain a k-clique on the two u i and all of the previous w's. Then we delete all the clauses corresponding to the edges leaving the clique. This detaches the clique from the rest of the graph as illustrated for M 4 in Figure 3d . Since (k − 1)-colorability of the k-clique is exactly the pigeonhole principle, we simply concatenate a PR − proof of the pigeonhole principle as described by Heule et al. [14] , which has maximum discrepancy 2. This completes the DPR − proof that M k is not colorable with k − 1 colors.

In total, the proof has length O(3 k k 2 ) and the PR inferences have maximum discrepancy 2. Hence, by Theorem 2, there also exists a DSPR − proof of length O(3 k k 2 ). Since MYC k has length Θ(3 k k), if we denote the length of the formula by S then the proof is of quasilinear length O(S log S).

Proof. At a high level, the proof is similar to the DPR − proof. However, in order to avoid deletion we introduce assumptions at each inductive step that imply the equivalence of every u i with its corresponding v i . This eliminates the need to detach M k [U ] from M k [V ], but leads to sets of vertices forced to have the same color. As a result, the witnesses for the PR inferences after the first inductive step that refer to switching the color of a vertex ν need to also include all the previous vertices forced to have the same color as ν.

1. We start by introducing the blocked clauses from (1). 2. Then we introduce the PR inferences from (2).

3. It becomes possible to infer the following |U |(k − 1)(k − 2) clauses via PR.

Let γ = u i,c ∧ v i,c , and denote the conjunction of the formula and the clauses in (1) and (2) by F . In step 3 of the previous proof we showed that

Then, by Lemma 1, we have F | γ 1 u j,c . Hence, we can switch the color of v i from c to c. This does not result in any conflicts since u i having color c implies that no v j ∈ N (v i ) ∩ V has the color c, and u j,c is implied by unit propagation. As a result, the clause

After the addition of these clauses, the equivalence u i,c ↔ v i,c is implied via unit propagation. Due to the edge v i v j , the existence of the edge u i u j is also implied via unit propagation. This step allows us to avoid deletion. 4. At this point, we inductively repeat steps 2-3 for each subgraph isomorphic to Mycielski graphs of descending order. However, due to the equivalences u i,c ↔ v i,c , any subsequent PR inference that argues by way of switching a vertex ν's color should include in its witness the same color switch for all the vertices that are transitively equivalent to ν from the previous steps. For instance, if a witness contains ν c ∧ ν c , then for each vertex η that is equivalent to ν it also has to contain η c ∧ η c . The maximum number of such vertices for any ν occurring in the proof is Ω(2 k ). 5. After the PR clauses are introduced for the subgraph isomorphic to M 3 , the existence of a k-clique is implied via unit propagation. Figure 4 shows the equivalent vertices and the implied edges after the last inductive step when starting from M 4 . At the end, we simply concatenate a proof of the pigeonhole principle as before, taking care to include in the witnesses all the equivalent vertices (as described in the previous step) to each vertex whose color is switched by a witness. The proof has length O(2 k k 2 ), and MYC k has length Θ(3 k k). Letting S denote the length of the formula, the proof has sublinear length O(S log 3 2 (log S) 2 ).

In the PR − proof, the maximum discrepancy is Ω(2 k ). Letting N be the length of the proof, this becomes Ω(N/(log N ) 2 ). As a result, we cannot rely on Theorem 2, and the existence of a polynomial-length SPR − proof for Mycielski graph formulas remains open. While the existence of such a proof is plausible, we conjecture that it will not be of constant width as the ones we present.

All of the formulas, proofs, and the code for our experiments are available at https://github.com/emreyolcu/mycielski.

In order to verify the proofs we described in the previous section, we implemented two proof generators for MYC k and checked the DPR − and PR − proofs with dpr-trim for values of k from 5 to 10. Figure 5 shows a plot of the lengths of the formulas and the proofs, and Table 1 shows their exact sizes. 

Suppose we have a proof search algorithm for DPR − and that the redundant clauses we introduce in the DPR − proof are discovered automatically. Assuming they are found by some method, we look at their effect on the efficiency of CDCL at finding the rest of the proof automatically. In addition, we generate satisfiable instances of the coloring problem (denoted MYC + k and stating that M k is colorable with k colors) and compare how many of the satisfying assignments remain after the clauses are introduced. The reduction in the number of solutions suggests that the added clauses do a significant amount of work in breaking symmetries. Let us denote by -BC: the blocked clauses that we add in step 1, -PR: the PR clauses that we add inductively in step 2, -R1: the RUP inferences that we add inductively in step 3, -R2: the RUP inferences that we add inductively in step 4.

We consider extended versions of the formulas where we gradually include more of the redundant clauses. We cumulatively introduce the redundant clauses from each step, i.e. when we add the PR clauses we also add the BC clauses. For the satisfiable formulas MYC + k , the remaining number of solutions are in Table 2 . We used allsat 3 to count the exact number of solutions. Adding only the BC or PR clauses drastically reduces the number of solutions. Adding them both leaves a fraction of the solutions.

For the unsatisfiable formulas, we ran CaDiCaL 4 [3] with a timeout of 2000 seconds on the original formulas and the versions including the clauses introduced at each step. The results are in Table 3 . These runtimes are somewhat unexpected as R1 and R2 can be derived from MYC k +PR with relatively few resolution steps. One would therefore expect the performance on MYC k +PR, MYC k +R1, and MYC k +R2 to be similar. We study this observation in the next subsection.

The CDCL paradigm has been highly successful, because it has been able to find short refutations for problems arising from various applications. However, the above results show that there exist formulas for which CDCL cannot find the short refutations. In particular, the MYC k +PR formulas have length Θ(3 k k) and there exist resolution refutations of length O(3 k k 3 ): Each clause in R1 and R2, of which there are O(3 k k 2 ), can be derived in O(k) steps of resolution. As for the clique, it is known that PHP k−1 has resolution refutations of length O(2 k k 3 ) [4] .

This shows that, even if we devise an algorithm to discover the redundant PR clauses automatically, the Mycielski graph formulas still remain difficult for the standard tools. After the clauses in BC and PR become part of the formula, the difficulty lies in deriving the R2 clauses automatically. If we resort to incremental SAT solving [10] and provide the cubes u i,c ∧ u j,c (negation of each clause in R2) as assumptions to the solver, the formulas become relatively easily solvable. For instance, MYC 10 +PR takes approximately 3 minutes on a single CPU. Although it is unlikely that a solver can run this efficiently without any explicit guidance, the small runtime provides evidence that the shortest resolution proof of MYC 10 +PR is of modest length.

In this section, we describe a method for discovering useful cubes automatically and using them to solve the MYC k +PR formulas. While inefficient, with this method it at least becomes possible to find proofs of these formulas in a matter of minutes, compared to CDCL which did not succeed even with a timeout of three days on MYC 10 +PR. Given a formula F , the below procedure discovers binary clauses, inserts them to F , and attempts to solve F via CDCL.

1. Iteratively remove the clause that has the largest number of resolution candidates until the formula becomes satisfiable. For MYC k +PR, this corresponds to simply removing the clause w 1 ∨ . . . ∨ w k−1 . Call the newly obtained formula, which is satisfiable, F − . 2. Repeat:

(a) Sample M satisfying assignments for F − using a local search solver (we used YalSAT 5 [2] ). (b) Find all pairs of literals (l i , l j ) that do not appear together in any of the solutions sampled so far. Form a list with the cubes l i ∧ l j , and shuffle it in order to avoid ordering the pairs with respect to variable indices. In the case of MYC k +PR, the clause u i,c ∨ u j,c is implied by F − , hence (u i,c , u j,c ) must be among the pairs found. (c) If the number of pairs found did not decrease by more than 1 percent after the latest addition of satisfying assignments, break. 3. Repeat:

(a) Partition the remaining cubes into P pieces. Use P workers in parallel to perform incremental solving with a limit of L conflicts allowed on the instances of the formula F using each separate piece as the set of assumptions. Aggregate a list of refuted cubes. (b) For each refuted cube B, append B to the formula F . (c) If the number of refuted cubes is less than half of the previous iteration, break. 4. Run CDCL on the final formula F that includes negations of all the refuted cubes. Table 4 displays the results for formulas with k ∈ {7, . . . , 10} and varying numbers of parallel workers P . Table 4 . Results on finding proofs for MYC k +PR. From left to right, the columns correspond to the number of samples used for obtaining a list of cubes, the number of cubes obtained after filtering pairs of literals, time it takes to sample solutions using a local search solver with 20 workers and filter pairs of literals, maximum number L of conflicts allowed to the incremental SAT solver, number of parallel workers P , total time it takes to refute cubes and prove unsatisfiability of the final formula F , percentage of time spent in the final CDCL run on F , number of iterations spent refuting cubes and adding them to the formula. 

We showed that there exist short DPR − , DSPR − , and PR − proofs of the colorability of Mycielski graphs. Interesting questions about the proof complexity of PR variants remain. For instance, DPR − has not been shown to separate from ER or Frege, and even simpler questions regarding upper bounds for some difficult tautologies are open. It is also unknown, although plausible, whether there exists a polynomial-length SPR − proof of the Mycielski graph formulas. Apart from our theoretical results, we encountered formulas with short resolution proofs for which CDCL requires substantial runtime. We developed an automated reasoning method to solve these formulas. In future work, we plan to study whether this method is also effective on other problems that are challenging for CDCL.

The On-Line Encyclopedia of Integer Sequences

CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT competition 2017

CaDiCaL at the SAT Race

Resolution and the weak pigeonhole principle

DRAT proofs, propagation redundancy, and extended resolution

Coloring graphs by iterated local search traversing feasible and infeasible solutions

The relative efficiency of propositional proof systems

Symmetry-breaking predicates for search problems

Efficient algorithms for finding critical subgraphs

Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science

Verification of proofs of unsatisfiability for CNF formulas

What a difference a variable makes

Clausal proofs of mutilated chessboards

Strong extension-free proof systems

On a generalization of extended resolution

GRASP-a new search algorithm for satisfiability

Sur le coloriage des graphs

Breaking instanceindependent symmetries in exact graph coloring

Dynamic symmetry breaking by simulating Zykov contraction

Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems

Another look at graph coloring via propositional satisfiability

Hard examples for common variable decision heuristics

An exact algorithm with learning for the graph coloring problem

SAT sweeping with local observability don't-cares

Acknowledgements. This work has been supported by the National Science Foundation (NSF) under grant CCF-1813993.