Frédéric Besson

Itauto: An Extensible Intuitionistic SAT Solver

Keywords: 2012 ACM Subject Classification Theory of computation → Automated reasoning; Computing methodologies → Theorem proving algorithms SAT solver, proof by reflection Digital Object Identifier 10, 4230/LIPIcs, ITP, 2021, 9

We present the design and implementation of itauto, a Coq reflexive tactic for intuitionistic propositional logic. The tactic inherits features found in modern SAT solvers: definitional conjunctive normal form; lazy unit propagation and conflict driven backjumping. Formulae are hash-consed using native integers thus enabling a fast equality test and a pervasive use of Patricia Trees. We also propose a hybrid proof by reflection scheme whereby the extracted solver calls user-defined tactics on the leaves of the propositional proof search thus enabling theory reasoning and the generation of conflict clauses. The solver has decent efficiency and is more scalable than existing tactics on synthetic benchmarks and preliminary experiments are encouraging for existing developments.

Introduction

Using an ideal proof-assistant, proofs would be written at high-level and mundane proof tasks would be discharged by automated procedures. However, automated reasoning is hard; even more so for sceptical [START_REF] Harrison | A Skeptic's Approach to Combining HOL and Maple[END_REF] proof-assistants: generating and verifying proofs at scale, even for decidable logic fragments, is a challenge requiring sophisticated implementation strategies [START_REF] Böhme | Fast LCF-Style Proof Reconstruction for Z3[END_REF][START_REF] Besson | Modular SMT Proofs for Fast Reflexive Checking Inside Coq[END_REF][START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF]. For the Coq proof-assistant, the situation is made slightly worse because intuitionistic logic is not mainstream for automated provers. Thus, the Satisfiability Modulo Theory (SMT) approach that is based on a classical SAT solver needs to be revisited.

Propositional Reasoning and Theory Reasoning in Coq

There are a variety of Coq tactics which perform intuitionistic propositional and theory reasoning. We describe here their main features and explain some limitations, thus motivating the need for a novel (extensible) solver for intuitionistic propositional logic (IPL). We defer to Section 6 the discussion of related approaches rooted in a classical setting and interfacing with external provers. tauto 1 is a complete decision procedure for IPL based on the LJT* calculus [START_REF] Dyckhoff | Contraction-Free Sequent Calculi for Intuitionistic Logic[END_REF]. rtauto 2 is another decision procedure for IPL verifying proof certificates using proof by reflection. These decision procedures are usually efficient enough for interactive use but do not perform theory reasoning. lia 3 is a decision procedure for linear arithmetic. It has a classical understanding of propositional connectives but abstracts away non-arithmetic propositions. congruence 4 [11] does not perform propositional reasoning but decides the theory of equality with constructors. Another tactic that is worth mentioning is intuition tac5 ; it first performs propositional reasoning and calls the leaf tactic tac when it gets stuck. (tauto is actually intuition fail.)

In a classical setting, calling a theory solver on the leaves of a propositional proof search is the basis of the DPLL(T ) algorithm [START_REF] Ganzinger | DPLL( T): Fast Decision Procedures[END_REF]. Unfortunately, in an intuitionistic setting, completeness is lost. Example 1 illustrates the issue.

▶ Example 1 (Incomplete Combination). Consider the following goals. For Ex1 and Ex2, intuition lia (resp. intuition congruence) fail whereas the goal can be decided using a combination of propositional logic with the theory of linear arithmetic and the theory of equality, respectively. The reason is that the intuition part does nothing and therefore calls the leaf tactic on the unmodified goal. For Ex1, lia abstracts away non-arithmetic propositions 6 and is left with the non-theorem x=0→(x>=0→True)→False. For Ex2, congruence abstracts away propositions and is also left with a non-theorem: a=b→b=c→False.

Besides completeness, intuition tac may also call the leaf tactic tac more often than necessary. This is illustrated by Example 2.

▶ Example 2 (Spurious Leaf Tactic Call). Consider the following goal. Lemma Ex3:∀(A:Type)(x y t:A)(p q:Prop),x=y→p∨q→(p→y=t)→(q→y=t)→x=t.

In this case, intuition congruence performs a case-split over p\/q, and derives y=t by modus-ponens. Eventually, it calls the leaf tactic congruence twice. However, in both branches, congruence solves the same theory problem i.e., x=y → y=t → x=t.

Contribution

A first contribution is the design and implementation of a reflexive intuitionistic SAT solver in Coq. The SAT solver obtains decent performances using features found in state-of-the-art SAT solvers such as hash-consing, lazy unit propagation, backjumping and theory learning. It also makes a pervasive use of native machine integers 7 and Patricia Trees [START_REF] Okasaki | Fast mergeable integer maps[END_REF].

Another contribution is a variation of the proof by reflection approach whereby the verified extracted SAT solver is first run inside the proof engine. Theory reasoning is then performs by calling user-defined tactics on the leaves of the propositional proof search. Following the DPLL(T ) approach, minimal conflict clauses obtained from the tactic proof-terms are passed back to the SAT solver. Eventually, a proof is obtained by asserting the conflict clauses and re-running the reflexive SAT solver with an empty theory module. To our knowledge, this design combining reflexive code with tactics is original.

F. Besson

9:3

The rest of the paper is organised as follows. In Section 2, we present the main features of our SAT solver and its implementation in Coq. The structure of the soundness proof is detailed in Section 3. In Section 4, we explain how to interface the SAT solver with the proof engine and user-defined tactics. We show experimental results in Section 5. Related work is presented in Section 6 and Section 7 concludes.

Note that the code snippets in the paper have been edited and idealised for clarity.

Design of an Intuitionistic SAT solver

Our algorithm is reusing several key components of modern SAT solvers. Fortunately, they are only slightly adapted to the intuitionistic setting.

Syntax and Semantics of Formulae

Our SAT solver takes as input hash-consed [START_REF] Allen | Anatomy of LISP[END_REF] formulae defined by the inductive type LForm. The interpretation of a formula f:LFORM is given by structural recursion with respect to an environment e:int → Prop mapping indexes i.e., propositional variables, to propositions.

LFF e = False LAT i e = e i LOP AND [f 1 ; . . . ; f n ] e = f 1 e ∧ • • • ∧ f n e LOP OR [f 1 ; . . . ; f n ] e = f 1 e ∨ • • • ∨ f n e LIMPL [f 1 ; . . . ; f n ] f e = f 1 e → • • • → f n e → f e
In the following, as the environment e is fixed, we drop the subscript and write f for f e .

Intuitionistic Clausal Form

In a classical setting, to prove that a formula f is a tautology, a modern SAT solver proves that the conjunctive normal form (CNF) of the negation of f is unsatisfiable. In other words, a SAT solver exploits the fact that ¬(¬f ) is equivalent to f and that the CNF conversion preserves provability. In an intuitionistic setting, this approach is not feasible because reductio ad adsurdum is not logically sound and the usual CNF conversion requires De Morgan laws which are not admissible. Yet, Claessen and Rosén [START_REF] Claessen | SAT Modulo Intuitionistic Implications[END_REF] show that it is possible to transform an intuitionistic formula f into an equi-provable formula of the form F ∧ I → q where q is a variable ; f ∈ F is a so-called flat clause of the form p 1 → . . . p n → q 1 ∨ • • • ∨ q m where the p i and q i are variables and i ∈ I is a so-called implication clause of the form (a → b) → c where a, b and c are variables. The transformation is based on Tseitin definitional CNF [START_REF] Tseitin | On the Complexity of Derivation in Propositional Calculus[END_REF] I T P 2 0 2 1 with the modification that a clause is written

p 1 → • • • → p n → q 1 ∨ • • • ∨ q n instead of ¬p 1 ∨ • • • ∨ ¬p n ∨ q 1 • • • ∨ q n .
The implication clauses are reminiscent of the fact that double arrows (e.g., in the LJT proof system) need a treatment that is specific to intuitionistic logic.

Our implementation is along these lines but optimises the transformation in order to reduce both the set of flat clauses and implication clauses. To reduce the set of flat clauses, our definitional CNF is based on Plaisted and Greenbaum CNF [START_REF] Plaisted | A Structure-Preserving Clause Form Translation[END_REF] which exploits the polarity of formulae and uses memoization thus avoiding recomputing the CNF of identical sub-formulae. In order to reduce the set of implication clauses, we exploit the fact that, if the conclusion q is decidable, intuitionistic logic reduces to classical logic. In that case, it is therefore admissible to replace an implication clause (a → b) → c by the equivalent flat clauses {a ∨ c; b → c}. Moreover, before performing CNF conversion, formulae are flattened using the associativity of ∧ and ∨. This has the advantage of augmenting the arity of the operators, reducing the depth of the formulae, and therefore reducing the number of intermediate propositional variables.

Pre-processing

The input formula is only using binary operators. To obtain n-ary operators, we recursively apply the following equivalences (the operator + + is the concatenation of lists):

LOP OR (LOP OR l 1 ) :: l 2 = LOP OR (l 1 + + l 2 ) LOP AND (LOP AND l 1 ) :: l 2 = LOP AND (l 1 + + l 2 ) LIMPL (LOP AND l 1 ) ::

l 2 r = LIMPL (l 1 + + l 2 ) r LIMPL l 1 (LIMPLl 2 r) = LIMPL (l 1 + + l 2 ) r

Literals

Tseitin style CNF [START_REF] Tseitin | On the Complexity of Derivation in Propositional Calculus[END_REF] consists in introducing fresh propositional variables. In a proofassistant, modelling freshness may incur some proof overhead. Fortunately, in our case, the new propositional variables are not arbitrary but correspond to sub-formulae. As a result, we represent a propositional variable by a hash-consed formula (HFormula = HCons.t LForm) and a literal is a positive or negative hash-consed formula.

Inductive literal : Type := | POS (f: HFormula) | NEG (f: HFormula)

As usual, a clause is a list of positive and negative literals but with the following interpretation.

NEGf :: l e = f e → l e POSf ::

l e = f e ∨ l e [] e = False
For readability, we will write ⌊f ⌋ for POSf and ⌊f ⌋ → for NEGf . A singleton clause [NEGf ] will be written ⌊f ⌋ → ⊥. In the remaining, we have the invariant that the negative literals are always before the positive literals. As a result, a general clause [NEGf 1 ; . . . ; NEGf i ; POSg 1 ; . . . ; POSg j ] will be written

⌊f 1 ⌋ → • • • → ⌊f i ⌋ → ⌊g 1 ⌋ ∨ • • • ∨ ⌊g j ⌋ or more compactly i ⌊f i ⌋ → j ⌊g j ⌋.
Moreover, we define the negation of a literal l: ¬l is such that ¬⌊f ⌋ = ⌊f ⌋ → and ¬⌊f →⌋ = ⌊f ⌋.

Introduction Rule

Before running the CNF conversion per se, we inspect the formula and perform reductio ad adsurdum if possible. The function intro_impl performs the introduction rule for implication with the twist that the conclusion is double negated if it is decidable. Therefore, intro_impl: HFormula → (list literal * HFormula) takes as input a hash-consed formula and returns a pair (l, c) where l are hypotheses and c is the conclusion. The constant HLFF is the hash-consed formula LFF i.e., the syntax for the proposition False.

The is_dec predicate is implemented by a boolean flag stored together with the hash-cons of the formula. It is recursively propagated from atomic propositions that are known to be classical i.e., we have r ∨ ¬r.

Construction of the CNF

The next step consists in computing the CNF of the literals and of the formula in the conclusion. We recursively compute for a positive literal CNFi.e., a set of clauses modelling the elimination rule; and for a negative literal (or the conclusion) CNF+ i.e., a set of clauses modelling the introduction rule.

f = (f 1 ∧ • • • ∧ f n ) AND-(f ) = {⌊f ⌋ → ⌊f 1 ⌋; . . . ; ⌊f ⌋ → ⌊f n ⌋} AND+(f ) = {⌊f 1 ⌋ → • • • → ⌊f n ⌋ → ⌊f ⌋} f = (f 1 ∨ • • • ∨ f n ) OR-(f ) = {⌊f ⌋ → ⌊f 1 ⌋ ∨ • • • ∨ ⌊f n ⌋} OR+(f ) = {⌊f 1 ⌋ → ⌊f ⌋; . . . ; ⌊f n ⌋ → ⌊f ⌋} f = (f 1 → • • • → f n → r) IMPL-(f ) = {⌊f ⌋ → ⌊f 1 ⌋ → • • • → ⌊f n ⌋ → ⌊r⌋} IMPL+(f ) = {⌊r⌋ → ⌊f ⌋} ∪ is_dec fi {⌊f i ⌋ ∨ ⌊f ⌋}
This clausal encoding is correct and the generated clauses are both classical and intuitionistic tautologies. Except for IMPL+, the clausal encoding is also complete e.g., we have

CNF+(f 1 ∧ • • • ∧ f n ) ∪ {⌊f 1 ⌋ ∧ • • • ∧ ⌊f n ⌋} ⊢ ⌊f 1 ∧ • • • ∧ f n ⌋ CNF-(f 1 ∧ • • • ∧ f n ) ∪ {⌊f 1 ∧ • • • ∧ f n ⌋} ⊢ ⌊f 1 ⌋ ∧ • • • ∧ ⌊f n ⌋
For IMPL+, if not all the f i are classical propositions, the clausal encoding is partial and we also keep the implication clause (⌊f 1 ⌋ → • • • → ⌊r⌋) → ⌊f ⌋ for later processing. An exception is when we intend to prove False. In that case, the IMPL+ rule may drop the requirement on the decidability of the f i thus providing a complete clausal encoding. This is sound because

for any f = (f 1 → • • • → f n → r), (⌊r⌋ → ⌊f ⌋) ∧ fi (⌊f i ⌋ ∨ ⌊f ⌋) → False is an intuitionistic tautology.
▶ Example 3. Suppose that we intend to prove the tautology (a

→ (b ∧ c)) → (b ∨ (a → c))
where a, b and c are intuitionistic propositional variables. After running the introduction rule, we obtain the following hypothesis and conclusion

{⌊a → (b ∧ c)⌋} ⊢ b ∨ (a → c)
We compute CNFfor the hypothesis i.e. IMPL-(⌊a → (b ∧ c)⌋), and CNF+ for the conclusion i.e., OR+(⌊d∨(a → c)⌋). Recursively, we compute AND-(b∧c) and IMPL+(a → c) and eventually obtain

       ⌊a → (b ∧ c)⌋, ⌊a → (b ∧ c)⌋ → ⌊a⌋ → ⌊b ∧ c⌋, ⌊b ∧ c⌋ → ⌊b⌋, ⌊b ∧ c⌋ → ⌊c⌋, ⌊b⌋ → ⌊b ∨ (a → c)⌋, ⌊a → c⌋ → ⌊b ∨ (a → c)⌋ ⌊c⌋ → ⌊a → c⌋, (⌊a⌋ → ⌊c⌋) → ⌊a → c⌋        ⊢ b ∨ (a → c)
Note that because a is an intuitionistic proposition, we keep the implication clause (⌊a⌋ → ⌊c⌋) → ⌊a → c⌋.

I T P 2 0 2 1

9:6

Itauto: An Extensible Intuitionistic SAT Solver

Lazy Unit Propagation

Once a clause is reduced to a single literal, say l, unit propagation simplifies all the remaining clauses using l. There are three cases to consider. If a clause c does not mention l, it is left unchanged. If the literal l belongs to the clause c, the clause is redundant and it is removed (see R1 and R2). If the negation of the literal l belongs to the clause, we deduce the simplified clause c \ ¬l (see M1 and M2). In logic terms, we have the following inferences:

R1 p p ∨ r R2 p → ⊥ p → r M1 p p → r r M2 p → ⊥ p ∨ r r
In the following, a literal l is said to be watched if neither [l] nor [¬l] is a unit clause. We also say that a literal l is assigned if it is not watched.

A naive unit propagation algorithm linearly traverses every clause and is therefore inefficient. A key observation is that the purpose of unit propagation is to produce new unit clauses. Said otherwise, it not necessary to traverse clauses where at least 2 literals are watched. As a result, a clause that is neither the empty clause nor the unit clause is represented by the type watched_clause given below.

Record watched_clause:={ watch1 : literal; watch2 : literal; unwatched : list literal }.

This is purely functional variant of so called head/tail lists 8 [START_REF] Zhang | An Efficient Algorithm for Unit Propagation[END_REF][START_REF] Zhang | Implementing the Davis-Putnam Method[END_REF] that is simpler than the 2-watched literals optimisation [START_REF] Moskewicz | Chaff: Engineering an Efficient SAT Solver[END_REF]. Watched clauses are indexed on their watched literals but also on whether the watched literals are positive or negative. To get an efficient representation of sets of clauses, each clause is given a unique identifier and is stored in a Patricia Tree [START_REF] Okasaki | Fast mergeable integer maps[END_REF]. In order to implement so-called non-chronological backtracking (see Section 2.4), we also track the set of literals that are needed to deduce a clause. As a result, each clause is annotated with a set of literals LitSet.t.

Record

F. Besson 9:7

EMPTY represents the empty clause, i.e. a contradiction. In that case, unit propagation concludes the proof. TRUE represents a redundant clause that will be dropped. UNIT l is a unit clause to be propagated and CLAUSE wc is a watched clause. Without loss of generality, suppose that ⌊f ⌋ belongs to the set of assigned literals s and that we have a clause c of the form:

c = {|watch1 := ¬⌊f ⌋; watch2 := x; unwatched := [y 1 ; . . . ; y n ; ]|}
The reduce function takes as input the watched literal x and aims at finding in the list [y 1 ; y n ; . . . ; y n ] a watched literal y i (i.e., y i is not assigned in s) and return as clause the rest of the list. If the list is empty, we produce the unit clause UNIT x and unit propagation will be recursively called for x. Let y be the head of the list l. If y is not assigned in s, we return a novel clause where the watched literals are x and y. If y is already assigned with the same polarity in s (y ∈ s), the clause is redundant and can be dropped. If y is already assigned but with opposite polarity (¬y ∈ s), the reduction is recursively called threading along the dependencies of the literal y.

▶ Example 4. Suppose that the set of assigned literals is given by s = {f ; ¬y 1 ; ¬y n } and we perform unit propagation over the clause c. By construction, we know that neither x nor ¬x are assigned in s. To get a well-defined watched clause with 2 watched literals, we need to find a replacement for the literal ¬⌊f ⌋ in the list [y 1 ; y 2 ; . . . ; y n ]. As {¬y 1 , ¬y n } ⊆ s, a greedy unit propagation would deduce that y 1 and y n can be removed but as the prohibitive cost of a linear scan of the whole clause. The idea of lazy unit propagation is to stop at the first unassigned literal i.e. y 2 . Therefore, we generate the watched clause {watche1 := x; watche2 := y 2 ; unwatched := [y 3 ; . . . ; y n ]}

Case Splitting and Backjumping

When all the unit clauses are propagated, the solver performs a case-split over a clause. The clause needs to represent a disjunction. If the conclusion is False, any clause may be selected. Otherwise, the clause may only contain either positive literals or negative classical literals. The soundness of this argument is expressed by the following inferences.

i Γ ∪ (pi → ⊥) ⊢ ⊥ j Γ ∪ qj ⊢ ⊥ Γ ∪ i pi → j qj ⊢ ⊥ i (pi ∨ ¬pi) i Γ ∪ (pi → ⊥) ⊢ g j Γ ∪ qj ⊢ g Γ ∪ i pi → j qj ⊢ g
A naive algorithm consists in doing a recursive call for each literal, say l i , of the clause. However, if for one of the cases, the proof does not depend on the literal l i , it is sound to ignore the other cases and immediately return (backjump) to a previous case-split. This is illustrated by Example 5.

I T P 2 0 2 1 9:8

Itauto: An Extensible Intuitionistic SAT Solver ▶ Example 5 (Backjumping). Consider the following goal where each clause H i is tagged with a set of dependencies d i where the d i are disjoint and do not contain the literals {l, m, n, o}.

{H 1 : (l ∨ m) d1 , H 2 : (n ∨ o) d2 , H 3 : (n → ⊥) d3 , H 4 : (o → ⊥) d4 } ⊢ ⊥
Suppose that we first perform a case-split over H 1 . For the first case, we introduce the unit clause H 5 : l {l} with a singleton dependency i.e., the literal only depends on itself. As no unit propagation is possible, we perform another case split over H 2 : (n ∨ o) d2 . For the case n, using H 3 , we derive the empty clause ⊥ d3∪{n} and for the case o, we derive the empty clause ⊥ d4∪{o} . Therefore, gathering both sub-cases, we have ⊥ d2∪d3∪d4 . As l / ∈ d 2 ∪ d 3 ∪ d 4 , the case-split over H 1 is irrelevant for the proof and, therefore, there is no need to explore the second case of the case-split over H 2 .

A propositional prover has the idealised type ProverT defined below.

ProverT := state → HFormula → option LitSet.t

It takes as input the prover state st, and the formula to prove g and returns, upon success, the set of literals that are needed for the proof. Details about the components of state are given in Section 2.7. The case_split algorithm is parametrised by a prover Prover:ProverT. It takes as input a clause cl and returns a prover performing a case-analysis over all the literals of the input clause cl. In addition to a set of literals, it returns a boolean indicating whether backjumping is possible. If the clause is empty i.e., it denotes False, the proof is finished. Suppose that f is the first literal of the clause cl, the prover is recursively called with the state st augmented with the unit clause f . If the proof d does not require f and all the literals in d are assigned in the current state (st ⊢ d), the whole case-split is spurious and the prover returns immediately. Otherwise, we recursively call case_split and return the updated set of literals needed by the proof. The literal f is momentarily removed from the dependencies of d but the dependencies are adjusted just after the case_split call by adding the dependencies of the clause cl.

Implication clauses

When there is no clause to branch over, the prover considers implication clauses and tries to (recursively) prove one of them. The function prover_arrows takes as argument a list l of literals. A literal f in the list is of the form POS(LIMPL [a 1 ; ...; a n ] b) which encodes an implication clause

⌊a 1 ⌋ → • • • → ⌊a n ⌋ → (⌊a 1 → • • • → a n → b⌋)
which was left aside during the CNF conversion. The prover is recursively called with, as goal, the formula i a i → b. If the proof succeeds, the literal f holds and the proof continues with a state augmented with f. Otherwise, the prover tries another literal.

Theory Reasoning

At leaves of the proof search, the solver has assigned a set of literals that do not lead to a propositional conflict. At this stage, a SAT solver reports that a model is found. Yet, this propositional model may be invalidated by performing theory reasoning. Our solver is parametrised by a theory reasoner. Essentially, it takes as input a list of literals and returns (upon success) a clause. The clause is a tautology of the theory that is added to the clauses of the SAT solver. The interface of a theory reasoner is given below.

Record Thy := { thy_prover : hmap → list literal → option (hmap * clause); thy_prover_sound : ∀ hm hm' cl cl', thy_prover hm cl = Some (hm',cl')

→ cl' ∧ hm ⊑ hm' ∧ ∀ l ∈ cl', l ∈ hm' }
A thy_prover takes as input a hash-cons map hm and a list of literals cl. The hash-cons map hm contains the currently hash-consed terms. The literals in the list cl are obtained from the current state of the SAT solver and are restricted to atomic formulae i.e., LAT i for some i. The theory prover may either fail to make progress or return an updated hash-cons map hm' and a clause cl' such that i) the clause cl' holds; ii) the literals in cl' are correctly hash-consed in hm'; iii) the updated hash-cons map hm' contains more hash-consed formulae than hm. Typically, the clause cl' is a conflict clause and therefore the literals of cl' are including in those of cl. However, we open the possibility to perform theory propagation and generate a clause made of new literals.

Solver State and Main Loop

Using the previous components, we are ready to detail the proof state.

Record state := { fresh_clause_id : int; hconsmap : hmap; arrows : list literal; wneg : iSet; defs : iSet * iSet; units : ptrie (Annot bool); unit_stack : list (Annot literal); clauses : watch_map }.

The field fresh_clause_id is a fresh index that is incremented each time a novel clause is created.

I T P 2 0 2 1 9:10

Itauto: An Extensible Intuitionistic SAT Solver

The field hconsmap is only updated by the theory prover and is used to ensure wellformedness conditions about hash-consing.

The field arrows contains a list of literals. Each literal is of the form IMPL[a 1 ; . . . ; a n ]b and represent an implication clauses i.e., (⌊a

1 ⌋ → • • • → ⌊a i ⌋ → ⌊b⌋) → Lita 1 → • • • → a i → b
which could not be turned into a proper flat clause during CNF conversion.

The field wneg contains a set of hash-cons indexes corresponding to watched negative literals. These literals are added to the list of literals sent to the theory prover. The field defs is a pair of sets of hash-cons indexes. These are used for memoizing the CNF+ and CNF-computations. The field units encodes using a Patricia Tree the set of assigned literals. The boolean indicates whether the literal is positive or negative and the annotation tells which sets of initial literals were needed for the deduction. The field unit_stack is the stack of literals for which unit propagation needs to be run. The field clauses contains the indexed watched_clauses.

The type of the implemented prover is slightly more complicated that what we explained in the Section 2.4. In addition to a set of literals, it also threads along a hmap and a list of clauses learnt by theory reasoning. Theory reasoning is only running if the boolean use_prover is set. Termination is ensured by provided some fuel computed (without proof) from the size of the formula. If the prover does not run out of fuel, it calls in sequence the different provers described in the previous sections. After performing unit propagation, it performs a case-split and recursively calls the prover. If no case-split is possible, it tries to prove one of the implication clause by recursively calling the prover. Eventually, if no implication clause can be derived, theory reasoning is called.

▶ Example 6 (Example 3 continued). Suppose that we have the proof state obtained after constructed the CNF for a → (b∧c) → (d∨(a → c)) (see Example 3). The literal ⌊a → (b∧c)⌋ triggers unit propagation and generates the clause ⌊a⌋ → ⌊b ∧ c⌋. At this stage, neither unit propagation nor case-splitting is possible. Yet, we have a single implication clause (⌊a⌋ → ⌊c⌋) → ⌊a → c⌋. Hence, we call prover_arrows with the singleton list [⌊a → c⌋]. To prove ⌊a → c⌋, we introduce ⌊a⌋ and attempt to prove c. By unit propagation, we derive first ⌊b ∧ c⌋ and then ⌊b⌋ and ⌊c⌋; thus concluding the sub-proof. As a result, we augment the context with ⌊a → c⌋ and conclude the goal by unit propagation.

Soundness Proof

In this part, we give some insights about the soundness proof that is based on three main properties: well-formedness, soundness of dependencies and soundness of provers. The only axioms of the development are those of the Int63 standard library which define native machine integers.

F. Besson

9:11

Well-formedness

Hash-consing has the advantage that the equality of terms can be decided by an equality of native integers without in-depth inspection of terms. However, this requires ensuring that the initial formula is correctly hash-consed and that the prover always operates with hash-consed literals. Fortunately, most of the generated literals are sub-formulae that are obtained by the CNF. The only exception is theory reasoning. The hash-consed formulae are stored in a map m : hmap := ptrie (bool*LForm). The keys of the map are the hash-cons indexes and the boolean indicates whether the formula is a classical proposition. The set of hash-consed formulae has_form m is inductively defined below.

m(i) = (true, LFF) LFF true i ∈ has_form m m(i) = (b, LAT i) b ↔ LAT i ∨ ¬ LAT i (LAT i) b i ∈ has_form m m(i) = (b, LOP o [_ b1 i1 ; . . . ; _ bn in ]) (f 1 ) b1 i1 ∈ has_form m . . . (f n ) bn in ∈ has_form m b ↔ b 1 ∧ • • • ∧ b n (LOP o [(f 1 ) b1 i1 ; . . . ; (f n ) bn in ]) b i ∈ has_form m m(i) = (b, LIMPL[_ b1 i1 ; . . . ; _ bn in ] _ b0 i0 ) (f 0 ) b0 i0 ∈ has_form m . . . (f n ) bn in ∈ has_form m b ↔ b 0 ∧ • • • ∧ b n (LIMP[(f 1 ) b1 i1 ; . . . ; (f n ) bn in ] (f 0 ) b0 i0 ) b i ∈ has_form m
Essentially, this consists in checking that all the sub-formulae are stored within the hmap m when only considering the top constructor and the hash-cons index of the sub-formulae. The advantage of this formulation is that f b i ∈ hash_form m can be checked algorithmically by a linear pass over the formula f . This definition also entails that formulae with the same hash-cons index are the same.

f b1 i ∈ has_form m ∧ g b2 i ∈ has_form m → f b1 i = g b2 i
Our well-formedness conditions state that a solver state st:state only contains hashconsed formulae. In particular, all the literals in the clauses are hash-consed formulae. As Patricia Trees come with structural invariants, every Patricia Tree needs to be well-formed. In the prover state, the set of assigned literals (see the units field) is represented by a Patricia Tree ptrie (Annot.t bool) where the keys are hash-consed indexes. In this case, the well-formedness conditions requires that there exists a hash-consed formula corresponding to this index. As all the formulae with the same hash-cons index are equal this identifies a unique formula.

wf_units_lit u m = ∀i, v, u(i) = v → ∃f b i , has_form m f b i
The proofs of preservation are compositional and do not pose any particular issue.

Soundness of Dependencies

The logical objects in the proof state are the set of indexed watched clauses (clauses) , the set of assigned literals (units) and the stack of literals that are yet to be unit-propagated (unit_stack). Each clause (or literal) is also annotated by the set of literals needed for the deduction. These sets are represented by Patricia Trees using hash-consed indexes as keys.

I T P 2 0 2 1

9:12

Itauto: An Extensible Intuitionistic SAT Solver

We write c d (resp. l d ) for a (watched) clause (resp. literal) annotated with a set of literals d. For each operation, we prove that the annotation is sound i.e. the conjunction of the literals in d entails the clause c (resp. the literal l). The interpretation is indexed by a hash-cons map m linking indexes to hash-consed formulae.

c {l1,...,ln} m = l 1 m ∧ . . . l n m → c
A literal l is introduced by either the introduction rule or a case-split. In that case, the set d is the singleton {l} and l {l} holds. New clauses are obtained by unit propagation and the soundness of the deduced clauses is obtained from the following deduction rules:

d 1 → p d 2 → (p → p 1 → . . . p n → q 1 ∨ . . . q n ) d 1 ∧ d 2 → (p 1 → . . . p n → q 1 ∨ . . . q n ) d 1 → ¬q d 2 → (q ∨ q 1 ∨ . . . q n ) d 1 ∧ d 2 → (q 1 ∨ . . . q n ) Syntactically, the conjunction d 1 ∧ d 2 is modelled by the union d 1 ∪ d 2 . d 1 ∪ d 2 m = d 1 m ∧ d 1 m
Given a prover state st, st dep holds if all the clauses (resp. literals) in the state have correct dependencies. The proofs that the dependencies are correct are also compositional but require well-formedness conditions to hold.

Soundness of Provers

Upon success, a prover p:ProverT returns a set of valid learnt clause, an updated hash-cons map but also a set of literals that are sufficient to entail a conflict. The soundness of provers is then stated by the following definition.

Definition sound_prover (prover: ProverT) (st: state) := ∀ g hm lc d, wf_state st → g b i ∈ hconsmap st → prover st g = Success (m,lc,d) →

( st → st dep → g ) ∧ ( st dep → d m → g ) ∧ c∈lc c
Therefore, soundness requires to prove that the goal formula g is entailed by either the clauses in the state and their dependencies or the dependencies alone and the set of literals d. Both properties are needed in order to prove that backjumping is correct. We also have to prove that the clauses lc obtained by theory reasoning are sound. Sometimes, the fact that we use classical reasoning in an intuitionistic context is a source of complication for the proof because this prevents a direct forward reasoning. For instance, in a pure classical context, the CNF of a formula f generates tautologies and the correctness can be directly stated by

∀cl, cl ∈ cnf f → cl
The correctness of our CNF depends on the goal formula. For instance, if the conclusion is False, De Morgan laws are admissible. Therefore, our formulation is the following.

((∀cl, cl ∈ cnf f → cl ) → g ) → g
Note that if g = False, we get a double negation. For most of our proof state transformation, say T, a simplified correctness lemma has the form

wf_state st → ( T st → g ) → ( st → g ) F. Besson 9:13 4

Proof by Hybrid Reflection

Having a SAT solver for deciding propositional logic, one option is to directly perform proof by reflection [START_REF] Castéran | Interactive theorem proving and program development. Coq'Art: The Calculus of inductive constructions[END_REF]Chap. 16]. Using this mode, we get a tactic that is similar to the existing tauto with the advantage that our reification process detects decidable propositions declared using the type-class mechanism [START_REF] Sozeau | First-Class Type Classes[END_REF].

In order to perform theory reasoning, the proof by reflection approach demands that we implement the interface of Section 2.6. However, a closer look shows that the interface does not expose a syntax for atoms: they are only represented by indexes. In a nutshell, the interface is purposely an empty shell. A fully reflexive approach would require to enrich the interface with an environment mapping atoms to theory-specific syntactic terms. Here, we follow a different path and implement theory reasoning using classic user-defined tactics. The advantages are that existing decision procedures can be readily reused and that user-defined tactics are more flexible. Yet, user-defined tactics and proof by reflection do not operate at the same level and embedding a powerful reflective tactic language would be a challenge by itself.

To reach our goal, we take the opposite approach and leverage the Coq extraction mechanism, thus allowing to run our SAT solver inside the Coq proof engine, i.e., at the level of tactics. There, the theory reasoning interface may be implemented by calling user-defined tactics. The theory prover thy_prover (see Section 2.6) takes a list of literals and attempts to produce a clause. Therefore, to interface with tactics, the followings tasks need to be performed: 1. Construct a goal from the literals provided by the SAT solver. 2. (Optionally) perform theory propagation 3. Run the tactic and obtain a proof-term. 4. Return a reduced clause. Within the proof engine, we maintain a mapping from literals to actual Coq terms. We interpret the list of literal as a clause to be discharged by the user-provided tactic. We obtain a goal G of the general form: G:=∀ i∈I (x i : p i ), j∈J q j . Actually, the p i and the q j do not depend on the x i . Yet, this dependent product notation is convenient to explain our minimisation procedure.

The fact that the conclusion is a disjunction j∈J q j may trigger, for some tactics, a costly case-analysis which would be more efficiently performed at the level of the SAT solver. For this purpose, we leverage the type-class mechanism to perform theory propagation at the level of individual propositions. For instance, if one of the q j is an equality over Z, say x=y, we directly return to the SAT solver the tautology clause x<y ∨ x=y ∨ y<x.

If the tactic fails, the unsuccessful goal G is a potential counter-example and is returned to the user for inspection. If the tactic proves the goal, the clause G holds and is therefore a conflict clause. A sound, but naive, approach is to return this clause containing all the input literals. Yet, to improve the efficiency of the SAT solver, it is desirable to reduce the clause and produce a minimal unsatisfiable core. In other words, we search for sets I ′ ⊆ I and J ′ ⊆ J such that G ′ :=∀ i∈I ′ (x i : p i ), j∈J ′ q j is still a tautology. In our context, if the tactic succeeds, it also produces a proof-term. Using a syntactic analysis, we track the subset of the x i that are used in the proof-term and therefore obtain a set I ′ ⊆ I containing the needed hypotheses. To minimise the set J, a finer grained analysis of the proof term may be possible. However, there is a sweet spot when the positive literals are classical propositions. In that case, the goal G is equivalent to G ′ G ′ :=∀ i∈I (x i : p i ), ∀ j∈J (y j : ¬p j ), False I T P 2 0 2 1 9:14

Itauto: An Extensible Intuitionistic SAT Solver

Using this formulation, the same syntactic analysis extracts both a subset I ′ ⊆ I of the negative literals and a subset J ′ ⊆ J of the positive literals. When the propositions are not classical, we perform some partial iterative proof-search and try to prove each of the q i , one at a time. Once the minimisation is done, we adjust the proof-term for the minimised conflict clause: this consists in recomputing the correct De Bruijn indexes to accommodate for the removed hypotheses.

If the extracted SAT solver succeeds, we have the guarantee that the goal is provable but the proof elements still need to be pieced together. The SAT solver returns the set of needed literals. We exploit this information to remove from the context the propositions that are irrelevant for the proof. Now, we enrich the context with all the conflict clauses that were generated during the SAT solver run, re-using the cached proof terms. At this stage, we have a goal that is a propositional tautology. It is solved by re-running the SAT solver, without theory reasoning, by a classic proof by reflection.

Using the extracted SAT solver has the advantage that the possible bugs are limited to the interface with user-provided tactic. Another possible design would be to rely on an external untrusted (intuitionistic) SAT solver. This would have some speed advantage for the generation of conflict clauses but would increase the code base. In our case, we reuse the same verified component both in the Coq proof engine and to perform proof by reflection.

Experiments

Before showing some larger scale experiments, we come back to the motivating examples (see Section 1.1) and explain how they are solved by our tactic.

Back to Motivating Examples

Consider again the goals in Example 1. For Ex1, the SAT solver has knowledge that x>=0 is a classical proposition and therefore performs a case-split over x>=0→ p. The first subcase is solved by theory reasoning (x=0 → ~x>= 0 → False holds); and the second by propositional reasoning (p → p). For Ex2, the SAT solver does not make progress. However, it asks the leaf tactic congruence whether a watched negative literal (i.e., a=c) may be deduced from the assigned literal (i.e., a=b and b=c). As a=b → b=c → a=c can be proved by congruence, the clause is asserted by theory reasoning. The proof follows by propositional reasoning.

For Example 2, the goal is solved by intuition congruence using two identical calls to the leaf tactic congruence. Because our SAT solver threads learnt clauses along the computation, the same goal is solved by itauto congruence by calling congruence only once.

Pigeon Hole

The Pigeon Hole Principle, stating that there is no way to fit n+1 pigeons in n holes, is a hard problem for resolution based SAT solvers. The algorithm presented here is no exception and the running time will be exponential in n. This is however a useful benchmark for assessing scalability. We have benchmarked our itauto tactic against the existing tauto and rtauto tactics using a timeout of 3600s and a memory limit of 15GB on a laptop (Intel Core i7 at 1.8GHz with 32GB of RAM). The results are shown in Fig. 1. For itauto, the running time of the tactic and the type-checking time (Qed time) are similar. As we perform a pure proof by reflection, this is not surprising. Though itauto scales slightly better, the running time are similar to rtauto which only performs proof by reflection to check certificates. tauto is the least scalable and the proof search reaches timeout for 5 pigeons. rtauto exhausts its memory quota when checking its certificate for 7 pigeons. itauto reaches the time limit of 3600s for 10 pigeons.

On existing developments

We have benchmarked itauto against the existing Coq tactics tauto and intuition for the Bedrock2 9 and CompCert 10 developments using Coq 8.14+alpha. We have replaced calls to tauto and intuition tac for tac ∈ {idtac, assumption, discriminate, congruence, lia, auto, eauto }. We have ruled out calls to intuition when they generate sub-goals. In terms of completeness, itauto is able to solve the vast majority of the goals. One representative case of failure is given in Example 7.

▶ Example 7.

The following goal is solved by intuition congruence.

Goal true = true ↔ (Z → (False ↔ False)).

Yet, itauto congruence fails because Z (i.e., the type of integers) has type Set and therefore the whole expression Z → (False ↔ False) is reified as an opaque atomic proposition. Our solution is to call itauto recursively i.e., itauto (itauto congruence) so that an hypothesis x:Z is explicitly introduced. The same approach works for goals with inner universal quantifiers.

For a few instances, we also strengthen the leaf tactic replacing e.g., idtac by reflexivity, and, discriminate by congruence. This is due to the fact that intuition implicitly calls reflexivity and that our handling of theory reasoning sometimes introduces negations which fool the discriminate tactic. After modification, Bedrock2 performs 1621 calls to itauto. For 40% of the goals, the running time differs by less than 1ms and itauto outperforms the historic tactics for 40% of the cases. Overall, itauto is faster and there is an slight speedup of 1.07. Yet, all the calls are quickly solved; the slowest goal is solved in 0.18s.

CompCert performs 924 calls to itauto. For 76% of the goals, the running time also differs by less than 1ms. itauto outperforms the historic tactics for 19% percent of the goals. Yet, when itauto is faster it can be by several orders of magnitudes: the 19% percent of goals are solved more than 20 times faster by itauto. For instance, the maximum running time of tauto is 5.26s to be compared to 0.81s for itauto. Overall, itauto performs better with a speedup of 2.8 for solving all the goals.

In summary, the results are rather positive though the advantage may be slim. It seems that itauto shows a decisive advantage for goals that are very slow with the existing tactics. As shown by the Pigeon Hole experiment, this would indicate a better scalability. It would not be surprising for itauto to be slower on simple goals where the overhead of setting up the proof by reflection cannot be amortised. itauto spends time in different proof tasks: SAT solver, theory reasoning and proof by reflection. We are confident that the SAT solver is scalable and reasonably fast. Yet, this is not always the bottleneck, and, the positive results reported here were only made possible by fine tuning other tasks e.g., the reification code.

Related Work

For propositional logic, Weber and Amjad [START_REF] Weber | Efficiently checking propositional refutations in HOL theorem provers[END_REF] for HOL theorem provers and Armand et al. [START_REF] Armand | Extending Coq with Imperative Features and Its Application to SAT Verification[END_REF] for Coq show how to efficiently validate resolution proofs that can be generated by modern SAT solvers using Conflict Driven Clause Learning (e.g. zChaff [START_REF] Moskewicz | Chaff: Engineering an Efficient SAT Solver[END_REF]). Satisfiability Modulo Theory (SMT) solvers (e.g., veriT [START_REF] Bouton | veriT: An Open, Trustable and Efficient SMT-Solver[END_REF], Z3 [START_REF] Mendonça De Moura | Z3: an efficient SMT solver[END_REF] , CVC4 [START_REF] Deters | A tour of CVC4: How it works, and how to use it[END_REF]) produce proof artefacts. Böhme and Weber [START_REF] Böhme | Fast LCF-Style Proof Reconstruction for Z3[END_REF] show how to efficiently perform proof reconstruction for HOL provers. Armand et al. [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF] and Besson et al. [START_REF] Besson | Modular SMT Proofs for Fast Reflexive Checking Inside Coq[END_REF] extract proof certificates from SMT proofs that are validated in Coq. Sledgehammer [START_REF] Christian Blanchette | Extending Sledgehammer with SMT Solvers[END_REF] interfaces Isabelle/HOL with a variety of provers; Metis [START_REF] Hurd | First-order proof tactics in higher-order logic theorem provers[END_REF][START_REF] Paulson | Source-Level Proof Reconstruction for Interactive Theorem Proving[END_REF] is in charge of performing proof reconstruction. We follow a different approach and verify a SAT solver interfaced with the tactics of Coq. What we loose in efficiency, we gain in flexibility because the user might use her own fine-tuned domain specific tactics. Claessen and Rosén [START_REF] Claessen | SAT Modulo Intuitionistic Implications[END_REF] build a prover for intuitionistic logic on top of a black-box SAT solver. Their implementation is more efficient than ours but is not integrated inside a proof-assistant. Lescuyer and Conchon [START_REF] Lescuyer | A Reflexive Formalization of a SAT Solver in Coq[END_REF]20] formalise a reflexive SAT solver for classical logic. Their implementation features a lazy definitional CNF that is not fully exploited because of the lack of hash-consing. Compared to ours, their SAT solver performs neither lazy unit propagation nor backjumping. Blanchette et al. [START_REF] Christian Blanchette | A verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality[END_REF] formalise a Conflict Driven Clause Learning (CDCL) SAT solver and derive a verified implementation. Using this framework, Fleury, Blanchette and Lamich [START_REF] Fleury | A verified SAT solver with watched literals using imperative HOL[END_REF] derive an imperative implementation using watched literals. Our implementation has less sophisticated features but is integrating as a reflective proof procedure and allows to perform theory reasoning.

Conclusion and Future Work

We have presented itauto a reflexive tactic for intuitionistic propositional logic which can be parametrised by user-provided tactics. The SAT solver is optimised to leverage classical reasoning thus limiting, when possible, costly intuitionistic reasoning. Our SAT solver has several features found in modern SAT solver. Yet, the implementation could be improved further. A first improvement would be to generate more sophisticated learnt clauses. This could be done by attaching to each clause, not only the needed literals, but also the performed unit propagations. Another improvement would be to use primitive persistent arrays (available since Coq 8.13) allowing to implement efficiently more imperative algorithms e.g., 2-watched literals.

Lemma

  Ex1:∀(p:Prop)(x:Z), x=0 → (x>=0 → p) → p. Lemma Ex2:∀(A:Type)(p:Prop)(a b c:A),a=b → b=c → (a=c → p) → p.

  l r) = if is_dec r then ((NEG r):: map POS l , HLFF) else (map POS l, r) intro_impl f = if is_dec f then ([NEG f] , HLFF) else ([], f)

  Annot (A: Type) := { elt := A ; deps := LitSet.t } Therefore, unit propagation operates on the following watch_map data-structure. Definition clause_set := ptrie (Annot watched_clause). Definition watch_map := ptrie (clause_set * clause_set).A watch_map m maps a propositional variable f i.e., a hash-consed formula, to two sets (n, s) of clauses where clauses in n are watched by ⌊f ⌋ → and clauses in p are watched by ⌊f ⌋. More precisely, we havec ∈ n iff c.watch1 = (⌊f ⌋ →) ∨ (c.watch2 = ⌊f ⌋ →) c ∈ p iff c.watch1 = ⌊f ⌋ ∨ c.watch2 = ⌊f ⌋Suppose that we perform unit propagation for the literal ⌊f ⌋ for a watched_map m such that m[f ] = (n, p). The clauses in p are redundant and can be dropped; the clauses in n need to be processed and reduced. The reduction takes as argument the set of literals that are currently assigned, a watched clause c and returns an annotated clause Annot clause where the type clause is given below Inductive clause:=|EMPTY |TRUE |UNIT (l:literal)|CLAUSE (wc:watched_clause)8 Head/tail lists give access to the first and last element of a list in O(1).

  reduce s d x [] = {| elt := UNIT x ; deps := d |} reduce s d x (y::l) = {| elt := TRUE ; deps := d |} when y ∈ s reduce s d x (y::l) = reduce s ((deps (s y)) ∪ d) l when ¬ y ∈ s reduce s d x (y::l) = let wc := {| watch1 := x ; watch2 := y ; unwatched := l |} in {| elt := CLAUSE wc ; deps := d |} when y / ∈ s

Fixpoint

  case_split cl st g := match cl with | [] => Some (false, LitSet.empty) | f::cl => match Prover (st ∪ f) g with | None => None | Some d => if f / ∈ d && st ⊢ d then Some (true,d) else match case_split cl st g with | None => None | Some(b, d') => if b then Some(b,d') else Some(false, d' ∪ (d \ {f})) end end end.

Fixpoint

  prover_arrows (l : list literal) (st: state) (g: HFormula) := match l with | [] => None | f :: l => match Prover st f with | Some _ => Prover (st ∪ f) g | None => prover_arrows l st g end end.

Fixpoint

  prover thy use_prover fuel st g := match n with | O => Fail OutOfFuel | S n => let ProverRec := prover thy use_prover n in (prover_unit n ; prover_case_split ProverRec ; prover_impl_arrows ProverRec ; prover_thy ProverRec thy use_prover) st g end.

  Running time of type-checking.

Figure 1

 1 Figure 1 Pigeon Hole for itauto, tauto and rtauto.

9

  https://github.com/mit-plv/bedrock2 10 https://github.com/AbsInt/CompCert

https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.congruence

https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.intuition

The propositional variable p is replaced by True or False depending on its polarity.

https://coq.inria.fr/refman/language/core/primitive.html#primitive-integers


Pierre Verger

Dimitri Scronias

Yves Fradier

Malika Meziani

Bruno Ventelou

Online study of health professionals about their vaccination attitudes and behavior in the COVID-19 era: addressing participation bias

Keywords: Health care professionals, online surveys, selection bias, attitudes, practices, covid-19, weighting, Heckman method

Online surveys of health professionals have become increasingly popular during the COVID-19 crisis because of their ease, speed of implementation, and low cost. This article leverages an online survey of general practitioners' (GPs') attitudes toward the soon-to-beavailable COVID-19 vaccines, implemented in October-November 2020 (before the COVID-19 vaccines were authorized in France), to study the evolu-tion of the distribution of their demographic and professional characteristics and opinions about these vaccines, as the survey fieldwork progressed, as reminders were sent out to encourage them to partici-pate. Focusing on the analysis of the potential determinants of COVID-19 vaccine acceptance, we also tested if factors related to survey participation biased the association estimates. Our results show that online surveys of health professionals may be subject to significant selection bias that can have a significant impact on estimates of the prevalence of some of these professionals' behavioral, opinion, or attitude variables. Our results also highlight the effectiveness of reminder strategies in reaching hard-to -reach professionals and reducing these biases. Finally, they indicate that weighting for nonparticipation remains indispensable and that methods exist for testing (and correcting) selection biases.

Introduction

Conducting surveys of health-care professionals' (HCPs) perceptions, attitudes, and practices is hard, and their participation rates are often low. In the era of COVID-19, use of online surveys to reach these professionals has increased [START_REF] Lin | Confidence and receptivity for COVID-19 vaccines: a rapid systematic review[END_REF] because these provide a convenient, inexpensive, and safe method for collecting information from large numbers of participants in a short time. The range of secure software solutions available for online questionnaire surveys has facilitated their development in recent years. Online surveys of professionals, however, as of the general population, present the risk of significant participation bias. [START_REF] Cho | Enhancing surveys of health care professionals: a meta-analysis of techniques to improve response[END_REF] Two types of participation bias can be distinguished by whether they are related to observed (measured) or unobserved (unmeasured) variables. In the first case, weighting strategies that take these observed variables (e.g., age and gender) into account make it possible to obtain samples representative for these variables. Weighting is not systematically applied however, as this requires sampling frames that contain accurate information for the entire population of interest about certain essential individual characteristics, and these do not always exist. For example, although HCPs' workload may be associated with their participation in surveys, [START_REF] Verger | Vaccine hesitancy among general practitioners and its determinants during controversies: a national cross-sectional survey in France[END_REF] this variable is rarely available. Bias can also arise if unobserved factors, such as their level of interest in public health, are linked to both survey participation and the dependent variables studied. This article leverages a survey of general practitioners' (GPs') attitudes toward the soon-to-be-available COVID-19 vaccines, implemented in October-November 2020 (before the COVID-19 vaccines were authorized in France), [START_REF] Verger | Attitudes of healthcare workers towards COVID-19 vaccination: a survey in France and French-speaking parts of Belgium and Canada[END_REF] to study the evolution of the distribution of their demographic and professional characteristics as the survey fieldwork progressed, as reminders were sent out to encourage them to participate, and simultaneously, of their opinions about these vaccines. Focusing on the analysis of the potential determinants of COVID-19 vaccine acceptance, we also tested if factors related to survey participation biased the association estimates.

Methods

Study design and population

We implemented an online cross-sectional survey within a representative national panel of 2,755 non-salaried GPs in France. The panel was set up in 2018, by random selection of GPs from an exhaustive database of health professionals (French national directory of health professionals). [START_REF] Verger | Attitudes of healthcare workers towards COVID-19 vaccination: a survey in France and French-speaking parts of Belgium and Canada[END_REF] To be included in the panel, GPs had to be in private practice and not practice complementary and alternative medicine exclusively.

Data collection

We collected the data with a sequential mixed-mode design: participants were invited to take part online; if they had not completed the survey after five e-mail or text (mobile phone numbers were available for 79% of panel members) reminders over 4 weeks, at different times of day and on different days of the week, they were contacted by telephone. Participants were informed in the e-mail sending them the link to the questionnaire that the collected data and the results would be anonymous. They were informed that the questionnaire was about 15 minutes long, with two parts: one on their opinions and practices regarding vaccination in general, and another on the COVID-19 epidemic. The ethics board of the Conseil national de l'information statistique (France, CNIS, avis n°114/H030) approved the study protocol and questionnaire.

Questionnaire

The questionnaire asked participants two questions about these future COVID-19 vaccines: 1) the GPs' willingness to be vaccinated themselves and 2) their willingness to recommend the vaccines to their patients. It used a five-point scale from "no, certainly not" and "no, probably not" to "yes, probably," and "yes, certainly," with a "don't know" option. Scores ranged from 0 to 3. Besides queries about their uptake of last year's seasonal influenza vaccine (Yes/No/Don't remember), other questions probed perceptions of the safety of these urgently developed new vaccines and trust in the health authorities to ensure that vaccines are safe. This last item was asked to assess the extent to which GPs perceive that the French health authorities are putting in place effective mechanisms to monitor the safety of vaccines. The degree of institutional trust is a key factor in vaccine hesitancy. [START_REF] Verger | Restoring confidence in vaccines in the COVID-19 era[END_REF] Finally, participants were asked about their perception of the medical severity of COVID-19 for the general population, on a scale from 0 (not severe) to 10 (extremely severe).

Workload

We created a categorical variable indicating GPs' workload, based on their number of consultations and patient visits in 2017. These data were obtained from the French National Health Insurance Fund.

Sample size

A sample size of about 1000 respondents was required to estimate the percentage of GPs willing to accept these vaccines with a 95% confidence interval and an error margin of ± 3%. [START_REF] Tillé | Sampling algorithms[END_REF]

Statistical analysis

To analyze the evolution of the sample's characteristics throughout the survey, we distinguished four periods by the reminders sent (Table 1) and compared the distribution of GPs' characteristics and opinions with Chi-2 tests on unweighted data by period. We also weighted the sample for age, gender, region, workload, and density of GPs in the GPs' practice area to compare weighted and unweighted percentages of these characteristics for the entire sample of respondents.

We applied a previously published method to construct a score of presumptive acceptance of future COVID-19 vaccines, [START_REF] Verger | Attitudes of healthcare workers towards COVID-19 vaccination: a survey in France and French-speaking parts of Belgium and Canada[END_REF] taking self-vaccination and recommendations to patients into account (alpha: 0.88, range [0-6]). Next, the score was transformed into a three-point variable named "COVID-19 vaccine acceptance": high acceptance (score >4), moderate acceptance (score = 4), hesitancy or reluctance (score <4, or answered "don't know" to at least one of the two items).

Finally, we focused on "Covid-19 vaccine acceptance" (polytomous dependent variable) to test whether potential differences between panel participants at inclusion and those participating in this survey might bias the results of a regression analysis studying factors associated with this dependent variable. We implemented a generalization of the Heckman selection model for polytomous outcomes that can test (and correct) for the presence of selection bias. It consists in a multinomial probit model with sample selection [START_REF] Greene | Econometric analysis. 8th[END_REF][START_REF] Heckman | Sample selection bias as a specification error[END_REF] (supplemental material S1). In these models, the first equation applied to the entire sample of panelists and analyzed factors (age, gender, region, workload, and GP density in the area of practice) potentially associated with both inclusion in the panel and participation in this survey (see supplemental material S2 for the specification of this equation). The other equation applied only to respondents to this survey (N = 1,209) and studied the factors associated with their COVID-19 vaccine acceptance. Such a model tests the correlation (rho) between the error terms of the two equations that may occur if any factors are associated with both survey participation and COVID-19 vaccine acceptance. A significant correlation means that estimates of the second equation are biased; the rho is then used to calculate unbiased estimates.

All analyses used two-sided p-values, defined statistical significance as p < .05, and were performed with Stata 14. The multinomial probit model was implemented using the cmp package. 9

Results

In all, 1,209/2,755 GPs (43.9%) participated. The evolution of the number of respondents throughout the survey according to reminders is shown in Figure S2 in the supplemental material. Over the four survey periods, the proportions of GPs who were male, aged 60+, and had a high workload all increased significantly (Table 2). The proportion practicing complementary and alternative medicine (CAM) also varied significantly, but not linearly. The proportion trusting the Ministry of Health increased significantly throughout the survey, while that perceiving the pandemic as severe decreased significantly (Table 3). Nonetheless, neither the acceptability of COVID-19 vaccines nor reports of personal vaccination against seasonal influenza during the previous winter varied significantly by survey phase. The perception of the safety of future vaccines developed as an emergency response to an epidemic showed non-linear variations at the limit of significance (p = .07).

Finally, in the Heckman model, the nonsignificant LR test of the correlation of the error terms of the two equations testing first survey participation and then vaccine acceptance determinants (p = .62, Table 4) indicated the absence of selection bias potentially due to panel participation and then attrition. The model showed that survey participation was lower among GPs who were older, worked in low GP-density areas or in southeastern France, had high workloads, or practiced CAM occasionally; participation was higher among women, however. Compared to GPs with high acceptance of COVID-19 vaccines, hesitancy was higher among women, doctors doubtful about the safety of rapidly developed vaccines, perceiving the epidemic's medical severity as low, distrustful of the health authorities, and those not vaccinated against influenza in the winter of 2019-20. The prevalence of moderate acceptance was lower among older GPs, those with a higher workload and who were vaccinated against seasonal influenza in 2019-20. It was, however, higher among GPs who occasionally practiced CAM, who thought the safety of vaccines developed during an emergency could not be considered guaranteed and who considered the medical severity of COVID-19 to be low.

Discussion

In this online survey of GPs, respondents differed significantly from nonrespondents for several characteristics (notably, age and workload) (Table 4). Among respondents, rapid responders also differed significantly from hard-to-reach GPs (who responded after multiple reminders) for gender, and again age and workload. Important selection processes are therefore at work in surveys of HCPs. The individual characteristics underlying these biases are likely to be associated with various behaviors, opinions, and attitudes toward patient care. For example, female GPs devote more time to prevention and screening activities than male GPs; 10 younger doctors are aware of and adhere to good practice guidelines more often than older 'hesitancy/reluctance'), there are two comparisons (multiple polytomous probit regression): 'moderate acceptance' is compared to 'high acceptance' (reference), and 'hesitancy/reluctance' is also compared to 'high acceptance'. Positive probit coefficient indicate a positive association with the dependent variable (e.g. female were more likely to participate in the study) whereas negative coefficients indicate a negative association (e.g. older GPs were less likely to participate in the study). The higher the absolute value of the probit coefficient, the greater the strength of the association. b Factors associated with participation to the study; these would have been used to correct the estimates of the next two columns, in the presence of selection bias; in the present analysis however, we did not find evidence for such bias. c Probit coefficient; d Confidence Interval; p-value LR test: 0.62 (comparison between models with and without sample selection; this non-significant result indicates there is no evidence for selection bias); rho_moderate = 0.49 (correlation between study participation and moderate acceptance); rho_hesitancy = -0.15 (correlation between study participation and hesitancy)

ones; [START_REF] Clerc | General practitioners and clinical practice guidelines: a reexamination[END_REF] and GPs with higher workloads tend to prescribe medication more often and spend less time with their patients than doctors with lower workloads. [START_REF] Silhol | How French general practitioners respond to declining medical density: a study on prescription practices, with an insight into opioids use[END_REF] Specifically concerning vaccination, our previous work showed that GPs younger than 50 y, female, or with the highest workloads tend to recommend the vaccines on the official schedule more frequently to patients than the others. [START_REF] Verger | Vaccine hesitancy among general practitioners and its determinants during controversies: a national cross-sectional survey in France[END_REF] In contrast, female HCPs (GPs and nurses) and those aged younger than 40 y expressed hesitation about upcoming COVID-19 vaccines more frequently. [START_REF] Verger | Attitudes of healthcare workers towards COVID-19 vaccination: a survey in France and French-speaking parts of Belgium and Canada[END_REF][START_REF] Gagneux-Brunon | Intention to get vaccinations against COVID-19 in French healthcare workers during the first pandemic wave: a cross sectional survey[END_REF][START_REF] Wang | Intention of nurses to accept coronavirus disease 2019 vaccination and change of intention to accept seasonal influenza vaccination during the coronavirus disease 2019 pandemic: a cross-sectional survey[END_REF] The prevalence of vaccine hesitancy among GPs also varies considerably between regions in the same country, independently of demographic and professional characteristics. [START_REF] Collange | Unexplained variations in general practitioners' perceptions and practices regarding vaccination in France[END_REF] During the 2009 A/H1N1 pandemic, GPs with the highest workloads and those in group practices were willing to accept the A/H1N1 pandemic vaccines more often than other GPs, while we observed no differences by age or gender. [START_REF] Schwarzinger | Positive attitudes of French general practitioners towards A/H1N1 influenza-pandemic vaccination: a missed opportunity to increase vaccination uptakes in the general public?[END_REF] These results among French GPs show that the direction of the observed links between their characteristics and their vaccination attitudes and behaviors may vary by vaccine type and event.

Behaviors and attitudes of CAM doctors toward patient management differ from those of other doctors: concerning vaccination, they are much more frequently hesitant and much less likely to recommend vaccines on the official calendar than non-CAM GPs. [START_REF] Verger | Vaccine hesitancy among general practitioners and its determinants during controversies: a national cross-sectional survey in France[END_REF][START_REF] Verger | Prevalence and correlates of vaccine hesitancy among general practitioners: a cross-sectional telephone survey in France, April to July 2014[END_REF] The significant variations in the percentage of CAM GPs between the survey phases did not follow a linear trend, perhaps due to the relatively small fraction of the sample they accounted for (N = 190).

The variation over the course of the survey in GPs' perceptions of the pandemic risks and confidence in the health authorities is another important result: as potential determinants of various attitudes and behaviors of GPs, [START_REF] Verger | Perceptions et opinions des médecins généralistes lors du déconfinement[END_REF] these variables are key indicators to monitor throughout a health crisis -such as COVID-19 -to follow GPs' adherence to the recommended management. The variation in the perception of the future vaccines' safety over the course of the survey (Table 3) was near the border of significance. It too is a crucial indicator to be monitored and may be sensitive to events, such as scientific publications about the efficacy and safety of new vaccines, marketing authorizations, and recommendations by professional societies.

An important methodological takeaway is the importance in online surveys of HCPs of applying a reminder strategy to improve the representativeness of survey participants. [START_REF] Cho | Enhancing surveys of health care professionals: a meta-analysis of techniques to improve response[END_REF] Our experience shows that it is appropriate and feasible to go up to 5 reminders, without unduly burdening the survey costs. Recourse to telephone reminders and interviews at the end of a survey could be an optimal solution in terms of participation as it makes it possible to contact and include hard-to-reach GPs. But this must be balanced against cost and feasibility considerations. In addition, the potential differential reporting bias between collection by an interviewer and direct collection without an intermediary in an online questionnaire should also be taken into account. [START_REF] Legleye | Agréger les échantillons d'une enquête multimode en limitant l'effet de mesure : une proposition d'imputation raisonnable et pragmatique[END_REF][START_REF] Vannieuwenhuyze | Method for evaluating mode effects in mixed-mode surveys[END_REF] In addition to a reminder strategy, our results also indicate the need to weight the data, especially when participation rates are relatively modest (here, 43.9%). Comparison of the unweighted and weighted results of our study showed nonnegligible differences in age, gender, and volume of activity.

Nonetheless, it is reassuring that the differences for the variables of interest studied here were more modest (4 to 5 percentage points for acceptance of COVID-19 vaccines, Table 3). As surveys among HCPs are likely to be repeated in a pandemic to monitor various aspects of their attitudes and behaviors as we did in France in the frame of our panel, [START_REF] Galimard | Heckman imputation models for binary or continuous MNAR outcomes and MAR predictors[END_REF] weighting remains essential and ideally should include workload, provided that this information is available in both national databases and surveys.

Our results are also reassuring regarding potential selection effects due to participation in a survey since Heckman's method did not suggest that they played a role in the analysis of factors associated with the acceptance of COVID-19 vaccines.

The results of this study must be interpreted with caution however. First, they relate to non-salaried GPs while the demographic and professional characteristics associated with being hard-to-reach in a survey may vary according to the type of health profession, practice setting (community, hospital), and country. However, workload is a characteristic that can reasonably be assumed to be common to all these professions. Furthermore, the impact of selection bias is likely to vary according to the dependent variable.

In any case, this type of bias should be systematically tested: to the extent possible, collecting the necessary data should be planned before survey implementation. Moreover, recent methodological developments make it possible to take unobserved factors into account in data weighting. 22

  1 to 2 reminders (09 to 18/10/2020) 411 34.00 3 to 5 reminders (19 to 25/10/2020) 184 15.22 Telephone interviews b (>25/10/2020by sending an e-mail or a text message to the panel members who had not yet responded b GPs who had not completed the questionnaire online were contacted by trained professional interviewers (Kantar Public) to invite them to complete the questionnaire with them on the phone. During this phase, 74 GPs preferred completing the questionnaire online: these GPs have been put in the last category because, along with those who were interviewed by telephone, they were the last to participate.

Table 1 .

 1 Number of respondents to the survey per phase, French general practitioners, unweighted data, October to November 2020.

	Phase	N	%
	No reminder a (<09/10/2020)	256	21.17

Table 2 .

 2 Trends in respondents' demographic and professional characteristics throughout the survey, French general practitioners, unweighted data, October to November 2020.

			Survey phases of the survey
					Telephone reminder
		No reminder N = 256	1-2 reminders N = 411	3-5 reminders N = 184	&/or interview N = 358	p-value a	Total N = 1,209
		Col. uW%	Col. uW%	Col. uW%	Col. uW%		uW% b	W% c
	Gender
	Male	49.22	43.07	52.72	64.80	< 0.001	52.27	60.87
	Female	50.78	56.93	47.28	35.20		47.73	39.13
	Age (years)
	<50	51.95	52.80	40.22	36.31	< 0.001	45.82	31.18
	50-59	28.13	22.38	26.63	26.82		25.56	32.24
	60+	19.92	24.82	33.15	36.87		28.62	36.57
	Region
	National	63.28	58.64	66.30	62.29	0.20	61.87	85.68
	Southeast	17.58	18.73	14.13	21.23		18.53	8.66
	West	19.14	22.63	19.57	16.48		19.60	5.66
	Workload
	Min-Q1	30.47	33.09	25.00	23.74	0.003	28.54	23.33
	Q1-Q3	55.47	52.31	54.35	52.23		53.27	50.79
	Q3-Max	14.06	14.60	20.65	24.02		18.20	25.88
	GPs density of practice area (deciles)
	Decile 1	10.94	12.90	13.04	16.76	0.19	13.65	6.55
	Deciles 2 to 10	89.06	87.10	86.96	83.24		86.35	93.45
	Occasional practice of complementary and alternative medicine (CAM)
	Yes	10.16	15.57	17.93	11.73	0.048	13.65	15.75
	No/Don't know	89.84	84.43	82.07	88.27		86.35	84.25

a p-value: Chi-squared test b uW: unweighted c W: weighted

Table 3 .

 3 Trends of respondents' opinions and attitudes throughout the survey, French general practitioners, unweighted data, October to November 2020.

				Phases of the survey
		No reminder N = 256	1-2 reminders N = 411	3-5 reminders N = 184	Telephone reminder &/or interview N = 358	p-value a	Total N = 1,209
		Col. %	Col. %	Col. %	Col. %		uW% b	W% c
	Covid-19 vaccine acceptance
	High acceptance	47.27	45.26	42.93	48.32	0.17	46.24	50.59
	Moderate acceptance	23.83	27.01	27.72	30.73		27.54	24.39
	Hesitancy or reluctance	28.91	27.74	29.35	20.95		26.22	25.02
	I trust the ministry of health to ensure that vaccines are safe Disagree/Don't know d 31.64 28.22	20.65	18.16	< 0.001	24.81	24.10
	Agree	68.36	71.78	79.35	81.84		75.19	75.90
	Were you vaccinated against seasonal influenza for the winter 2019-2020 season? No/Don't know d 11.72 11.19 11.96	14.80	0.46	12.49	14.70
	Yes	88.28	88.81	88.04	85.20		87.51	85.30
	The

safety of a vaccine developed in an emergency, during an epidemic, cannot be considered guaranteed

	Disagree Agree/Don't know d	44.53 55.47	38.44 61.56	37.50 62.50	46.37 53.63	0.07	41.94 58.06	42.45 57.55
	In

your opinion, for the population as a whole, how serious is COVID-19 on a scale of 0 to 10?

	Moderate/High/Don't know d [5-10]	67.19	69.34	76.09	79.61	0.001	72.95	72.54
	Low [0-4]	32.81	30.66	23.91	20.39		27.05	27.46

a p-value: Chi-squared test b uW: unweighted c W: weighted d Due to their small sizes, "don't know" categories were merged with others.

Table 4 .

 4 Factors associated with Covid-19 vaccines acceptance among French GPs, polytomous probit regressions with sample selection (on all GPs eligible for the panel, N = 11,146), unweighted data, October to November 2020.

				Covid-19 vaccine acceptance (ref. High a )
	Participation in the study b (ref. No)		Moderate	Hesitancy/reluctance
	N = 11,146		N = 1,209	N = 1,209
	Coef c	[CI 95%] d	Coef	[CI 95%]	Coef	[CI 95%]

risks of new vaccines in emergencies and of Covid-19

	The safety of a vaccine developed in an emergency, during an epidemic, cannot
	be considered guaranteed (ref. Disagree)
	Agree	0.97*** [0.67,1.28]	1.93*** [1.54,2.31]
	Don't know	0.56**	[0.21,0.91]	1.31*** [0.87,1.76]
	Perceived risks of Covid 19
	In your opinion, for the population as a whole, how serious is COVID-19 on a scale
	of 0 to 10?
	Low [0-4]	0.26*	[0.03,0.50]	0.47*** [0.20,0.74]
	Trust in science and in the ministry of health
	I trust the ministry of health to ensure that vaccines are safe (ref. Disagree)
	Agree	-0.31	[-0.64,0.01] -0.86*** [-1.22,-0.50]
	Don't know/no response	-0.11	[-0.61,0.38]	0.10	[-0.40,0.61]
	Personal vaccination
	Were you vaccinated against seasonal influenza for the winter 2019-2020
	season? (ref. No/non-response)
	Yes	-0.43*	[-0.79,-0.07] -0.87*** [-1.26,-0.48]
	P-values: *: <0.05; **: <0.01; ***: <0.001;

a Because the dependent variable (i.e. acceptance) has three categories ((i) 'high acceptance', (ii) 'moderate acceptance' and (iii)

Acknowledgments

We thank all the participants of this survey, Jo Ann Cahn for supervising our English, and Maxime Bergeat for his invaluable advice.

Disclosure of potential conflicts of interest

None to declare.

Funding

This study was supported by grants from the Direction de la Recherche, des Etudes, de l'Evaluation et des Statistiques (DREES)/Ministère des solidarités et de la santé (grant 2102173353) and from the Agence Nationale de la Recherche (ANR) in the frame of the call for projects 2020 "Recherche-Action Covid-19". [2102173353]