Learning in a compiler for MINSAT algorithms

作     者：Remshagen, A Truemper, K 

作者机构：State Univ W Georgia Dept Comp Sci Carrollton GA 30118 USA Univ Texas Dept Comp Sci Richardson TX 75083 USA 

出 版 物：《THEORY AND PRACTICE OF LOGIC PROGRAMMING》 (逻辑程序设计理论与实践)

年 卷 期：2003年第3卷第3期

页      面：271-286页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：logic minimization problem propositional logic learning lemmas compiler for logic 

摘      要：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.