According to a conjecture:
Conjecture (Fan & Raspaud, 1994) Every bridgeless cubic graph contains three perfect matchings with no edge in common.
Equivalent statement here
Given a bridgeless cubic graph $G$, can one find in polynomial or subexponential time three perfect matchings with no edge in common or answer no solution?
I encoded the problem in SAT.
The encoding of PM to SAT boils down to ONE-IN-K SAT with exactly two occurrences of a variable and the inverse encoding is possible too (there are papers on this).
To encode to SAT I work with three copies of $G$: $A,B,C$.
For each edge $e \in E(G)$ introduce three boolean variables $A_e,B_e,C_e$ and encode perfect matchings in $A,B,C$.
For empty intersection, for all edges $e \in E(G)$ add the clauses:
$$ \lnot A_e \lor \lnot B_e \lor \lnot C_e \qquad (1) $$
Experimentally good SAT solvers solve this encoding fast.
Is there some gadget that encodes the constraints (1) as matching problem, so the full solution of (1) and PMs in $A,B,C$ is a PM or maximum weighted matching?
I suspect such gadget doesn't exist.