solver

package
v0.0.0-...-aa6980f Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Mar 12, 2023 License: GPL-3.0 Imports: 5 Imported by: 0

Documentation

Overview

The solver package contains the BaseCDCLSolver

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func ConstructBaseClause 

func ConstructBaseClause(d types.Disjunction, learnt bool) types.Clause

Constructs an instance of BaseClause from a Disjunction

func ConstructMapClause 

func ConstructMapClause(d types.Disjunction, learnt bool) types.Clause

func ResolveBaseClause 

func ResolveBaseClause(d1, d2 types.Disjunction, lit types.Literal, atomCount uint) types.Clause

func ResolveMapClause 

func ResolveMapClause(d1, d2 types.Disjunction, lit types.Literal, atomCount uint) types.Clause

Types

type BaseCDCLSolver 

type BaseCDCLSolver struct {
	Model         ModelList       // Model is stored in a customized LinkedList. Refer `model.go`
	Check         []*ModelElement // Check is used to check is an Atom has been included in the Model
	AtomCount     uint            // No of Atoms
	DecisionCount uint            // No of decisions made
	F             types.Formula   // Formula of clause to solve satisfiability problem

	/*
		Construct wraps Disjunctions into Clauses.

		This is overwritten on initialization to support modularity.
	*/
	Construct func(types.Disjunction, bool) types.Clause // a Clause Construction function which is overwritten on initialization to support modularity
}

The BaseCDCLSolver is a close implementation of SAT Solver v3 from http://poincare.matf.bg.ac.rs/~filip/phd/sat-tutorial.pdf

func InitializeBaseSolver 

func InitializeBaseSolver(satfile types.SATFile, experimental bool) (solver BaseCDCLSolver, err error)

Intializes all the BaseCDCLSolver fields based on SATFile and CLI Flags

func (*BaseCDCLSolver) AnalyseConflict 

func (solver *BaseCDCLSolver) AnalyseConflict(clause types.Clause) (types.Clause, error)

AnalyseConflict finds a resolvent clause by continously resolving the conflict clause with the reason of last literal of conflict clause to get a new conflict clause till we reach unique implication point

func (*BaseCDCLSolver) Decide 

func (solver *BaseCDCLSolver) Decide(clause types.Clause) error

Decide selects the first unassigned literal from the selected clause 

[TODO] Random Selection of Decide variable

func (*BaseCDCLSolver) ResolveConflict 

func (solver *BaseCDCLSolver) ResolveConflict(clause types.Clause) (err error)

ResolveConflict works in 3 steps

  1. Calls AnalyseConflict to learn new clause
  2. Find the last literal in Model that makes new clause true when we negate it
  3. Find decision level to which we want to BackJump

func (BaseCDCLSolver) Solve 

func (solver BaseCDCLSolver) Solve() (types.Solution, error)

func (*BaseCDCLSolver) UIP 

func (solver *BaseCDCLSolver) UIP(lit types.Literal, clause types.Clause) bool

UIP checks if given literal is the UIP of given clause

func (*BaseCDCLSolver) UnitPropagate 

func (solver *BaseCDCLSolver) UnitPropagate(clause types.Clause) error

UnitPropgate takes the only literal and appends that to our model

type BaseClause 

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

Implements the Clause interface defined in `pkg/types/types.go`

func (BaseClause) Apply 

func (c BaseClause) Apply(l types.Literal) types.Clause

func (BaseClause) Contains 

func (c BaseClause) Contains(l types.Literal) bool

func (BaseClause) Disjunction 

func (c BaseClause) Disjunction() types.Disjunction

func (BaseClause) IsLearnt 

func (c BaseClause) IsLearnt() bool

func (BaseClause) IsSolved 

func (c BaseClause) IsSolved() bool

func (BaseClause) Original 

func (c BaseClause) Original() types.Disjunction

func (BaseClause) Reset 

func (c BaseClause) Reset() types.Clause

func (BaseClause) Type 

func (c BaseClause) Type() types.ClauseType

func (BaseClause) Undo 

func (c BaseClause) Undo(l types.Literal) types.Clause

type BaseFormula 

type BaseFormula struct {
	Clauses []types.Clause
}

func (BaseFormula) Assign 

func (f BaseFormula) Assign(l types.Literal) types.Formula

func (BaseFormula) Learn 

func (f BaseFormula) Learn(c types.Clause) types.Formula

func (BaseFormula) NextClause 

func (f BaseFormula) NextClause() types.Clause

func (BaseFormula) Print 

func (f BaseFormula) Print() string

func (BaseFormula) Restart 

func (f BaseFormula) Restart() types.Formula

func (BaseFormula) Unassign 

func (f BaseFormula) Unassign(l types.Literal) types.Formula

type LiteralState 

type LiteralState int
const (
	UNASSIGNED LiteralState = iota
	ASSIGNED
	REFUTED
)

type MapClause 

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

func (MapClause) Apply 

func (c MapClause) Apply(lit types.Literal) types.Clause

func (MapClause) Contains 

func (c MapClause) Contains(lit types.Literal) bool

func (MapClause) Disjunction 

func (c MapClause) Disjunction() types.Disjunction

func (MapClause) IsLearnt 

func (c MapClause) IsLearnt() bool

func (MapClause) IsSolved 

func (c MapClause) IsSolved() bool

func (MapClause) Original 

func (c MapClause) Original() types.Disjunction

func (MapClause) Reset 

func (c MapClause) Reset() types.Clause

func (MapClause) Type 

func (c MapClause) Type() types.ClauseType

func (MapClause) Undo 

func (c MapClause) Undo(lit types.Literal) types.Clause

type ModelElement 

type ModelElement struct {
	Literal       types.Literal // The Literal Assigned in the Model
	Reason        types.Clause  // The reason for assignment. Used for conflict resolution and unit propagation
	Decision      bool          // True if this is a decision literal
	DecisionLevel uint          // No of decision literal present in model before this literal counting itself
	Next          *ModelElement // The Next Pointer for ModelElement
	Prev          *ModelElement // The Prev Pointer for ModelElement
}

ModelElement is the Node of the ModelList. It represents a literal assignment in the Model

type ModelList 

type ModelList struct {
	Head          *ModelElement // Head of the List
	Tail          *ModelElement // Tail of the List
	DecisionLevel uint          // Number of decision literals in list
	Size          uint          // Size of list
}

ModelList is the LinkedList implementation of the Model Insertion and Deletion is more effecient in Linkedlist so that is why it has been preferred over arrays

func (*ModelList) PopBack 

func (modelList *ModelList) PopBack() (ModelElement, error)

Pop last element of List

func (*ModelList) PopTillLevel 

func (modelList *ModelList) PopTillLevel(level uint) (ModelElement, error)

Pop element of list till a given decision level

func (*ModelList) Pushback 

func (modelList *ModelList) Pushback(m *ModelElement)

Pushing Literal assignment to the Model

func (*ModelList) SearchLastLiteral 

func (modelList *ModelList) SearchLastLiteral(clause types.Clause) (ModelElement, error)

Finding Last Literal that refutes given Clause. Used for conflict resolution

type PQFormula 

type PQFormula struct {
	Clauses PriorityQueue
}

func ConstructHeap 

func ConstructHeap(clauses []types.Clause) PQFormula

func (PQFormula) Assign 

func (f PQFormula) Assign(l types.Literal) types.Formula

func (PQFormula) Learn 

func (f PQFormula) Learn(c types.Clause) types.Formula

func (PQFormula) NextClause 

func (f PQFormula) NextClause() types.Clause

func (PQFormula) Print 

func (f PQFormula) Print() string

func (PQFormula) Restart 

func (f PQFormula) Restart() types.Formula

func (PQFormula) Unassign 

func (f PQFormula) Unassign(l types.Literal) types.Formula

type PriorityQueue 

type PriorityQueue []types.Clause

func (PriorityQueue) Len 

func (pq PriorityQueue) Len() int

func (PriorityQueue) Less 

func (pq PriorityQueue) Less(i, j int) bool

func (*PriorityQueue) Pop 

func (pq *PriorityQueue) Pop() any

func (*PriorityQueue) Push 

func (pq *PriorityQueue) Push(x any)

func (PriorityQueue) Swap 

func (pq PriorityQueue) Swap(i, j int)

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.