dimacs

Documentation

Overview

Package dimacs implements reading and writing of DIMACS format files for satisfiability problem statement.

Index

• func EncodeFile(path string, p *Problem) error
• func EncodeProblem(w io.Writer, p *Problem) error
• type Decoder
  • func NewDecoder(r io.Reader) *Decoder
  • func (r *Decoder) Clause() []Lit
  • func (r *Decoder) Decode() bool
  • func (r *Decoder) Err() error
  • func (r *Decoder) Header() *Header
• type Encoder
  • func NewEncoder(w io.Writer) *Encoder
  • func (enc *Encoder) Close() error
  • func (enc *Encoder) Encode(clause []Lit) error
  • func (enc *Encoder) WriteHeader(h *Header) error
• type Header
• type Lit
  • func (lit Lit) Neg() bool
  • func (lit Lit) Var() int
• type Problem
  • func DecodeFile(path string) (*Problem, error)
  • func DecodeProblem(r io.Reader) (*Problem, error)

Functions

func EncodeFile

func EncodeFile(path string, p *Problem) error

EncodeFile encodes p in DIMACS format and writes the resulting bytes to a new file at path.

func EncodeProblem

func EncodeProblem(w io.Writer, p *Problem) error

EncodeProblem encodes p in DIMACS format and writes the resulting bytes to w.

Types

type Decoder

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

Decoder reads a DIMACS format stream of bytes from an io.Decoder.

func NewDecoder

func NewDecoder(r io.Reader) *Decoder

NewDecoder returns

func (*Decoder) Clause

func (r *Decoder) Clause() []Lit

Clause returns the last clause decoded from the input stream. The underlying storage of the returned slice is part of an internal buffer. Any attempt to presist the clause must store the literal values in a new slice.

func (*Decoder) Decode

func (r *Decoder) Decode() bool

Decode decodes a clause from the input stream. If r can decode a clause true is returned and the clause can be inspected or copied using r.Clause(). If no clause can be decoded false is returned and r.Err() will return any encountered error. If the stream was fully consumed than false will be returned and r.Err() will return nil.

func (*Decoder) Err

func (r *Decoder) Err() error

Err returns any error that encountered while decoding the input bytes.

func (*Decoder) Header

func (r *Decoder) Header() *Header

Header returns the header decoded from the input stream. Header returns nil if no header could be decoded from the input. If Header returns nil then r.Err() will return the encountered error.

type Encoder

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

Encoder encodes Lit clauses as a DIMACS format byte stream.

func NewEncoder

func NewEncoder(w io.Writer) *Encoder

NewEncoder initializes a new Encoder. The returned encoder must be closed before it is discarded to avoid a corrupt output stream.

enc := NewEncoder(f)
defer enc.Close()

func (*Encoder) Close

func (enc *Encoder) Close() error

Close writes any buffered output to the underlying io.Writer. If the number of encoded clauses is less than the number specified in the header an error is returned.

func (*Encoder) Encode

func (enc *Encoder) Encode(clause []Lit) error

Encode encodes clause and writes it to the output stream.

func (*Encoder) WriteHeader

func (enc *Encoder) WriteHeader(h *Header) error

WriteHeader encodes and writes h to the output stream. WriteHeader must be called only once, before any clauses have been written.

type Header

type Header struct {
	NumVar    int
	NumClause int
}

Header precedes clause data in a DIMACS data stream

type Lit

type Lit int

Lit is a simple representation of a clause literal. Positive literals are equal to the variable they contain. Negated literals are equal to the negative value (additive inverse) of the variable they contain. The value 0 is not a valid Lit.

func (Lit) Neg

func (lit Lit) Neg() bool

Neg returns true if the literal is negated (lit == -p for some variable p).

func (Lit) Var

func (lit Lit) Var() int

Var returns the variable of lit. A valid literal has a positive variable.

type Problem

type Problem struct {
	NumVar  int
	Clauses [][]Lit
}

Problem is the statement of a SAT problem in CNF.

func DecodeFile

func DecodeFile(path string) (*Problem, error)

DecodeFile opens path and decodes its contents using DecodeProblem.

func DecodeProblem

func DecodeProblem(r io.Reader) (*Problem, error)

DecodeProblem decodes the contents of r into a new Problem.