twosat

Documentation

Index

• type TwoSat
  • func New(n int) *TwoSat
  • func (ts *TwoSat) AddClause(i int, f bool, j int, g bool)
  • func (ts *TwoSat) Answer() []bool
  • func (ts *TwoSat) Satisfiable() bool

Types

type TwoSat

type TwoSat struct {
	// contains filtered or unexported fields
}

TwoSat defines n, answer and scc

func New

func New(n int) *TwoSat

New creates a TwoSAT of n variables and 0 clauses

func (*TwoSat) AddClause

func (ts *TwoSat) AddClause(i int, f bool, j int, g bool)

AddClause adds a clause.

func (*TwoSat) Answer

func (ts *TwoSat) Answer() []bool

Answer returns a truth assignment that satisfies all clauses of the last call of satisfiable

func (*TwoSat) Satisfiable

func (ts *TwoSat) Satisfiable() bool

Satisfiable returns True if there is a truth assignment that satisfies all clauses