kdrag.solvers.sat

Classes

DPLLSolver(trail, _model, clauses)	A simple DPLL SAT solver implementation.
GroundClause(pos, neg)

class kdrag.solvers.sat.DPLLSolver(trail: list[list[Var]] = <factory>, _model: list[bool | None] = <factory>, clauses: list[Clause] = <factory>)

Bases: object

A simple DPLL SAT solver implementation. https://www.philipzucker.com/smt_sat_solver2/

>>> s = DPLLSolver()
>>> x,y = s.makevar(), s.makevar()
>>> s.clauses.append([x])
>>> s.check()
sat
>>> s.model()
{1: True}
>>> s.clauses.append([-x])
>>> s.check()
unsat

Parameters:

• trail (list[list[Var]])

• _model (list[bool | None])

• clauses (list[Clause])

backtrack()

Backtrack to previous decision level. Returns True if no more levels to backtrack to.

check()

DPLL loop. return True for sat, False for unsat

clauses: list[Clause]

decide()

Pick first unassigned variable and assign it True. Make new decision level in trail

eval_lit(lit: Lit) → bool | None

Find value of lit in current _model

Parameters:

lit (Lit)

Return type:

bool | None

is_conflict() → bool

Return type:

bool

is_sat() → bool

Return type:

bool

makevar()

model()

propagate() → bool

Find clauses with a single unassigned lit and make it true in the model

Return type:

bool

trail: list[list[Var]]

class kdrag.solvers.sat.GroundClause(pos, neg)

Bases: NamedTuple

Parameters:

• pos (tuple[BoolRef])

• neg (tuple[BoolRef])

count(value, /)

Return number of occurrences of value.

index(value, start=0, stop=9223372036854775807, /)

Return first index of value.

Raises ValueError if the value is not present.

neg: tuple[BoolRef]

Alias for field number 1

classmethod of_expr(e: BoolRef) → GroundClause

>>> e = smt.Or(smt.Bool("a"), smt.Not(smt.Bool("b")), smt.Bool("c"))
>>> GroundClause.of_expr(e)
GroundClause(pos=(a, c), neg=(b,))

Parameters:

e (BoolRef)

Return type:

GroundClause

pos: tuple[BoolRef]

Alias for field number 0

to_expr() → BoolRef

>>> c = GroundClause((smt.Bool("a"), smt.Bool("c")), (smt.Bool("b"),))
>>> c.to_expr()
Or(a, c, Not(b))

Return type:

BoolRef