timbeurskens / gobdd

An ROBDD & CDCL based SAT solver

Hi there 👋

I'm Tim, an embedded software engineer from the Netherlands.

gobdd's Issues

Function type arithmetic

Describe the numeric arithmetic operations in terms of function types.

CDCL optimization

Find failing clauses before traversing all variables.

Domain specific language for describing SAT problems

Implement a DSL for SAT problems.

Function types

Support the ability to write relations as function applications:
A function can be described by means of a look-up table, such that the output of a function only depends on its inputs: f(a) = b.
This function type can be used to describe more complex operations, such as addition, multiplication, or prime factorization.