# CryptoMiniSat

This is a user interface, in Julia, to the CryptoMiniSat SAT solver.

It exposes all the functions of the C interface, in the same syntax (cmsat_new, etc.), and provides higher-level interfaces:

- the same functions as in the C interface, without
`cmsat_`

, accept 1-based variables of any integer type (rather than the 0-based UInt32) - a high-level
`solve(clauses; ...)`

function that accepts a vector of clauses, each a vector of terms represented as integers (negative for negated terms) for one-go solving, as well as an iterator`itersolve(clauses; ...)`

- a higher-level
`solve(clauses; ...)`

in which the terms of the clauses are`Lit(x)`

,`NotLit(x)`

or generally`Lit(x,negated::Bool)`

for usual clauses, and`x`

may be of any type; or the terms are of the form`XorLit(x)`

and`XNorLit(x)`

for XOR-clauses, in which the number of non-satisfied terms should have the same parity as the number of XNorLit terms.

julia> using CryptoMiniSat
julia> # simple clauses
julia> cnf = [[1, -5, 4], [-1, 5, 3, 4], [-3, -4]];
julia> solve(cnf)
5-element Array{Int64,1}:
-1
-2
-3
-4
-5
julia> # coffee with cream, tea with milk
julia> cnf = [[XorLit(:coffee),XorLit(:tea)],[NotLit(:coffee),Lit(:cream)],[NotLit(:tea),Lit(:milk)]];
julia> collect(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)