Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-25T16:00:46.842Z Has data issue: false hasContentIssue false
  • English
  • Français

Learning in a compiler for MINSAT algorithms

Published online by Cambridge University Press:  13 May 2003

ANJA REMSHAGEN  and
KLAUS TRUEMPER
ANJA REMSHAGEN
Affiliation:
Department of Computer Science, State University of West Georgia, 1600 Maple St, Carrollton, GA 30118, USA (email: [email protected])
KLAUS TRUEMPER
Affiliation:
University of Texas at Dallas, Department of Computer Science, EC31, Box 830688, Richardson, TX 75083-0688, USA (email: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper describes learning in a compiler for algorithms solving classes of the logic minimization problem MINSAT, where the underlying propositional formula is in conjunctive normal form (CNF) and where costs are associated with the True/False values of the variables. Each class consists of all instances that may be derived from a given propositional formula and costs for True/False values by fixing or deleting variables, and by deleting clauses. The learning step begins once the compiler has constructed a solution algorithm for a given class. The step applies that algorithm to comparatively few instances of the class, analyses the performance of the algorithm on these instances, and modifies the underlying propositional formula, with the goal that the algorithm will perform much better on all instances of the class.

Keywords

logic minimization problempropositional logiclearning lemmascompiler for logic
Type
Research Article
Information
Theory and Practice of Logic Programming , Volume 3 , Issue 3 , May 2003 , pp. 271 - 286
Copyright
© 2003 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)