Lingeling.jl

Julia interface for the SAT solver Lingeling (Website, Repo) created by Armin Biere.

---

As Lingeling's API is similar to that of the SAT-Solver PicoSAT, some parts of Lingeling.jl are based on the Julia bindings in PicoSAT.jl.

✨ Features

Lingeling.jl includes some but not all functions of the Lingeling SAT-Solver:

• Constructing and destructing the solver
• Getting and setting solver options
• Adding, freezing, and melting literals
• Checking whether literals are usable/reusable
• Solving and dereferencing

Have a look at the documentation.

Tip

Some additional information may also be found in the Lingeling header file, as well as in the PicoSAT header file.

🔧 Installation

Lingeling.jl can be installed using

]add Lingeling

or

using Pkg
Pkg.add("Lingeling")

Lingeling.jl does currently not support Windows.

💡 Usage Example

Lingeling.jl/example/short_example.jl

Lines 1 to 29 in 9f7aa36

	using Lingeling
	# Initialize the Lingeling SAT-Solver
	solver = lgl_init()
	# Add some literals and finish the clause (by adding a `0` literal)
	# (1 OR 2)
	lgl_add(solver, 1)
	lgl_add(solver, 2)
	lgl_add(solver, 0)
	# Add another clause
	# (1 OR !2)
	lgl_add(solver, 1)
	lgl_add(solver, -2)
	lgl_add(solver, 0)
	# Solve
	result_code = lgl_sat(solver)
	# Check whether the formula is satisfiable
	println("Satisfiable: ", result_code == Lingeling.SATISFIABLE)
	# Get the satisfying literal assignments
	println("Literal 1: ", lgl_deref(solver, 1))
	println("Literal 2: ", lgl_deref(solver, 2))
	# Destruct the SAT-Solver
	lgl_release(solver)

❗ Any Problems?

If you encounter any issues with this package, please consider creating an issue or fixing the problem by submitting a pull request.

💼 LICENSE

Lingeling.jl is provided under an MIT license, same as the Lingeling SAT-Solver (Lingeling license file).