Construct System of Equations

A system can be represented in the form of AND, OR, NOT and XOR gates/equations. The total number of equations of my system is around 650000 with 15000 unknown variables. Theoretically, if the number of equations is greater than the unknown variables, the system of equations become solvable. Practically, is it possible to construct and solve a system of equations of 650000 with 15000 unknown variables with some equation system solver?

• "if the number of equations is greater than the unknown variables, the system of equations become solvable" - this only applies to systems of linear equations (and even then, the system may be inconsistent). But logical operators are not linear. – gandalf61 Apr 24 '18 at 11:08
• You could write your system as a circuit, a netlist of interconnected logical gates. Then use bc2cnf to translate the circuit description into Conjunctive Normal Form (CNF) and feed this into a SAT solver like cryptominisat, Z3 or Clasp. If you are lucky, the SAT solver will find a solution. – Axel Kemper Jan 28 at 22:16