Boolean satisfiability problem solving using restricted boltzmann machines

A system comprising one or more computers and one or more storage devices storing instructions that when executed by the one or more computers cause the one or more computers to perform operations comprising:

• receiving a request to determine whether an input Boolean formula is satisfiable according to a set of satisfiability criteria, wherein the input Boolean formula is a conjunction of a plurality of clauses, wherein each clause is a disjunction of one or more literals;
• processing the input Boolean formula using a formula model that is configured to receive, as input, the input Boolean formula, and to generate, as output, a satisfiability probability distribution over assignments of values to the literals in the clauses of the input Boolean formula;
• determining whether the input Boolean formula is satisfiable according to the set of satisfiability criteria, comprising, at each of one or more sampling iterations:
• sampling, using the satisfiability probability distribution, an assignment of values to the literals in the clauses of the input Boolean formula, and
• determining whether the assignment of values satisfies the set of satisfiability criteria;
• and
• in response to determining that the input Boolean formula is satisfiable according to the satisfiability problem, sending, in response to the request, an indication that the input Boolean formula is satisfiable.

One or more non-transitory computer-readable storage media storing instructions that when executed by one or more computers cause the one or more computers to perform operations comprising:

• receiving a request to determine whether an input Boolean formula is satisfiable according to a set of satisfiability criteria, wherein the input Boolean formula is a conjunction of a plurality of clauses, wherein each clause is a disjunction of one or more literals;
• processing the input Boolean formula using a formula model that is configured to receive, as input, the input Boolean formula, and to generate, as output, a satisfiability probability distribution over assignments of values to the literals in the clauses of the input Boolean formula;
• determining whether the input Boolean formula is satisfiable according to the set of satisfiability criteria, comprising, at each of one or more sampling iterations:
• sampling, using the satisfiability probability distribution, an assignment of values to the literals in the clauses of the input Boolean formula, and
• determining whether the assignment of values satisfies the set of satisfiability criteria;
• and
• in response to determining that the input Boolean formula is satisfiable according to the satisfiability problem, sending, in response to the request, an indication that the input Boolean formula is satisfiable.