CMS(variables = 0; num_threads = Sys.CPU_THREADS)

creates a new CryptoMiniSat problem, with optional number of variables and threas.

Lit(x,inverted::Bool = false) Creates a literal x

NotLit(x) Creates a negated literal x; this is equivalent to Lit(x,true)

XNorLit(x) Creates a negated literal x, to be used in an XOR clause

XorLit(x) Creates a literal x, to be used in an XOR clause

add_clause(p::CMS, clause::Vector{Union{CMSLit,Integer}})::Bool

Add a clause to the system, namely the disjunction of the entries in clause. Direct terms are integers are numbered from 1, inverted terms are negative numbered from -1. They may also be specified as CMSLit(variable,invert).

add_clauses(p::CMS, clauses::Vector)

Adds all clauses to p.

add_xor_clause(p::CMS, clause::Vector{Union{CMSLit,Int}}, rhs::Bool)::Bool

Adds an XOR clause to p. This is a clause of the form x_1 ⊻ x_2 ⊻ ... ⊻ x_n = rhs.

add_xor_clauses(p::CMS, clauses::Vector)

Adds all XOR clauses to p.

get_conflict(p::CMS)::Vector{CMSLit}

returns the conflicting variables in the current solution to p. This assumes that solve(p) was called and returned false

get_model(p::CMS)::Vector{Bool}

returns the variables in the current solution to p. This assumes that solve(p) was called and returned true.

itersolve(clauses; verbose::Integer=0, num_threads::Integer=Sys.CPU_THREADS)

• verbose - verbosity
• num_threads - number of CPU threads to use

The first argument is a vector of clauses. Each clause is a vector of literals of, each encapsulated in Lit(T), NotLit(T), XorLit(T) or XNorLit(T) for some type T. Each clause containing XorLit and XNotLit terms is an XOR clause, and the number of satisfied clauses must have the same parity as the number of NotLit and XNorLit for the clause to be satified. Clauses containing Lit and NotLit terms are usual disjunctive clauses.

Returns an iterable object over all solutions.

julia> import CryptoMiniSat
julia> # coffee with cream, tea with milk
julia> cnf = [[XorLit(:coffee),XorLit(:tea)],[NotLit(:coffee),Lit(:cream)],[NotLit(:tea),Lit(:milk)]];
julia> collect(CryptoMiniSat.itersolve(cnf))
4-element Vector{Any}:
 Dict{Symbol, Bool}(:cream => 0, :milk => 1, :tea => 1, :coffee => 0)
 Dict{Symbol, Bool}(:cream => 1, :milk => 1, :tea => 1, :coffee => 0)
 Dict{Symbol, Bool}(:cream => 1, :milk => 1, :tea => 0, :coffee => 1)
 Dict{Symbol, Bool}(:cream => 1, :milk => 0, :tea => 0, :coffee => 1)

itersolve(clauses; vars::Integer=-1, verbose::Integer=0, proplimit::Integer=0, num_threads::Integer=Sys.CPU_THREADS)

• vars - the number of variables
• verbose - verbosity
• proplimit - ignored
• num_threads - number of CPU threads to use

Returns an iterable object over all solutions.

julia> import CryptoMiniSat
julia> cnf = [[1, -5, 4], [-1, 5, 3, 4], [-3, -4]];
julia> collect(CryptoMiniSat.itersolve(cnf))
18-element Array{Any,1}:
 [-1, -2, -3, -4, -5]
 [-1, 2, -3, -4, -5]
 [-1, 2, 3, -4, -5]
 [1, 2, 3, -4, 5]
 [-1, -2, -3, 4, -5]
 [1, -2, 3, -4, 5]
 [-1, -2, -3, 4, 5]
 [-1, 2, -3, 4, -5]
 [1, -2, -3, 4, 5]
 [1, 2, -3, 4, 5]
 [1, 2, -3, 4, -5]
 [-1, 2, -3, 4, 5]
 [1, -2, -3, 4, -5]
 [1, -2, 3, -4, -5]
 [-1, -2, 3, -4, -5]
 [1, 2, -3, -4, 5]
 [1, -2, -3, -4, 5]
 [1, 2, 3, -4, -5]

new_vars(p::CMS, n::Int)

Add n new variables to the system p

nvars(p::CMS)::Int

Return the number of variables in the system p

solve(p::CMS, assumptions=[])

returns whether p is solvable; possibly returns :undefined.

solve(clauses; verbose::Integer=0, num_threads::Int = Sys.CPU_THREADS)

• verbose - verbosity
• num_threads - number of CPU threads to use

Returns a solution if the problem is satisfiable. Satisfiable solutions are represented as a dictionary.

The first argument is a vector of clauses. Each clause is a vector of literals of, each encapsulated in Lit(T), NotLit(T), XorLit(T) or XNorLit(T) for some type T. Each clause containing XorLit and XNotLit terms is an XOR clause, and the number of satisfied clauses must have the same parity as the number of NotLit and XNorLit for the clause to be satified. Clauses containing Lit and NotLit terms are usual disjunctive clauses.

If the problem is not satisfiable the method returns an :unsatisfiable symbol.

julia> import CryptoMiniSat
julia> # coffee with cream, tea with milk
julia> cnf = [[XorLit(:coffee),XorLit(:tea)],[NotLit(:coffee),Lit(:cream)],[NotLit(:tea),Lit(:milk)]];
julia> CryptoMiniSat.solve(cnf)
Dict{Symbol, Bool} with 3 entries:
  :cream  => 0
  :milk   => 1
  :tea    => 1
  :coffee => 0

solve(clauses; vars::Integer=-1, verbose::Integer=0, proplimit::Integer=0, num_threads::Int = Sys.CPU_THREADS)

• vars - the number of variables (will be inferred if not specified)
• verbose - verbosity
• proplimit - ignored
• num_threads - number of CPU threads to use

Returns a solution if the problem is satisfiable. Satisfiable solutions are represented as a vector of signed integers. If the problem is not satisfiable the method returns an :unsatisfiable symbol.

julia> import CryptoMiniSat
julia> cnf = [[1, -5, 4], [-1, 5, 3, 4], [-3, -4]];
julia> CryptoMiniSat.solve(cnf)
5-element Array{Int64,1}:
 -1
 -2
 -3
 -4
 -5