SAT Solver

A solver for the boolean satisfiability problem (with C-style syntax)

// SAT expressions for
// https://aprogrammerlife.com/top-rated/will-you-crack-the-code-143

// auxiliaries to express that a digit occurs somewhere
q0 == x0 || y0 || z0 ;
q1 == x1 || y1 || z1 ;
q2 == x2 || y2 || z2 ;
q3 == x3 || y3 || z3 ;
q4 == x4 || y4 || z4 ;
q6 == x6 || y6 || z6 ;
q7 == x7 || y7 || z7 ;
q8 == x8 || y8 || z8 ;

// every cell gets a number
x0 || x1 || x2 || x3 || x4 || x6 || x7 || x8 ;
y0 || y1 || y2 || y3 || y4 || y6 || y7 || y8 ;
z0 || z1 || z2 || z3 || z4 || z6 || z7 || z8 ;

// no cell gets two numbers
!x0 || !x1; !x0 || !x2; !x0 || !x3; !x0 || !x4; !x0 || !x6; !x0 || !x7; !x0 || !x8;
            !x1 || !x2; !x1 || !x3; !x1 || !x4; !x1 || !x6; !x1 || !x7; !x1 || !x8;
                        !x2 || !x3; !x2 || !x4; !x2 || !x6; !x2 || !x7; !x2 || !x8;
                                    !x3 || !x4; !x3 || !x6; !x3 || !x7; !x3 || !x8;
                                                !x4 || !x6; !x4 || !x7; !x4 || !x8;
                                                            !x6 || !x7; !x6 || !x8;
                                                                        !x7 || !x8;
!y0 || !y1; !y0 || !y2; !y0 || !y3; !y0 || !y4; !y0 || !y6; !y0 || !y7; !y0 || !y8;
            !y1 || !y2; !y1 || !y3; !y1 || !y4; !y1 || !y6; !y1 || !y7; !y1 || !y8;
                        !y2 || !y3; !y2 || !y4; !y2 || !y6; !y2 || !y7; !y2 || !y8;
                                    !y3 || !y4; !y3 || !y6; !y3 || !y7; !y3 || !y8;
                                                !y4 || !y6; !y4 || !y7; !y4 || !y8;
                                                            !y6 || !y7; !y6 || !y8;
                                                                        !y7 || !y8;
!z0 || !z1; !z0 || !z2; !z0 || !z3; !z0 || !z4; !z0 || !z6; !z0 || !z7; !z0 || !z8;
            !z1 || !z2; !z1 || !z3; !z1 || !z4; !z1 || !z6; !z1 || !z7; !z1 || !z8;
                        !z2 || !z3; !z2 || !z4; !z2 || !z6; !z2 || !z7; !z2 || !z8;
                                    !z3 || !z4; !z3 || !z6; !z3 || !z7; !z3 || !z8;
                                                !z4 || !z6; !z4 || !z7; !z4 || !z8;
                                                            !z6 || !z7; !z6 || !z8;
                                                                        !z7 || !z8;

// no number is in two cells
!x0 || !y0; !x0 || !z0; !y0 || !z0;
!x1 || !y1; !x1 || !z1; !y1 || !z1;
!x2 || !y2; !x2 || !z2; !y2 || !z2;
!x3 || !y3; !x3 || !z3; !y3 || !z3;
!x4 || !y4; !x4 || !z4; !y4 || !z4;
!x6 || !y6; !x6 || !z6; !y6 || !z6;
!x7 || !y7; !x7 || !z7; !y7 || !z7;
!x8 || !y8; !x8 || !z8; !y8 || !z8;

// one of 682 is correct and well placed
(q6 && !q8 && !q2) || (!q6 && q8 && !q2) || (!q6 && !q8 && q2);
x6 == !q8 && !q2 ;
y8 == !q6 && !q2 ;
z2 == !q6 && !q8 ;

// one of 614 is correct but wrong place
(q6 && !q1 && !q4) || (!q6 && q1 && !q4) || (!q6 && !q1 && q4);
y6 || z6 == !q1 && !q4 ;
x1 || z1 == !q6 && !q4 ;
x4 || y4 == !q6 && !q1 ;

// two of 206 are correct but wrong place
(q2 && q0 && !q6) || (q2 && !q0 && q6) || (!q2 && q0 && q6);
!q2  ==  (x0 || z0) && (x6 || y6) ;
!q0  ==  (y2 || z2) && (x6 || y6) ;
!q6  ==  (y2 || z2) && (x0 || z0) ;

// nothing of 738 is correct
!q7 ;
!q3 ;
!q8 ;

// one of 870 is correct but wrong place
(q8 && !q7 && !q0) || (!q8 && q7 && !q0) || (!q8 && !q7 && q0);
y8 || z8 == !q7 && !q0 ;
x7 || z7 == !q8 && !q0 ;
x0 || y0 == !q8 && !q7 ;

// exclude solutions to see if other solutions are possible
// !x0 || !y4 || !z2;