Decision and factoring algorithms

SmtSolver: lazy DPLL(T) for integer difference logic. Atom k is the constraint x - y <= c; the Boolean skeleton is solved by Dpll, asserted atoms (and the integer negations y - x <= -c - 1 of those set false) become weighted edges, and Bellman-Ford returns either potentials (a model) or a negative cycle whose negation is learned as a clause. ShorFactoring: Shor's algorithm with the order-finding measurement drawn (Philox) from its exact output distribution, then continued fractions. Identical to the Python arm morie.fn.compalgo.

Usage

SmtSolver(formula, max_iter = 10000L)

ShorFactoring(N, seed = 1, max_attempts = 20L)

Arguments

formula

List with atoms (list of list(x, y, c)) and clauses (list of signed integer vectors, DIMACS style; indices above the number of atoms are Boolean variables).

max_iter

Maximum SAT-theory rounds.

N

Composite integer below 1024.

seed

Philox seed.

max_attempts

Maximum bases tried.

Value

List. SmtSolver: satisfiable, model, solution, theory_conflicts, learned. ShorFactoring: factors, order, base, Q, attempts, route.

References

Nieuwenhuis, R., Oliveras, A. and Tinelli, C. (2006). Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann- Loveland procedure to DPLL(T). Journal of the ACM 53, 937-977.

Shor, P. W. (1997). Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM Journal on Computing 26, 1484-1509.

Nielsen, M. A. and Chuang, I. L. (2010). Quantum Computation and Quantum Information. Cambridge University Press.

Examples

f <- list(atoms = list(list("x", "y", -1), list("y", "z", -1),
                       list("z", "x", -1), list("z", "x", 5)),
          clauses = list(1, 2, c(3, 4)))
SmtSolver(f)$solution
#> $x
#> [1] -2
#> 
#> $y
#> [1] -1
#> 
#> $z
#> [1] 0
#> 
ShorFactoring(15, seed = 2)$factors
#> [1] 3 5